8.3.5 Plain proofs

Prev Up Next 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 P in order to prove L. Tactic evaluation is similar to macro expansion and rendering.

The T proof constructor uses the tactic definition of T to prove L. 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'.

Prop lemma M1.8a : #x imply #x end lemma

prepare proof indentation,proof of M1.8a : line L01 : Premise >> Prop ; line L02 : A2 >> ( #x imply ( #y imply #x ) imply #x ) imply newline ( #x imply #y imply #x ) imply #x imply #x ; line L03 : A1 >> #x imply ( #y imply #x ) imply #x ; line L04 : MP ponens L02 ponens L03 >> ( #x imply #y imply #x ) imply #x imply #x ; line L05 : A1 >> #x imply #y imply #x ; line L06 : MP ponens L04 ponens L05 >> #x imply #x qed

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

In Line L05 we use Axiom A1 of Prop to prove #x imply #y imply #x. Line L02 and L03 are similar.

In Line L06 we apply Modus Ponens MP of Prop to Line L04 and L05 to conclude #x imply #x. Line L04 is similar.

Prev Up Next Page 314 of 800 Search logiweb.eu

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