Logiweb(TM)

8.3.1 Proof constructors

Prev Up Next Page 310 of 800 Search internet


A 'proof constructor' is construct like

   T proof of L : P

which proves a lemma. The constructor above proves the lemma L in the theory T using the proof P.

We shall refer to the proof constructor above as the T proof constructor as opposed to the plain proof constructor described later.

As an example of a proof constructed by the T proof constructor, take the proof of 3.2l on the multzero page:

prepare proof indentation,PA proof of 3.2l : line L01 : S7 >> 0 * 0 = 0 ; line L02 : Block >> Begin ; line L03 : Hypothesis >> 0 * x = 0 ; line L04 : S8 >> 0 * x suc = 0 * x + 0 ; line L05 : S5 >> 0 * x + 0 = 0 * x ; line L06 : 3.2c mp L04 mp L05 >> 0 * x suc = 0 * x ; line L07 : 3.2c mp L06 mp L03 >> 0 * x suc = 0 ; line L08 : Block >> End ; line L09 : Induction at x ponens L01 ponens L08 >> 0 * x = 0 ; line L10 : Gen1 ponens L09 >> all x : 0 * x = 0 qed

Prev Up Next Page 310 of 800 Search logiweb.eu

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