Logiweb(TM)

8.4.5 Conditions

Prev Up Next Page 320 of 800 Search internet


The following constructs allow to assume that a side condition holds:

   line L : Condition >> C ; N

Example:

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

We say that the variable #x avoids the term #h, written #x avoid #h if the variable #x does not occur free in the term #h. The lemma above says that if #x avoids #h and if #h imply #a then #h imply all #x : #a. The proof of the lemma reads:

prepare proof indentation,proof of ConditionExample : 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 L01 >> 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 Line L01 we assume that #x avoids #a.

In Line L02 we assume #h imply #a as a premise and in Line L03 we generalize the premise.

Axiom A5 of first order predicate calculus says:

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 we use modus probans on Axiom A5 and the side condition we assumed in Line L01. Finally, we use modus ponens on Line L04 and Line L03.

Using a condition is the typical way to prove a lemma of form A endorse B.

Do not use conditions in proof of form

   T proof of L : P qed

where T is Prop, FOL, or Peano from the Peano page. The tactics of Prop, FOL, and Peano are not intended to be used together with conditions.

Prev Up Next Page 320 of 800 Search logiweb.eu

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