{ Logiweb, a system for electronic distribution of mathematics Copyright (C) 2004 Klaus Grue This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307 USA Contact: Klaus Grue, DIKU, Universitetsparken 1, DK2100 Copenhagen, Denmark, grue@diku.dk, http://yoa.dk/, http://www.diku.dk/~grue/ Logiweb is a system for distribution of mathematical definitions, lemmas, and proofs. For more on Logiweb, consult http://yoa.dk/. } PAGE peano {A bibliography may look like e.g. base: nani seku tisa teki teni neku sise kati tani sike take kuke nuti sise suka seti kanu sase nete susu tesu kute susi kunu kinu sana sese sita nasa natu, ground: "http://yoa.dk/logiweb/page/ground/vector/page.lgw", first floor: "http:first-floor/latest/vector/page.lgw", second floor: "file:page/second-floor/vector/page.lgw" third floor: "lgw:01A0FFF3C5ACDE30FD3D7FAB8708D230D33DDDFD919184AFC8C9B29A0806" In general, a bibliography is a comma separated list of bibliographic entries. Each entry has two elements: A name (like 'base') and then either a reference in mixed endian kana or the url of a page. The url may start with "http:" in which case it is looked up on the internet. If "http:" is followed by a slash, the url is looked up as it is. Otherwise, it is relative to the "url=..." option of the pyk compiler. The url may also start with "file:" in which case it is looked up in the local file system. Finaly, the url may start with "lgw:" in which case the characters following "lgw:" are interpretted as a Logiweb reference in mixed endian kana.} BIBLIOGRAPHY base: nani suse neni kike sake setu naki seti senu tuse nutu tita nine tene sate kane niki nuni kiti sini tuna keku kuku keke kune suta seka sise nasa natu PREASSOCIATIVE base: bracket * end bracket, intro * index * pyk * tex * end intro, intro * pyk * tex * end intro, peano zero, peano one, peano two, peano a, peano b, peano c, peano d, peano e, peano f, peano g, peano h, peano i, peano j, peano k, peano l, peano m, peano n, peano o, peano p, peano q, peano r, peano s, peano t, peano u, peano v, peano w, peano x, peano y, peano z, peano nonfree * in * end nonfree, peano nonfree star * in * end nonfree, peano free * set * to * end free, peano free star * set * to * end free, peano sub * is * where * is * end sub, peano sub star * is * where * is * end sub, system s, axiom a one, axiom a two, axiom a three, axiom a four, axiom a five, axiom s one, axiom s two, axiom s three, axiom s four, axiom s five, axiom s six, axiom s seven, axiom s eight, axiom s nine, rule mp, rule gen, lemma l three two a PREASSOCIATIVE base: * sub * end sub, * peano var PREASSOCIATIVE base: unicode start of text * end unicode text PREASSOCIATIVE base: * bit nil PREASSOCIATIVE base: * apply * PREASSOCIATIVE base: * raw head, * peano succ PREASSOCIATIVE base: * times *, * peano times * PREASSOCIATIVE base: * plus *, * peano plus * PREASSOCIATIVE base: * term plus * end plus POSTASSOCIATIVE base: * raw pair * POSTASSOCIATIVE base: * comma * PREASSOCIATIVE base: * boolean equal *, * peano is *, * is peano var PREASSOCIATIVE base: not *, peano not * PREASSOCIATIVE base: * and *, * peano and * PREASSOCIATIVE base: * or *, * peano or * PREASSOCIATIVE peano all * indeed *, peano exist * indeed * POSTASSOCIATIVE base: * macro imply *, * peano imply *, * peano iff * POSTASSOCIATIVE base: * guard * PREASSOCIATIVE base: * select * else * end select PREASSOCIATIVE base: lambda * dot * PREASSOCIATIVE base: * init PREASSOCIATIVE base: * at * POSTASSOCIATIVE base: * infer * PREASSOCIATIVE base: all * indeed * POSTASSOCIATIVE base: * rule plus * POSTASSOCIATIVE base: * cut * PREASSOCIATIVE base: * proves * PREASSOCIATIVE base: locally define * as * cut * POSTASSOCIATIVE base: * then * PREASSOCIATIVE base: * tab * PREASSOCIATIVE base: * row * BODY "File page.tex \documentclass [fleqn]{article} \setlength {\overfullrule }{1mm} \input{lgwinclude} \usepackage{latexsym} %\setlength{\parindent}{0em} %\setlength{\parskip}{1ex} % The font of each Logiweb construct is under tight control except that % strings are typeset in whatever font is in effect at the time of % typesetting. This is done to enhance the readability of strings in the % TeX source generated by Logiweb. The default font for typesetting % strings is \rm: \everymath{\rm} \usepackage{makeidx} \usepackage{page} \makeindex \newcommand{\intro}[1]{\emph{#1}} \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} \newlength{\bracketwidth} \settowidth{\bracketwidth}{$[{}$} \newcommand{\back}{\protect\makebox[-1.0\bracketwidth]{}} \usepackage[dvipdfm=true]{hyperref} \hypersetup{pdfpagemode=none} \hypersetup{pdfstartpage=1} \hypersetup{pdfstartview=FitBH} \hypersetup{pdfpagescrop={120 130 490 730}} \hypersetup{pdftitle=Introduction to Logiweb} \hypersetup{colorlinks=true} \bibliographystyle{plain} % \tex{something} writes something to page.otx for later inclusion \newwrite\outex \newtoks\toktex \immediate\openout\outex=page.otx \newcommand{\tex}[1]{\toktex={\item #1}\immediate\write\outex{\the\toktex}} % \test{something} writes something to page.tst for later inclusion \newwrite\outest \immediate\openout\outest=page.tst \newcommand{\test}[1]{\toktex={\item #1}\immediate\write\outest{\the\toktex}} % Concerning \catcode`\@=11 : See the TeXbook, Appendix B (page 344). % \afterheading suppresses indentation once, c.f. latex.ltx. % \display{something} displays something as a displayed equation except % that linebreaking is possible and displaymath is not turned on by default. % The first paragraph after \display{something} is unindented. % Glue below formulas may be wrong. The definition of \display misses % something like \addvspace{\belowdisplayskip}. \catcode`\@=11 \def\afterheading{\@afterheading} \catcode`\@=12 \newcommand{\display}[1]{\begin{list}{}{\setlength{\leftmargin}{\mathindent}} \item #1\end{list} \afterheading} \newcommand{\statement}[1]{\begin{list}{}{\setlength{\leftmargin}{0mm}} \item #1\end{list} \afterheading} \begin {document} \title {Introduction to Logiweb} \author {Klaus Grue} \maketitle \tableofcontents "[ ragged right expansion ]" \section{Peano arithmetic} This Logiweb page \cite{logiweb} defines Peano arithmetic. \subsection{Introduction of new constructs} The following constructs allow to introduce a new construct (``introduce'' in the normal sense of the word, not in the sense of a Logiweb revelation). The constructs allow to define the pyk aspect "[ bracket var p end bracket ]" and tex aspect "[ bracket var t end bracket ]" of a new construct "[ bracket var x end bracket ]" and also makes two entries in the index. The first of the constructs below adds the text "[ bracket var i end bracket ]" in front of one of the index entries. % \index{intro: intro * index * pyk * tex * end intro @intro: "[ bracket unicode start of text text intro var x index var i pyk var p tex var t end intro end text end unicode text end bracket ]" intro * index * pyk * tex * end intro} % \index{intro * index * pyk * tex * end intro "[ bracket unicode start of text text intro var x index var i pyk var p tex var t end intro end text end unicode text end bracket ]"}% % \tex{"[ math tex define intro var x index var i pyk var p tex var t end intro as "\index{#2.: #3. @#2.: $[#1/tex name/tex.]$ #3.}% \index{#3. $[#1/tex name/tex.]$}% \tex{ $[#1/tex name/tex. \stackrel {\mathrm {tex}}{=} #4/tex name. ]$}$[ #1/tex name/tex.% ]$\footnote{$[#1/tex name/tex. \stackrel {\mathrm {pyk}}{=} #3/tex name. ]$}" end define end math ]"}% % \tex{"[ math tex name define intro var x index var i pyk var p tex var t end intro as " intro(#1. ,#2. ,#3. ,#4. )" end define end math ]"}% % \display{"[ math macro define intro var x index var i pyk var p tex var t end intro as pyk define var x as var p end define then tex define var x as var t end define end define end math ]"% % \footnote{"[ math pyk define intro var x index var i pyk var p tex var t end intro as "intro * index * pyk * tex * end intro" end define end math ]"}} % \index{intro: intro * pyk * tex * end intro @intro: "[ bracket unicode start of text text intro var x pyk var p tex var t end intro end text end unicode text end bracket ]" intro * pyk * tex * end intro} % \index{intro * pyk * tex * end intro "[ bracket unicode start of text text intro var x pyk var p tex var t end intro end text end unicode text end bracket ]"}% % \tex{"[ math tex define intro var x pyk var p tex var t end intro as "\index{\alpha #2. @\back \makebox[20mm][l]{$[#1/tex name/tex.]$}#2.}% \index{#2. $[#1/tex name/tex.]$}% \tex{ $[#1/tex name/tex. \stackrel {\mathrm {tex}}{=} #3/tex name. ]$}$[ #1/tex name/tex.% ]$\footnote{$[#1/tex name/tex. \stackrel {\mathrm {pyk}}{=} #2/tex name. ]$}" end define end math ]"}% % \tex{"[ math tex name define intro var x pyk var p tex var t end intro as " intro(#1. ,#2. ,#3. )" end define end math ]"}% % \display{"[ math macro define intro var x pyk var p tex var t end intro as pyk define var x as var p end define then tex define var x as var t end define end define end math ]"% % \footnote{"[ math pyk define intro var x pyk var p tex var t end intro as "intro * pyk * tex * end intro" end define end math ]"}} \subsection{The constructs of Peano arithmetic} Terms of Peano arithmetic are constructed from zero "[ intro peano zero pyk "peano zero" tex " \dot{0}" end intro ]", successor "[ intro var x peano succ pyk "* peano succ" tex "#1. '" end intro ]", plus "[ intro var x peano plus var y pyk "* peano plus *" tex "#1. \mathop{\dot{+}} #2." end intro ]", and times "[ intro var x peano times var y pyk "* peano times *" tex "#1. \mathop{\dot{\cdot}} #2." end intro ]". Formulas of Peano arithmeric are constructed from equality "[ intro var x peano is var y pyk "* peano is *" tex "#1. \stackrel{p}{=} #2." end intro ]", negation "[ intro peano not var x pyk "peano not *" tex " \dot{\neg}\, #1." end intro ]", implication "[ intro var x peano imply var y pyk "* peano imply *" tex "#1. \mathrel{\dot{\Rightarrow}} #2." end intro ]", and universal quantification "[ intro peano all var x indeed var y pyk "peano all * indeed *" tex " \dot{\forall} #1. \colon #2." end intro ]". From these constructs we macro define one "[ intro peano one pyk "peano one" tex " \dot{1}" end intro ]", two "[ intro peano two pyk "peano two" tex " \dot{2}" end intro ]", conjunction "[ intro var x peano and var y pyk "* peano and *" tex "#1. \mathrel{\dot{\wedge}} #2." end intro ]", disjunction "[ intro var x peano or var y pyk "* peano or *" tex "#1. \mathrel{\dot{\vee}} #2." end intro ]", biimplication "[ intro var x peano iff var y pyk "* peano iff *" tex "#1. \mathrel{\dot{\Leftrightarrow}} #2." end intro ]", and existential quantification "[ intro peano exist var x indeed var y pyk "peano exist * indeed *" tex " \dot{\exists} #1. \colon #2." end intro ]": \display{"[ math macro define peano one as peano zero peano succ end define end math ]"} \display{"[ math macro define peano two as peano one peano succ end define end math ]"} \display{"[ math macro define var x peano and var y as peano not parenthesis var x peano imply peano not var y end parenthesis end define end math ]"} \display{"[ math macro define var x peano or var y as peano not var x peano imply var y end define end math ]"} \display{"[ math macro define var x peano iff var y as parenthesis var x peano imply var y end parenthesis peano and parenthesis var y peano imply var x end parenthesis end define end math ]"} \display{"[ math macro define peano exist var x indeed var y as peano not peano all var x indeed peano not var y end define end math ]"} \subsection{Variables} We now introduce the unary operator "[ intro var x peano var pyk "* peano var" tex " \dot{#1. }" end intro ]" and define that a term is a \index{variable, Peano}\indexintro{Peano variable} (i.e.\ a variable of Peano arithmetic) if it has the "[ bracket var x peano var end bracket ]" operator in its root. "[ intro var x is peano var pyk "* is peano var" tex "#1. {} ^ {\cal P}" end intro ]" is true if "[ bracket var x end bracket ]" is a Peano variable: \display{"[ math value define var x is peano var as var x term root equal quote var x peano var end quote end define end math ]"} We macro define "[ intro peano a pyk "peano a" tex " \dot{\mathit{a}}" end intro ]" to be a Peano variable: \display{"[ math macro define peano a as var a peano var end define end math ]"}% % \test{"[ math test quote peano a end quote is peano var end test end math ]"}% % \test{"[ math false test quote var a end quote is peano var end test end math ]"} Appendix \ref{section:VariablesOfPeanoArithmetic} defines Peano variables for the other letters of the English alphabet. "[ intro peano nonfree var x in var y end nonfree pyk "peano nonfree * in * end nonfree" tex " \dot{nonfree}(#1. ,#2. )" end intro ]" is true if the Peano variable "[ bracket var x end bracket ]" does not occur free in the Peano term/formula "[ bracket var y end bracket ]". "[ intro peano nonfree star var x in var y end nonfree pyk "peano nonfree star * in * end nonfree" tex " \dot{nonfree}^*(#1. ,#2. )" end intro ]" is true if the Peano variable "[ bracket var x end bracket ]" does not occur free in the list "[ bracket var y end bracket ]" of Peano terms/formulas. \display{"[ math value define peano nonfree var x in var y end nonfree as newline open if var y is peano var then not var x term equal var y else newline open if not var y term root equal quote peano all var x indeed var y end quote then peano nonfree star var x in var y tail end nonfree else newline open if var x term equal var y first then true else peano nonfree var x in var y second end nonfree end define end math ]"} \display{"[ math value define peano nonfree star var x in var y end nonfree as var x tagged guard tagged if var y then true else peano nonfree var x in var y head end nonfree macro and peano nonfree star var x in var y tail end nonfree end if end define end math ]"}% % \test{"[ math test peano nonfree quote peano x end quote in quote peano y peano is peano z peano imply peano all peano x indeed peano x peano is peano y end quote end nonfree end test end math ]"}% % \test{"[ math false test peano nonfree quote peano x end quote in quote peano x peano is peano z peano imply peano all peano x indeed peano x peano is peano y end quote end nonfree end test end math ]"}% % \test{"[ math false test peano nonfree quote peano x end quote in quote peano y peano is peano x peano imply peano all peano x indeed peano x peano is peano y end quote end nonfree end test end math ]"}% % \test{"[ math false test peano nonfree quote peano x end quote in quote peano y peano is peano z peano imply peano all peano y indeed peano x peano is peano y end quote end nonfree end test end math ]"}% "[ intro peano free var a set var x to var b end free pyk "peano free * set * to * end free" tex " \dot{free}\langle #1. | #2. := #3. \rangle" end intro ]" is true if the substitution "[ bracket substitute var a set var x to var b end substitute end bracket ]" is free. "[ intro peano free star var a set var x to var b end free pyk "peano free star * set * to * end free" tex " \dot{free}{}^*\langle #1. | #2. := #3. \rangle" end intro ]" is the version where "[ bracket var a end bracket ]" is a list of terms. \display{"[ math value define peano free var a set var x to var b end free as var x tagged guard var b tagged guard newline open if var a is peano var then true else newline open if not var a term root equal quote peano all var u indeed var v end quote then peano free star var a tail set var x to var b end free else newline open if var a first term equal var x then true else newline open if peano nonfree var x in var a second end nonfree then true else newline open if not peano nonfree var a first in var b end nonfree then false else newline peano free var a second set var x to var b end free end define end math ]"} \display{"[ math value define peano free star var a set var x to var b end free as var x tagged guard var b tagged guard tagged if var a then true else peano free var a head set var x to var b end free macro and peano free star var a tail set var x to var b end free end if end define end math ]"}% % \test{"[ math test peano free quote peano all peano x indeed var b pair peano x pair var c end quote set quote peano x end quote to quote var x pair peano y pair var z end quote end free end test end math ]"}% % \test{"[ math false test peano free quote peano all peano y indeed var b pair peano x pair var c end quote set quote peano x end quote to quote var x pair peano y pair var z end quote end free end test end math ]"}% % \test{"[ math test peano free quote peano all peano x indeed var b pair peano x pair var c end quote set quote peano y end quote to quote var x pair peano y pair var z end quote end free end test end math ]"}% % \test{"[ math test peano free quote peano all peano y indeed var b pair peano x pair var c end quote set quote peano y end quote to quote var x pair peano y pair var z end quote end free end test end math ]"}% % "[ intro peano sub var a is var b where var x is var c end sub pyk "peano sub * is * where * is * end sub" tex "#1. {\equiv}\langle #2. |#3. :=#4. \rangle" end intro ]" is true if "[ bracket var a end bracket ]" equals "[ bracket substitute var b set var x to var c end substitute end bracket ]". "[ intro peano sub star var a is var b where var x is var c end sub pyk "peano sub star * is * where * is * end sub" tex "#1. {\equiv}\langle^* #2. |#3. :=#4. \rangle" end intro ]" is the version where "[ bracket var a end bracket ]" and "[ bracket var b end bracket ]" are lists. \display{"[ math value define peano sub var a is var b where var x is var c end sub as var a tagged guard var x tagged guard var c tagged guard newline open if var b term root equal quote peano all var u indeed var v end quote macro and var b first term equal var x then var a term equal var b else newline open if var b is peano var and var b term equal var x then var a term equal var c else newline var a term root equal var b macro and peano sub star var a tail is var b tail where var x is var c end sub end define end math ]"} \display{"[ math value define peano sub star var a is var b where var x is var c end sub as var b tagged guard var x tagged guard var c tagged guard tagged if var a then true else peano sub var a head is var b head where var x is var c end sub macro and peano sub star var a tail is var b tail where var x is var c end sub end if end define end math ]"}% % \test{"[ math test peano sub peano a is peano a where peano b is peano c end sub end test end math ]"}% % \test{"[ math test peano sub peano c is peano b where peano b is peano c end sub end test end math ]"}% % \test{"[ math test peano sub all peano a indeed peano a peano is peano b is all peano a indeed peano a peano is peano b where peano a is peano c end sub end test end math ]"}% % \test{"[ math test peano sub all peano a indeed peano a peano is peano c is all peano a indeed peano a peano is peano b where peano b is peano c end sub end test end math ]"}% % \test{"[ math test peano sub peano all peano a indeed peano a peano is peano zero peano plus peano a peano imply peano c peano times peano d peano is peano zero peano plus peano c peano times peano d is peano all peano a indeed peano a peano is peano zero peano plus peano a peano imply peano b peano is peano zero peano plus peano b where peano b is peano c peano times peano d end sub end test end math ]"}% % \test{"[ math test peano sub peano all peano a indeed peano a peano is peano zero peano plus peano a peano imply peano b peano is peano zero peano plus peano b is peano all peano a indeed peano a peano is peano zero peano plus peano a peano imply peano b peano is peano zero peano plus peano b where peano a is peano c end sub end test end math ]"}% % \subsection{Axiomatic system} System "[ intro system s pyk "system s" tex " S" end intro ]" of Mendelson \cite{mendelson} expresses Peano arithmetic. It comprises the axioms "[ intro axiom a one pyk "axiom a one" tex " A1" end intro ]", "[ intro axiom a two pyk "axiom a two" tex " A2" end intro ]", "[ intro axiom a three pyk "axiom a three" tex " A3" end intro ]", "[ intro axiom a four pyk "axiom a four" tex " A4" end intro ]", and "[ intro axiom a five pyk "axiom a five" tex " A5" end intro ]" and inference rules "[ intro rule mp pyk "rule mp" tex " MP" end intro ]" and "[ intro rule gen pyk "rule gen" tex " Gen" end intro ]" of first order predicate calculus. Furthermore, it comprises the proper axioms "[ intro axiom s one pyk "axiom s one" tex " S1" end intro ]", "[ intro axiom s two pyk "axiom s two" tex " S2" end intro ]", "[ intro axiom s three pyk "axiom s three" tex " S3" end intro ]", "[ intro axiom s four pyk "axiom s four" tex " S4" end intro ]", "[ intro axiom s five pyk "axiom s five" tex " S5" end intro ]", "[ intro axiom s six pyk "axiom s six" tex " S6" end intro ]", "[ intro axiom s seven pyk "axiom s seven" tex " S7" end intro ]", "[ intro axiom s eight pyk "axiom s eight" tex " S8" end intro ]", and "[ intro axiom s nine pyk "axiom s nine" tex " S9" end intro ]". System "[ bracket system s end bracket ]" is defined thus: \display{"[ math theory system s end theory end math ]"} \display{"[ math in theory system s rule axiom a one says all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end rule end math ]"} \display{"[ math in theory system s rule axiom a two says all meta a indeed all meta b indeed all meta c indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end rule end math ]"} \display{"[ math in theory system s rule axiom a three says parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end rule end math ]"} The order of quantifiers in the following axiom is such that "[ bracket meta a end bracket ]" which the system can currently guess comes first. At a later stage, when a planned generalisation of the conclusion tactic has been implemented, the system will be able to guess "[ bracket meta x end bracket ]" and "[ bracket meta b end bracket ]" also. Guessing "[ bracket meta c end bracket ]" would require a separate tactic. \display{"[ math in theory system s rule axiom a four says all meta c indeed all meta x indeed all meta b indeed all meta a indeed peano sub meta a is meta b where meta x is meta c end sub endorse peano all meta x indeed meta b peano imply meta a end rule end math ]"} \display{"[ math in theory system s rule axiom a five says all meta x indeed all meta a indeed all meta b indeed peano nonfree meta x in meta a end nonfree endorse peano all meta x indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply peano all meta x indeed meta b end rule end math ]"} \display{"[ math in theory system s rule rule mp says all meta a indeed all meta b indeed meta a peano imply meta b infer meta a infer meta b end rule end math ]"} \display{"[ math in theory system s rule rule gen says all meta x indeed all meta a indeed meta a infer peano all meta x indeed meta a end rule end math ]"} Axiom "[ bracket axiom s one end bracket ]" to "[ bracket axiom s eight end bracket ]" are stated as Mendelson \cite{mendelson} does. This is done here to test certain parts of the Logiweb system. Serious users of Peano arithmetic are advised to take Mendelson's Lemma 3.1 as axioms instead. \display{"[ math in theory system s rule axiom s one says peano a peano is peano b peano imply peano a peano is peano c peano imply peano b peano is peano c end rule end math ]"} \display{"[ math in theory system s rule axiom s two says peano a peano is peano b peano imply peano a peano succ peano is peano b peano succ end rule end math ]"} \display{"[ math in theory system s rule axiom s three says not peano zero peano is peano a peano succ end rule end math ]"} \display{"[ math in theory system s rule axiom s four says peano a peano succ peano is peano b peano succ peano imply peano a peano is peano b end rule end math ]"} \display{"[ math in theory system s rule axiom s five says peano a peano plus peano zero peano is peano a end rule end math ]"} \display{"[ math in theory system s rule axiom s six says peano a peano plus peano b peano succ peano is parenthesis peano a peano plus peano b end parenthesis peano succ end rule end math ]"} \display{"[ math in theory system s rule axiom s seven says peano a peano times peano zero peano is peano zero end rule end math ]"} \display{"[ math in theory system s rule axiom s eight says peano a peano times parenthesis peano b peano succ end parenthesis peano is parenthesis peano a peano times peano b end parenthesis peano plus peano a end rule end math ]"} \display{"[ math in theory system s rule axiom s nine says all meta a indeed all meta b indeed all meta c indeed all meta x indeed macro newline peano sub meta b is meta a where meta x is peano zero end sub endorse peano sub meta c is meta a where meta x is meta x peano succ end sub endorse macro newline meta b peano imply peano all meta x indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta x indeed meta a end rule end math ]"} \subsection{A lemma and a proof} We now prove Lemma "[ intro lemma l three two a pyk "lemma l three two a" tex " L3.2(a)" end intro ]" which is an instance of the corresponding proposition in Mendelson \cite{mendelson}: \statement{"[ math in theory system s lemma lemma l three two a says peano x peano is peano x end lemma end math ]"} The first four lines of the proof has revealed an error in the conclusion tactic which has to be corrected before the proof will be accepted: \statement{"[ math system s proof of lemma l three two a reads line ell a because axiom s five indeed peano a peano plus peano zero peano is peano a cut line ell b because rule gen modus ponens ell a indeed peano all peano a indeed peano a peano plus peano zero peano is peano a cut line ell c because axiom a four at peano x at peano a at macro newline peano a peano plus peano zero peano is peano a at macro newline peano x peano plus peano zero peano is peano x indeed peano all peano a indeed peano a peano plus peano zero peano is peano a peano imply peano x peano plus peano zero peano is peano x cut because rule mp modus ponens ell c modus ponens ell b indeed peano x peano plus peano zero peano is peano x qed end math ]"} \appendix \section{Chores} \subsection{The name of the page} This defines the name of the page: \display{"[ math pyk define peano as "peano" end define end math ]"} \subsection{Variables of Peano arithmetic}\label{section:VariablesOfPeanoArithmetic} We use "[ intro peano b pyk "peano b" tex " \dot{\mathit{b}}" end intro ]", "[ intro peano c pyk "peano c" tex " \dot{\mathit{c}}" end intro ]", "[ intro peano d pyk "peano d" tex " \dot{\mathit{d}}" end intro ]", "[ intro peano e pyk "peano e" tex " \dot{\mathit{e}}" end intro ]", "[ intro peano f pyk "peano f" tex " \dot{\mathit{f}}" end intro ]", "[ intro peano g pyk "peano g" tex " \dot{\mathit{g}}" end intro ]", "[ intro peano h pyk "peano h" tex " \dot{\mathit{h}}" end intro ]", "[ intro peano i pyk "peano i" tex " \dot{\mathit{i}}" end intro ]", "[ intro peano j pyk "peano j" tex " \dot{\mathit{j}}" end intro ]", "[ intro peano k pyk "peano k" tex " \dot{\mathit{k}}" end intro ]", "[ intro peano l pyk "peano l" tex " \dot{\mathit{l}}" end intro ]", "[ intro peano m pyk "peano m" tex " \dot{\mathit{m}}" end intro ]", "[ intro peano n pyk "peano n" tex " \dot{\mathit{n}}" end intro ]", "[ intro peano o pyk "peano o" tex " \dot{\mathit{o}}" end intro ]", "[ intro peano p pyk "peano p" tex " \dot{\mathit{p}}" end intro ]", "[ intro peano q pyk "peano q" tex " \dot{\mathit{q}}" end intro ]", "[ intro peano r pyk "peano r" tex " \dot{\mathit{r}}" end intro ]", "[ intro peano s pyk "peano s" tex " \dot{\mathit{s}}" end intro ]", "[ intro peano t pyk "peano t" tex " \dot{\mathit{t}}" end intro ]", "[ intro peano u pyk "peano u" tex " \dot{\mathit{u}}" end intro ]", "[ intro peano v pyk "peano v" tex " \dot{\mathit{v}}" end intro ]", "[ intro peano w pyk "peano w" tex " \dot{\mathit{w}}" end intro ]", "[ intro peano x pyk "peano x" tex " \dot{\mathit{x}}" end intro ]", "[ intro peano y pyk "peano y" tex " \dot{\mathit{y}}" end intro ]", and "[ intro peano z pyk "peano z" tex " \dot{\mathit{z}}" end intro ]" to denote variables of Peano arithmetic: "[ math macro define peano b as var b peano var end define end math ]", "[ math macro define peano c as var c peano var end define end math ]", "[ math macro define peano d as var d peano var end define end math ]", "[ math macro define peano e as var e peano var end define end math ]", "[ math macro define peano f as var f peano var end define end math ]", "[ math macro define peano g as var g peano var end define end math ]", "[ math macro define peano h as var h peano var end define end math ]", "[ math macro define peano i as var i peano var end define end math ]", "[ math macro define peano j as var j peano var end define end math ]", "[ math macro define peano k as var k peano var end define end math ]", "[ math macro define peano l as var l peano var end define end math ]", "[ math macro define peano m as var m peano var end define end math ]", "[ math macro define peano n as var n peano var end define end math ]", "[ math macro define peano o as var o peano var end define end math ]", "[ math macro define peano p as var p peano var end define end math ]", "[ math macro define peano q as var q peano var end define end math ]", "[ math macro define peano r as var r peano var end define end math ]", "[ math macro define peano s as var s peano var end define end math ]", "[ math macro define peano t as var t peano var end define end math ]", "[ math macro define peano u as var u peano var end define end math ]", "[ math macro define peano v as var v peano var end define end math ]", "[ math macro define peano w as var w peano var end define end math ]", "[ math macro define peano x as var x peano var end define end math ]", "[ math macro define peano y as var y peano var end define end math ]", and "[ math macro define peano z as var z peano var end define end math ]". \subsection{\TeX\ definitions}\label{section:TexDefinitions} \begin{list}{}{ \setlength{\leftmargin}{5em} \setlength{\itemindent}{-5em}} \immediate\closeout\outex \input{./page.otx} \end{list} \subsection{Test} \begin{list}{}{ \setlength{\leftmargin}{5em} \setlength{\itemindent}{-5em}} \immediate\closeout\outest \input{./page.tst} \end{list} \subsection{Priority table}\label{section:PriorityTable} "[ flush left math priority table Priority end table end math end left ]" \section{Index} \newcommand\myidxitem{\par\noindent} \renewenvironment{theindex}{\let\item\myidxitem}{} \printindex \section{Bibliography} \bibliography{./page} \end{document} End of file File page.bib @article {berline97, author = {C. Berline and K. Grue}, title = {A $\kappa$-denotational semantics for {M}ap {T}heory in {ZFC+SI}}, journal = TCS, year = {1997}, volume = {179}, number = {1--2}, pages = {137--202}, month = {jun}} @book {church41, author = {A. Church}, title = {The Calculi of Lambda-Conversion}, publisher = {Princeton University Press}, year = {1941}} @Article {godel, author = {K. G{\"!o}del}, title = {{\"!U}ber for\-mal un\-ent\-scheid\-ba\-re \mbox{S\"!at}\-ze der \mbox{Prin}\-ci\-pia \mbox{Mathe}\-ma\-ti\-ca und ver\-wand\-ter \mbox{Sys}\-teme \mbox{I}}, journal = {Mo\-nats\-hef\-te f{\"!u}r Mathe\-ma\-tik und Phy\-sik}, year = {19\-31}, volume = {12}, number = {\mbox{XXXVIII}}, pages = {173-198}} @book {Gordon79, author = {M. J. Gordon, A. J. Milner, C. P. Wadsworth}, title = {Edinburgh {LCF}, A mechanised logic of computation}, publisher = {Springer-Verlag}, year = {1979}, volume = {78}, series = {Lecture Notes in Computer Science}} @article {grue92, author = {K. Grue}, title = {Map Theory}, journal = TCS, year = {1992}, volume = {102}, number = {1}, pages = {1--133}, month = {jul}} @inproceedings{Logiweb, author = {K. Grue}, title = {Logiweb}, editor = {Fairouz Kamareddine}, booktitle = {Mathematical Knowledge Management Symposium 2003}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {93}, year = {2004}, pages = {70--101}} @article {mccarthy60, author = {J. McCarthy}, title = {Recursive functions of symbolic expressions and their computation by machine}, journal = {Communications of the ACM}, year = {1960}, pages = {184--195}} @book {mendelson, author = {E. Mendelson}, title = {Introduction to Mathematical Logic}, publisher = {Wadsworth and Brooks}, year = {1987}, edition = {3.}} @book {TeXbook, author = {D. Knuth}, title = {The TeXbook}, publisher = {Addison Wesley}, year = {1983}} End of file File page.sty % thebibliography environment from % /usr/share/texmf/tex/latex/base/book.cls % with \chapter removed \renewenvironment{thebibliography}[1] {\list{\@biblabel{\@arabic\c@enumiv}}% {\settowidth\labelwidth{\@biblabel{#1}}% \leftmargin\labelwidth \advance\leftmargin\labelsep \@openbib@code \usecounter{enumiv}% \let\p@enumiv\@empty \renewcommand\theenumiv{\@arabic\c@enumiv}}% \sloppy \clubpenalty4000 \@clubpenalty \clubpenalty \widowpenalty4000% \sfcode`\.\@m} {\def\@noitemerr {\@latex@warning{Empty `thebibliography' environment}}% \endlist} End of file latex page makeindex page bibtex page latex page makeindex page latex page"