Logiweb(TM)

8.5.11 Verify

Prev Up Next Page 336 of 800 Search internet


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

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

PA lemma VerifyExample1 : c = 0 imply all u : c = 0 end lemma

prepare proof indentation,proof of VerifyExample1 : line L01 : Premise >> PA ; line L02 : M1.8f >> c = 0 imply c = 0 ; line L03 : Gen ponens L02 >> all u : ( c = 0 imply c = 0 ) ; line L04 : A5 >> all u : ( c = 0 imply c = 0 ) imply c = 0 imply all u : c = 0 ; line L05 : MP ponens L04 ponens L03 >> c = 0 imply all u : c = 0 qed

Axiom A5 reads:

rule A5 : All #x ,, #a ,, #b : #x avoid #a endorse all #x : ( #a imply #b ) imply #a imply all #x : #b end rule

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

We may also prove the lemma thus:

PA lemma VerifyExample2 : c = 0 imply all u : c = 0 end lemma

prepare proof indentation,proof of VerifyExample2 : line L01 : Premise >> PA ; line L02 : M1.8f >> c = 0 imply c = 0 ; line L03 : Gen ponens L02 >> all u : ( c = 0 imply c = 0 ) ; line L04 : MP ponens A5 At At At Verify ponens L03 >> c = 0 imply all u : c = 0 qed

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 A5 Conclude in place of A2 At At At Verify.

Prev Up Next Page 336 of 800 Search logiweb.eu

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