Logiweb system pages  
Tutorial T03: Proving  
System pages 
IntroductionThe present tutorial teaches how to state a lemma and a proof. PrerequisitesYou must have done Tutorial T01: Hello world.ReferencesAs in Tutorial T01: Hello world, construct a page with the following bibliography: PAGE my page BIBLIOGRAPHY "check" "http:../../../page/check/latest/vector/page.lgw". "Peano" "http:../../../page/Peano/latest/vector/page.lgw". "base" "http:../../../page/base/latest/vector/page.lgw". In case you have forgot, these are the steps to perform:
The bed pageThe first reference of your page is called the 'bed' page of your page in Logiweb terminology. The bed page defines several things: how your page is macro expanded, how it is verified, how it is rendered, and how it is unpacked. The check page defines a macro expanding engine and a verification engine. The verification engine is a conjunction of the a proof checker defined on the check page itself and a test evaluator from the base page which takes care of 'ttst', 'ftst', and 'etst' constructs. In general, one should define the verification engine as a conjunction of several verification engines since one typically requires a page to be correct in many different ways. As an example, one may introduce typing and require a page to be type correct in addition to requiring that test cases succeed and that proof are correct. The sense in which a page is correct can be looked up in the codex of the bed page. The proof checker defined on the check page only accepts references to lemmas on other pages if (1) the other page has been checked by the proof checker itself and (2) the other page is deemed to be correct. The check page defines no rendering engine and no unpacking engine. For that reason, your page is rendered using default rendering and unpacked using default unpacking. Default rendering can do many things. See the 'renderer' and 'rendered' pages in the test suite that comes with Logiweb for examples of custom rendering. The 'rendered' page defines a 'colon droping quantifier' which has the property that if one writes 'all X : exists Y : Z' then the universal quantifier is rendered without a colon because it is followed by another quantifier. That is beyound the capability of default rendering. See the 'unpacker' and 'unpacked' pages in the test suite which comes with Logiweb for an example of a custom unpacker. A custom unpacker can be used for decompressing compressed pages or decrypting encrypted pages. Look here for a description of how a Logiweb page is treated by the system. In short, a page is treated thus: the unpacker converts the page from a sequence of bytes to a body, a bibliography, and a dictionary. Then the body is macro expanded and the codex is constructed by 'harvesting' definitions in the expansion. Then the page is verified based on the codex and the expansion, and the page is rendered based on the unexpanded body. Note that macro expansion happens before verification. As an example, parentheses are macro defined such that they disappear during macro expansion. For that reason, the proof checker does not need to care about parentheses. Introduce a new constructIn the upper window, add a line after the one saying "base" base: ... PREASSOCIATIVE "check" check "Peano" Peano "base" base "" 3.2l PREASSOCIATIVE "base" +" ...The 3.2l construct is going to represent Lemma 3.2l in Mendelson: Introduction to Mathematical Logic. Stating and proving the lemmaPut the following in the lower text window: BODY page ( Pyk , Priority ) title "Multiplication by zero" bib " @Book {Mendelson87, author = {E. Mendelson}, title = {Introduction to Mathematical Logic}, publisher = {Wadsworth and Brooks}, year = {1987}, edition = {3.}} " main text " \title{Multiplication by zero} \author{A. U. Thor} \maketitle \tableofcontents "[ make macro expanded version ragged right ]" "[ prepare proof indentation ]" \section{Theorem} We now state Lemma 3.2l of \cite{Mendelson87}: "[ PA lemma 3.2l : all x : 0 * x = 0 end lemma ]" \section{Proof} "[ 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 ]" \bibliography{./page} " appendix " \title{Multiplication by zero  appendix} \author{A. U. Thor} \maketitle \tableofcontents \section{\TeX\ definitions} \begin{statements} \item "[[ tex define 3.2l as " \mathbf{3.2l}" end define ]]" \end{statements} " end page The 'lemma' and 'proof' constructs make TeX switch to vertical mode. For that reason, they should not be surrounded by dollar signs. That is why they are included in "[...]" rather than "[[...]]". Submit your page
Viewing your pageClick to your page (following the here link in the Logiwiki response). Then click 'Body' and 'Pdf' to see your page. The lemma says that 0 * x = 0 holds for all x. Then look up the expansion of your page (Click 'back' two times, then click 'Expansion' and 'Pdf'). In the macro expanded version, your lemma has been expanded into two definitions: a statement definition and a unitac definition. The statement definition defines the statement aspect of 3.2l to be a statement which says that PA (Peano arithmetic) infers that for all terms x, 0 * x = 0. That is your lemma in a selfcontained form in which Peano arithmetic is assumed as a premise. The unitac definition says what the unification tactic should do when it sees a reference to 3.2l in some other proof in case somebody else decides to build on top of your work. The unification tactic is defined on the check page and is responsible for instantiating metaquantifiers suitably. Read the check page for details. Your proof has been macro expanded into a definition of the proof aspect of 3.2l. The proof checker defined on the check page considers 3.2l as a lemma because it has both a statement and a proof aspect. If you stated the lemma without a proof, the proof checker would have accepted the lemma as a conjecture; but the checker would protest if you tried to use the lemma without proving it first. If you stated the proof without a lemma, the proof checker would protest. The macro expanded proof looks somewhat different from the unexpanded one. When your proof is checked, it is 'tactic' evaluated. Tactic evaluation and macro expansion are both Turing complete, so it is up to the one who defines the proof checker how much should be done by the macro expander and how much by the tactic evaluator. A difference between the two is that the outcome of macro expansion is kept for future reference whereas the outcome from tactic evaluation is discarded as soon as the outcome has been checked for correctness.
In the codex you can see the statement, unitac, proof, tex, and pyk definitions of lemma 3.2l. In the codex you can see all the understood parentheses. Suggestions for further work/reading
ConclusionYou have now verified your first proof using Logiweb.
