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:

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

Thus, Lemma 3.2l says that all x : 0 * x = 0 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 Prop , first order predicate calculus FOL , and Peano arithmetic . The Peano page also defines the following tactics:

$tactic define Prop as \ u . tactic-Prop ( u ) end define$

$tactic define FOL as \ u . tactic-FOL ( u ) end define$

$tactic define PA as \ u . tactic-FOL ( u ) end define$

Thus, proofs expressed relative to first order predicate calculus and Peano arithmetic are tactic expanded as specified by tactic-FOL ( u ) whereas proofs expressed in propositional calculus are tactic expanded by tactic-Prop ( u ) . 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