Logiweb system pages
Tutorial T03: Proving

### Introduction

The present tutorial teaches how to state a lemma and a proof.

### Prerequisites

You must have done Tutorial T01: Hello world.

### References

As 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:

• Open the header creation form in a separate window (in most browsers: right click the link and select something like 'open in new window').
• Enter the text above in the upper text window.
• Click 'Suggest Header'.
• Enter some strings in the 'org=' and 'name=' fields.

### The bed page

The 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 construct

In 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 lemma

Put 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

• Use the 'level' control to change 'level=body' to 'level=all'.
• Click 'Submit'.

### Viewing your page

Click 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 self-contained 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 meta-quantifiers 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.

• Look up lemma 3.2l in the codex of your page

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

• Try to add "[[ ttst trace ( self [[ quote self end quote ref ]] [[ "codex" ]] [[ quote 3.2l end quote ref ]] [[ quote 3.2l end quote idx ]] [[ 0 ]] [[ statement ]] ) end test ]]" to your 'multiplication by zero' page and translate with 'level=compile'. The 'self' construct macro expands to the page construct of your page (your 'my page' construct declared in the PAGE section). The value of the page construct is the cache of the page, which is an array. The array is indexed by 'quote self end quote ref' where self macro expands to your page construct, the quote prohibits your page construct from being evaluated, and the 'ref' operator extracts the reference of your page. That gives the rack of your page. Then pick the 'codex' from the rack, use the reference and index of the 3.2l construct to get to the definitions of 3.2l, use a zero to get to aspects represented by strings, and use 'statement' to get to the statement aspect of 3.2l. As you can see from the output from pyk when you hit 'Submit', the statement aspect of 3.2l is the definition of the statement aspect of 3.2l. Using 'self' and array indexing you can access all of the semantics of your page represented as simple data structures.
• Read the base, check, and Peano pages (in that order) to get loads of information about how things work. The base and check pages have all the definitions but could use more explanations. I work on that. If you have problems, contact me at grue@diku.dk.
• Read the help text in general and the page on loading in particular.
• Try writing some macro definitions like "[[ macro define f ( x ) as x + 1 end define ]]" and see how they work.
• The base page contains some advanced macro definitions like one which expands a tuple << 1 ,, 2 ,, 3 >> into a sequence 1 :: 2 :: 3 :: T of pairs. To make such macros you need a 'Macro define' rather than a 'macro define' construct. Read the base page to see how advanced macros work.
• Download and install Logiweb locally.
• Formalize mathematics. Send me a note on grue@diku.dk when you are done.
• Write some papers for publication in the 'Logiweb journal on formalization of mathematics'. Papers are published as follows: (1) Publish your paper on Logiweb. (2) Send the reference of your paper to me at grue@diku.dk. (3) If referees request changes, update your paper accordingly, publish your paper again on Logiweb, and go to (2). (4) When your paper is accepted, the next issue of the online journal will contain a Logiweb reference to your paper. Furthermore, your paper is mirrorred such that it remains in existence even if you delete your copy. The 'Logiweb journal on formalization of mathematics' is something I intend to establish later, but if you have a good paper, don't hesitate to send it to me. Making a Logiweb journal is easy, so I will do it on demand, if needed. If you have some small, well formulated formalization, then your could also consider writing about it on WikiPedia with a link to your formalization.
• Subscribe to the Logiweb mailing lists by sending e-mails to logiweb-request@diku.dk, logiweb-announce@diku.dk, and logiweb-notices@diku.dk with body 'subscribe' (without the quotes). The 'logiweb-announce' list announces new version, the 'logiweb-notices' list announces new pages, and you may ask for help at the 'logiweb' list.
• Have fun.

### Conclusion

You have now verified your first proof using Logiweb.