Logiweb(TM)

8.5.16 Infer

Prev Up Next Page 341 of 800 Search internet


The infer operator P infer C allows to state a premise inside an argumentation. As an example, consider this lemma:

Prop lemma PremiseExample1 : #x infer #y imply #x end lemma

A human reader friendly proof reads:

prepare proof indentation,proof of PremiseExample1 : line L01 : Premise >> Prop ; line L02 : Premise >> #x ; line L03 : A1 >> #x imply #y imply #x ; line L04 : MP ponens L03 ponens L02 >> #y imply #x qed

We may also state Line L02-L04 as a one-liner, however:

Prop lemma PremiseExample2 : #x infer #y imply #x end lemma

A human reader friendly proof reads:

prepare proof indentation,proof of PremiseExample2 : line L01 : Premise >> Prop ; line L02 : #x infer ( MP ponens A1 Conclude ) Ponens >> #x infer #y imply #x qed

Thus, the infer operator can replace the premise in Line L02 in the proof of PremiseExample1 above. The infer operator cannot replace the premise in Line L01 because unitac-rule only searches for rules in conclusions of previous proof lines. Thus, you cannot use A1 and MP unless you assume Prop in a proof line of its own. Or, rather, if you really want to avoid assuming Prop on a line of its own, then you really have to work hard to construct sequent operators which unitac-rule normally generates for you.

The endorsement operator S endorse C is similar to the infer operator. The endorsement operator can be used for replacing condition lines.

Prev Up Next Page 341 of 800 Search logiweb.eu

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