## 8.5.11 Verify

Page 336 of 800 |
| Search internet |

The verify operation says that if the side condition endorses the conclusion , written , and if the side condition evaluates to , then we can conclude . The verification operator is named .

As an example of use, consider the following lemma and proof:

Axiom reads:

In Line L04 of the proof above, adaption replaces by to get rid of three meta-quantifiers and a side condition. The side condition evaluates to because avoids (i.e. does not occur free in ).

We may also prove the lemma thus:

Above, the verify operator has to be given explicitly because adaption is not applied to the second argument of ponens operators.

As noted later, one can write in place of .

Page 336 of 800 |
| Search logiweb.eu |

Copyright © 2010
Klaus Grue,
GRD-2010-01-05