## 6.7.3 The contents of the multzero page

 Page 89 of 800 Search internet

Recall multzero.lgs:

     1	"";;014E20344F3D486370710A10269E83D974EB8E9787EFB994A0BBD8BB0806
2	""P multzero
3	""R check
4	""R Peano
5	""R base
6
7	""D 0
8	3.2l
9
10	""B
11	page ( ""N , ""C )
12	title "Multiplication by zero"
13	bib "
14	@Book         {Mendelson87,
15	  author    = {E. Mendelson},
16	  title     = {Introduction to Mathematical Logic},
17	  publisher = {Wadsworth and Brooks},
18	  year      = {1987},
19	  edition   = {3.}}
20	"
21	main text "
22	\title{Multiplication by zero}
23	\author{A. U. Thor}
24	\maketitle
25	\tableofcontents
26	"[ make macro expanded version ragged right ]"
27	"[ prepare proof indentation ]"
28	\section{Theorem}
29	We now state Lemma 3.2l of \cite{Mendelson87}:
30	"[ PA lemma 3.2l : all x : 0 * x = 0 end lemma ]"
31	\section{Proof}
32	"[ PA proof of 3.2l :
33	line L01 : S7 >> 0 * 0 = 0 ;
34	line L02 : Block >> Begin ;
35	line L03 : Hypothesis >> 0 * x = 0 ;
36	line L04 : S8 >> 0 * x suc = 0 * x + 0 ;
37	line L05 : S5 >> 0 * x + 0 = 0 * x ;
38	line L06 : 3.2c mp L04 mp L05 >> 0 * x suc = 0 * x ;
39	line L07 : 3.2c mp L06 mp L03 >> 0 * x suc = 0 ;
40	line L08 : Block >> End ;
41	line L09 : Induction at x ponens L01 ponens L08 >> 0 * x = 0 ;
42	line L10 : Gen1 ponens L09 >> all x : 0 * x = 0 qed ]"
43	\bibliography{./page}
44	"
45	appendix "
46	\title{Multiplication by zero - appendix}
47	\author{A. U. Thor}
48	\maketitle
49	\tableofcontents
50	\section{\TeX\ definitions}
51	\begin{statements}
52	\item "[[ tex show define 3.2l as "
53	\mathbf{3.2l}" end define ]]"
54	\end{statements}
55	"
56	end page
57



The multzero page merely proves one lemma. That lemma is Lemma 3.2l of E. Mendelson: Introduction to Mathematical Logic.

Line 8 defines 3.2l as a new, syntactic construct and Line 30 states Lemma 3.2l:

Thus, Lemma 3.2l says that follows from the rules of Peano arithmetic where is defined on the Peano page.

The check and Peano pages do not distinguish between axioms, axiom schemes, and inference rules. On those pages, the word 'rule' is used for all three cases.

Lines 32-42 prove Lemma 3.2l:

Thus, the proof is expressed relative to Peano arithmetic . That defines which axioms and inference rules are applicable. It also defines how the proof is tactic expanded before it is verified.

The Peano page defined propositional calculus , first order predicate calculus , and Peano arithmetic . The Peano page also defines the following tactics:

Thus, proofs expressed relative to first order predicate calculus and Peano arithmetic are tactic expanded as specified by whereas proofs expressed in propositional calculus are tactic expanded by . The difference between the two tactics is microscopic.

Before a proof is verified, it is macro expanded and then tactic expanded. The output from macro expansion is kept in the cache whereas the output from tactic expansion is forgotten the moment the output has been verified.

 Page 89 of 800 Search logiweb.eu