Logiweb(TM)

6.7.3 The contents of the multzero page

Prev Up Next 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 PA where PA 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:

prepare proof indentation,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

Thus, the proof is expressed relative to Peano arithmetic PA. 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 PA. 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.

Prev Up Next Page 89 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05