This rule can only be used forwards to derive the sub formula of a FOR ALL formula with the variable replaced by another term.
To use it forwards:
- select an empty line and click on For All Elimination.
- then select the FOR ALL formula line you wish to use in the elimination (the formula must be in the scope of the empty line).
- when prompted enter the term you wish to replace the variable (shown in the prompt) with. This term must already be in the signature of the empty line.
- if the FOR ALL formula you selected had multiple FOR ALL quantifiers around the sub formula (e.g. AxAy[f]) then you will also be asked in turn to enter a term to replace each of the variables with until you don't enter a term for a variable, or you have eliminated all of the variables).
- the sub formula will then be added to your proof as a new line with the FOR ALL variables eliminated replaced by the terms you entered.
|