For All Elimination
   
 

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:

  1. select an empty line and click on For All Elimination.
  2. 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).
  3. 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.
  4. 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).
  5. 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.