## 8.3.5 Plain proofs

Page 314 of 800 |
| Search internet |

The T proof constructor

T proof of L : P

has a companion

proof of L : P

which we shall refer to as the *plain proof constructor*.

The plain proof constructor tactic evaluates in order to prove . Tactic evaluation is similar to macro expansion and rendering.

The T proof constructor uses the tactic definition of to prove . Thus, the T proof constructor allows to customize tactic evaluation on a per theory basis whereas the the plain proof constructor treats all proofs equally.

As an example of a proof which uses the plain construct, consider the following proof of Lemma 1.8 in Mendelson: 'Introduction to mathematical logic'.

In Line we assume propositional calculus as defined on the Peano page.

In Line we use Axiom of to prove . Line and are similar.

In Line we apply Modus Ponens of to Line and to conclude . Line is similar.

Page 314 of 800 |
| Search logiweb.eu |

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