Logiweb(TM)

6.7.2 The claim of the multzero page

Prev Up Next Page 88 of 800 Search internet


A numbered version of multzero.lgs looks thus:

     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 references check, Peano, and base in that order. Since check is first, the multzero page is verified according to the claim of the check page. Had the base page been first then multzero would have been verified according to the claim of the base page. The claims of the base, check, and Peano pages are:

base
All test cases are checked.
check
All test cases and all proofs are checked.
Peano
All test cases, all proofs, and all math definitions are checked.

Thus, you can also choose to have Peano as your first reference and still get your proofs checked.

The claim of the check page is defined thus in check.lgs:

   verifier test1 &c proofcheck end verifier

The test1 function is the one which scans the page and evaluates all test cases. It is the test1 function which verified the test case on the combinations page.

The proofcheck function is the Logiweb proof checker. Among other, it checks everything on a page which it recognizes as a proof. It also checks that proofs do not reference each other in a circular way. And whenever a proof references a lemma on another page, proofcheck verifies that that other page was also checked by proofcheck and that the check was positive. That is a very fast check to conduct since proofcheck just has to look up the diagnose of the referenced page to see that the referenced page is correct.

If multzero had had a claim of its own, then that claim would have been used in place of the claim of the check page.

You can define your own claims if you like. And you can choose to combine claims using the &c conjunction. As an example, if you want to enforce a type discipline, you can define a type checker and add it to the conjunction of claims.

Prev Up Next Page 88 of 800 Search logiweb.eu

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