Page 97 of 800
| Page 97 of 800 | Search internet |
Recall the proof of 
:
Line 
finishes the proof. The conclusion of the proof reads 
since all the reasoning was done under the premise 
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:
Thus, the lemma also says 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.
| Page 97 of 800 | Search logiweb.eu |