|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|