8.5.19 Reference and dereference

Prev Up Next Page 344 of 800 Search internet

The dereferencing operator A Deref modifies the conclusion of A into the statement aspect of that conclusion. Hence, if the conclusion is e.g. the name of an axiom, then the dereferencing operator changes the name of the axiom into what the axiom says.

The referencing operator A id est N does the opposite: if the statement aspect of the name N equals the conclusion of A, then the operator changes the conclusion to be the name N.

As examples of use, we define intuitionistic propositional calculus IProp thus:

theory IProp : A1 oplus A2 oplus MP end theory

Then we state that intuitionistic propositional calculus follows from propositional calculus:

Prop lemma IPropLemma : IProp end lemma

prepare proof indentation,proof of IPropLemma : line L01 : Premise >> Prop ; line L02 : L01 Deref >> A1 oplus A2 oplus A3 oplus MP oplus Def ; line L03 : HeadLemma Init Deref ponens L02 >> A1 ; line L04 : TailLemma Init Deref ponens L02 >> A2 oplus A3 oplus MP oplus Def ; line L05 : HeadLemma Init Deref ponens L04 >> A2 ; line L06 : TailLemma Init Deref ponens L04 >> A3 oplus MP oplus Def ; line L07 : TailLemma Init Deref ponens L06 >> MP oplus Def ; line L08 : HeadLemma Init Deref ponens L07 >> MP ; line L09 : ConsLemma Init Deref ponens L05 ponens L08 >> A2 oplus MP ; line L10 : ConsLemma Init Deref ponens L03 ponens L09 >> A1 oplus A2 oplus MP ; line L11 : L10 id est IProp >> IProp qed

In Line L01 we assume Prop. In line L02 we dereference it into A1 oplus A2 oplus A3 oplus MP oplus Def. Then we prove A1 oplus A2 oplus MP in Line L03-L10. And finally we change A1 oplus A2 oplus MP to IProp in Line L11.

In the intermediate lines L03-L10 we also happen to use dereferencing. The Cons, Head, and Tail lemmas were proved on the previous page.

The Cons, Head, and Tail lemmas have no associated unitac aspect, so they cannot be used directly. Instead, we use the init operation followed by dereferencing as in HeadLemma Init Deref. The init operation states that HeadLemma holds because it is proved 'elsewhere', and the dereferencing operation changes HeadLemma to All #x ,, #y : ( #x oplus #y ) infer #x. 'Elsewhere' covers previous proof lines, lemmas on the same page, and lemmas on transitively referenced pages. When 'elsewhere' covers lemmas on the same page, be sure not to use lemmas in a circular fashion or you will get a Circular proof error message. 'Elsewhere' also covers argumentations like #x infer #x Init where #x is assumed by the inference operator and then used immediately.

Prev Up Next Page 344 of 800 Search logiweb.eu

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