Logiweb(TM)

11.9 multzero: A small formal proof

Prev Up Next Page 386 of 800 Search internet


The multzero page states and proves a simple lemma. The page uses the definition of Peano arithmetic, a lemma, and a lot of proof tactics from the Peano page. A numbered version of the multzero.lgs source text is included below. Also see the original, unnumbered lgs file, the main pdf, and the document root.

     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	

Prev Up Next Page 386 of 800 Search logiweb.eu

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