|Page 344 of 800||Search internet|
The dereferencing operator modifies the conclusion of 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 does the opposite: if the statement aspect of the name equals the conclusion of , then the operator changes the conclusion to be the name .
As examples of use, we define intuitionistic propositional calculus thus:
Then we state that intuitionistic propositional calculus follows from propositional calculus:
In Line L01 we assume Prop. In line L02 we dereference it into . Then we prove in Line L03-L10. And finally we change to 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 . The init operation states that holds because it is proved 'elsewhere', and the dereferencing operation changes to . '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 where is assumed by the inference operator and then used immediately.
|Page 344 of 800||Search logiweb.eu|