Logiweb(TM)

8.5.12 Unary modus probans

Prev Up Next Page 337 of 800 Search internet


Unary modus probans A Probans expresses A probans S without specifying the side condition S. Unary modus probans can be used in place of binary modus probans in Line L04 of the proof of ConditionExample stated earlier:

PA lemma ConditionExample1 : #x avoid #h endorse #h imply #a infer #h imply all #x : #a end lemma

prepare proof indentation,proof of ConditionExample1 : line L00 : Premise >> PA ; line L01 : Condition >> #x avoid #h ; line L02 : Premise >> #h imply #a ; line L03 : Gen ponens L02 >> all #x : ( #h imply #a ) ; line L04 : A5 Probans >> all #x : ( #h imply #a ) imply ( #h imply all #x : #a ) ; line L05 : MP ponens L04 ponens L03 >> #h imply all #x : #a qed

In the proof above, unary modus probans is used in Line L04 to prevent adaption from verifying the side conditions of A5. An attempt to verify the side condition would fail since one cannot know whether or not #x avoids #h. That is so because the meta variables #x and #h can denote arbitrary terms so #x avoids #h for some but not all terms #x and #h.

Prev Up Next Page 337 of 800 Search logiweb.eu

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