Logiweb(TM)

6.7.11 Line L10 of the proof

Prev Up Next Page 97 of 800 Search internet


Recall the proof of 3.2l:

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

Line L10 finishes the proof. The conclusion of the proof reads PA infer all x : 0 * x = 0 since all the reasoning was done under the premise PA in the header of the proof.

When the Logiweb proof checker has verified a proof, it compares the conclusion with the associated lemma. In this case, the lemma reads:

PA lemma 3.2l : all x : 0 * x = 0 end lemma

Thus, the lemma also says PA infer all x : 0 * x = 0 which is fine.

The Logiweb proof checker complains if the proof proves something different from what the lemma states. And it whines if it finds a proof with no associated lemma.

On the other hand, the Logiweb proof checker does not care at all if you state a lemma without proof. The proof checker just thinks of such a lemma as a conjecture and does not care as long as you do not use the lemma in proofs.

Actually, the Logiweb proof checker does not distinguish between lemmas, theories, conjectures, axioms, inference rules, and object theories. To Logiweb, they are all just 'statements' expressed inside the language of the Logiweb sequent calculus.

Prev Up Next Page 97 of 800 Search logiweb.eu

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