{ 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: "http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/latest/vector/page.lgw" PREASSOCIATIVE base: bracket * end bracket, 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, system prime s, axiom prime a one, axiom prime a two, axiom prime a three, axiom prime a four, axiom prime a five, axiom prime s one, axiom prime s two, axiom prime s three, axiom prime s four, axiom prime s five, axiom prime s six, axiom prime s seven, axiom prime s eight, axiom prime s nine, rule prime mp, rule prime gen, lemma prime l three two a, mendelson one seven, hypothetical rule prime mp, hypothesize, hypothetical rule prime gen, mendelson three two a, hypothetical three two a, hypothetical three two b, hypothetical three one s one, hypothetical three two c, hypothetical three one s two, hypothetical three one s five, hypothetical three one s six, mendelson three two f 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 *, * macro modus ponens *, * hypothetical modus ponens * POSTASSOCIATIVE base: * infer * PREASSOCIATIVE base: all * indeed * POSTASSOCIATIVE base: * rule plus * POSTASSOCIATIVE base: * cut * PREASSOCIATIVE base: * proves * PREASSOCIATIVE base: locally define * as * end line * 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 {Peano arithmetic} \author {Klaus Grue} \maketitle \tableofcontents "[ ragged right expansion ]" \section{Peano arithmetic} This Logiweb page \cite{logiweb} defines Peano arithmetic. \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 index "p" 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 index "P" 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 index "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 index "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 index "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 index "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 index "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{Mendelsons system S} System "[ intro system s index "S" pyk "system s" tex " S" end intro ]" of Mendelson \cite{mendelson} expresses Peano arithmetic. It comprises the axioms "[ intro axiom a one index "A1" pyk "axiom a one" tex " A1" end intro ]", "[ intro axiom a two index "A2" pyk "axiom a two" tex " A2" end intro ]", "[ intro axiom a three index "A3" pyk "axiom a three" tex " A3" end intro ]", "[ intro axiom a four index "A4" pyk "axiom a four" tex " A4" end intro ]", and "[ intro axiom a five index "A5" pyk "axiom a five" tex " A5" end intro ]" and inference rules "[ intro rule mp index "MP" pyk "rule mp" tex " MP" end intro ]" and "[ intro rule gen index "Gen" pyk "rule gen" tex " Gen" end intro ]" of first order predicate calculus. Furthermore, it comprises the proper axioms "[ intro axiom s one index "S1" pyk "axiom s one" tex " S1" end intro ]", "[ intro axiom s two index "S2" pyk "axiom s two" tex " S2" end intro ]", "[ intro axiom s three index "S3" pyk "axiom s three" tex " S3" end intro ]", "[ intro axiom s four index "S4" pyk "axiom s four" tex " S4" end intro ]", "[ intro axiom s five index "S5" pyk "axiom s five" tex " S5" end intro ]", "[ intro axiom s six index "S6" pyk "axiom s six" tex " S6" end intro ]", "[ intro axiom s seven index "S7" pyk "axiom s seven" tex " S7" end intro ]", "[ intro axiom s eight index "S8" pyk "axiom s eight" tex " S8" end intro ]", and "[ intro axiom s nine index "S9" 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 all meta a indeed all meta b indeed 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 c end bracket ]" which the current conclusion tactic cannot guess comes first. This allows to supply a value for "[ bracket meta c end bracket ]" without having to supply values for the other meta-variables. \display{"[ math in theory system s rule axiom a four says all meta c indeed all meta a indeed all meta x indeed all meta b indeed peano sub quote meta a end quote is quote meta b end quote where quote meta x end quote is quote meta c end quote 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 index "L3.2(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 ]"} \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 end line 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 end line line ell c because axiom a four at 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 end line line ell d because rule mp modus ponens ell c modus ponens ell b indeed peano x peano plus peano zero peano is peano x end line line ell e because axiom s one indeed peano a peano is peano b peano imply peano a peano is peano c peano imply peano b peano is peano c end line line ell f because rule gen modus ponens ell e indeed peano all peano c indeed parenthesis peano a peano is peano b peano imply peano a peano is peano c peano imply peano b peano is peano c end parenthesis end line line ell g because axiom a four at peano x indeed peano all peano c indeed parenthesis peano a peano is peano b peano imply peano a peano is peano c peano imply peano b peano is peano c end parenthesis peano imply peano a peano is peano b peano imply peano a peano is peano x peano imply peano b peano is peano x end line line ell h because rule mp modus ponens ell g modus ponens ell f indeed peano a peano is peano b peano imply peano a peano is peano x peano imply peano b peano is peano x end line line ell i because rule gen modus ponens ell h indeed peano all peano b indeed parenthesis peano a peano is peano b peano imply peano a peano is peano x peano imply peano b peano is peano x end parenthesis end line line ell j because axiom a four at peano x indeed peano all peano b indeed parenthesis peano a peano is peano b peano imply peano a peano is peano x peano imply peano b peano is peano x end parenthesis peano imply peano a peano is peano x peano imply peano a peano is peano x peano imply peano x peano is peano x end line line ell k because rule mp modus ponens ell j modus ponens ell i indeed peano a peano is peano x peano imply peano a peano is peano x peano imply peano x peano is peano x end line line ell l because rule gen modus ponens ell k indeed peano all peano a indeed parenthesis peano a peano is peano x peano imply peano a peano is peano x peano imply peano x peano is peano x end parenthesis end line line ell m because axiom a four at peano x peano plus peano zero indeed peano all peano a indeed parenthesis peano a peano is peano x peano imply peano a peano is peano x peano imply peano x peano is peano x end parenthesis peano imply peano x peano plus peano zero peano is peano x peano imply peano x peano plus peano zero peano is peano x peano imply peano x peano is peano x end line line ell n because rule mp modus ponens ell m modus ponens ell l indeed peano x peano plus peano zero peano is peano x peano imply peano x peano plus peano zero peano is peano x peano imply peano x peano is peano x end line line ell o because rule mp modus ponens ell n modus ponens ell d indeed peano x peano plus peano zero peano is peano x peano imply peano x peano is peano x end line because rule mp modus ponens ell o modus ponens ell d indeed peano x peano is peano x qed end math ]"} \subsection{An alternative axiomatic system} System "[ intro system prime s index "S'" pyk "system prime s" tex " S'" end intro ]" is system "[ bracket system s end bracket ]" in which the proper axioms are taken from Lemma 3.1 in Mendelson \cite{mendelson}. It comprises the axioms "[ intro axiom prime a one index "A1'" pyk "axiom prime a one" tex " A1'" end intro ]", "[ intro axiom prime a two index "A2'" pyk "axiom prime a two" tex " A2'" end intro ]", "[ intro axiom prime a three index "A3'" pyk "axiom prime a three" tex " A3'" end intro ]", "[ intro axiom prime a four index "A4'" pyk "axiom prime a four" tex " A4'" end intro ]", and "[ intro axiom prime a five index "A5'" pyk "axiom prime a five" tex " A5'" end intro ]" and inference rules "[ intro rule prime mp index "MP'" pyk "rule prime mp" tex " MP'" end intro ]" and "[ intro rule prime gen index "Gen'" pyk "rule prime gen" tex " Gen'" end intro ]" of first order predicate calculus. Furthermore, it comprises the proper axioms "[ intro axiom prime s one index "S1'" pyk "axiom prime s one" tex " S1'" end intro ]", "[ intro axiom prime s two index "S2'" pyk "axiom prime s two" tex " S2'" end intro ]", "[ intro axiom prime s three index "S3'" pyk "axiom prime s three" tex " S3'" end intro ]", "[ intro axiom prime s four index "S4'" pyk "axiom prime s four" tex " S4'" end intro ]", "[ intro axiom prime s five index "S5'" pyk "axiom prime s five" tex " S5'" end intro ]", "[ intro axiom prime s six index "S6'" pyk "axiom prime s six" tex " S6'" end intro ]", "[ intro axiom prime s seven index "S7'" pyk "axiom prime s seven" tex " S7'" end intro ]", "[ intro axiom prime s eight index "S8'" pyk "axiom prime s eight" tex " S8'" end intro ]", and "[ intro axiom prime s nine index "S9'" pyk "axiom prime s nine" tex " S9'" end intro ]". System "[ bracket system prime s end bracket ]" is defined thus: \display{"[ math theory system prime s end theory end math ]"} \display{"[ math in theory system prime s rule axiom prime 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 prime s rule axiom prime 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 prime s rule axiom prime a three says all meta a indeed all meta b indeed 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 ]"} \display{"[ math in theory system prime s rule axiom prime a four says all meta c indeed all meta a indeed all meta x indeed all meta b indeed peano sub quote meta a end quote is quote meta b end quote where quote meta x end quote is quote meta c end quote end sub endorse peano all meta x indeed meta b peano imply meta a end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime a five says all meta x indeed all meta a indeed all meta b indeed peano nonfree quote meta x end quote in quote meta a end quote 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 prime s rule rule prime 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 prime s rule rule prime gen says all meta x indeed all meta a indeed meta a infer peano all meta x indeed meta a end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s one says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta a peano is meta c peano imply meta b peano is meta c end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s two says all meta a indeed all meta b indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s three says all meta a indeed not peano zero peano is meta a peano succ end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s four says all meta a indeed all meta b indeed meta a peano succ peano is meta b peano succ peano imply meta a peano is meta b end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s five says all meta a indeed meta a peano plus peano zero peano is meta a end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s six says all meta a indeed all meta b indeed meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s seven says all meta a indeed meta a peano times peano zero peano is peano zero end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s eight says all meta a indeed all meta b indeed meta a peano times parenthesis meta b peano succ end parenthesis peano is parenthesis meta a peano times meta b end parenthesis peano plus meta a end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime 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 ]"} Note that "[ bracket axiom a one end bracket ]" and "[ bracket axiom prime a one end bracket ]" are distinct. The former says "[ bracket system s infer all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end bracket ]" and the latter says "[ bracket system prime s infer all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end bracket ]". \subsection{Restatement of lemma and proof} We now prove Lemma "[ bracket lemma l three two a end bracket ]" once again under the name of "[ intro lemma prime l three two a index "L3.2(a)'" pyk "lemma prime l three two a" tex " L3.2(a)'" end intro ]": \statement{"[ math in theory system prime s lemma lemma prime l three two a says all meta a indeed meta a peano is meta a end lemma end math ]"} \statement{"[ math system prime s proof of lemma prime l three two a reads arbitrary meta a end line line ell b because axiom prime s five indeed meta a peano plus peano zero peano is meta a end line line ell c because axiom prime s one indeed meta a peano plus peano zero peano is meta a peano imply macro newline meta a peano plus peano zero peano is meta a peano imply meta a peano is meta a end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed meta a peano plus peano zero peano is meta a peano imply meta a peano is meta a end line because rule prime mp modus ponens ell d modus ponens ell b indeed meta a peano is meta a qed end math ]"} \section{Formal development} \subsection{Propositional calculus} \subsubsection{Modus ponens} We use "[ intro var x macro modus ponens var y pyk "* macro modus ponens *" tex "#1. \unrhd #2." end intro ]" as shorthand for modus ponens: \display{"[ math macro define var x macro modus ponens var y as rule prime mp modus ponens var x modus ponens var y end define end math ]"} \subsubsection{Lemma M1.7} Lemma "[ intro mendelson one seven index "M1.7" pyk "mendelson one seven" tex " M1.7" end intro ]" (i.e.\ Lemma 1.7 in Mendelson \cite{mendelson}) reads: \statement{"[ math in theory system prime s lemma mendelson one seven says all meta b indeed meta b peano imply meta b end lemma end math ]"} \statement{"[ math system prime s proof of mendelson one seven reads arbitrary meta b end line line ell a because axiom prime a one indeed meta b peano imply parenthesis meta b peano imply meta b end parenthesis peano imply meta b end line line ell c because axiom prime a two indeed parenthesis meta b peano imply parenthesis meta b peano imply meta b end parenthesis peano imply meta b end parenthesis peano imply macro newline parenthesis meta b peano imply meta b peano imply meta b end parenthesis peano imply meta b peano imply meta b end line line ell d because ell c macro modus ponens ell a indeed parenthesis meta b peano imply meta b peano imply meta b end parenthesis peano imply meta b peano imply meta b end line line ell b because axiom prime a one indeed meta b peano imply meta b peano imply meta b end line because ell d macro modus ponens ell b indeed meta b peano imply meta b qed end math ]"} \subsubsection{Hypothetical modus ponens} The hypothetical version "[ intro hypothetical rule prime mp index "MP" pyk "hypothetical rule prime mp" tex " MP'_h" end intro ]" of modus ponens "[ math rule prime mp end math ]" has a hypothesis "[ math meta h end math ]" on each premise and on the conclusion: \statement{"[ math in theory system prime s lemma hypothetical rule prime mp says all meta h indeed all meta a indeed all meta b indeed meta h peano imply meta a peano imply meta b infer meta h peano imply meta a infer meta h peano imply meta b end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical rule prime mp reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line line ell a premise meta h peano imply meta a peano imply meta b end line line ell b premise meta h peano imply meta a end line line ell c because axiom prime a two indeed parenthesis meta h peano imply meta a peano imply meta b end parenthesis peano imply parenthesis meta h peano imply meta a end parenthesis peano imply meta h peano imply meta b end line line ell d because ell c macro modus ponens ell a indeed parenthesis meta h peano imply meta a end parenthesis peano imply meta h peano imply meta b end line because ell d macro modus ponens ell b indeed meta h peano imply meta b qed end math ]"} We use "[ intro var x hypothetical modus ponens var y pyk "* hypothetical modus ponens *" tex "#1. \unrhd_h #2." end intro ]" as shorthand for hypothetical modus ponens: \display{"[ math macro define var x hypothetical modus ponens var y as hypothetical rule prime mp modus ponens var x modus ponens var y end define end math ]"} \subsubsection{Turning lemmas to hypothetical lemmas} Lemma "[ intro hypothesize index "hypothesize" pyk "hypothesize" tex " Hypothesize" end intro ]" turns a lemma with no premises into one that assumes the hypothesis "[ bracket meta h end bracket ]" to hold: \statement{"[ math in theory system prime s lemma hypothesize says all meta h indeed all meta a indeed meta a infer meta h peano imply meta a end lemma end math ]"} \statement{"[ math system prime s proof of hypothesize reads arbitrary meta h end line arbitrary meta a end line line ell a premise meta a end line line ell b because axiom prime a one indeed meta a peano imply meta h peano imply meta a end line because ell b macro modus ponens ell a indeed meta h peano imply meta a qed end math ]"} \subsection{First order predicate calculus} \subsubsection{Hypothetical generalization} The hypothetical version "[ intro hypothetical rule prime gen index "Gen" pyk "hypothetical rule prime gen" tex " Gen'_h" end intro ]" of generalisation "[ math rule prime gen end math ]" has a hypothesis "[ math meta h end math ]" on premise and conclusion: \statement{"[ math in theory system prime s lemma hypothetical rule prime gen says all meta h indeed all meta x indeed all meta a indeed peano nonfree quote meta x end quote in quote meta h end quote end nonfree endorse meta h peano imply meta a infer meta h peano imply peano all meta x indeed meta a end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical rule prime gen reads arbitrary meta h end line arbitrary meta x end line arbitrary meta a end line line ell a side condition peano nonfree quote meta x end quote in quote meta h end quote end nonfree end line line ell b premise meta h peano imply meta a end line line ell c because axiom prime a five modus probans ell a indeed peano all meta x indeed parenthesis meta h peano imply meta a end parenthesis peano imply meta h peano imply peano all meta x indeed meta a end line line ell d because rule prime gen modus ponens ell b indeed peano all meta x indeed parenthesis meta h peano imply meta a end parenthesis end line because ell c macro modus ponens ell d indeed meta h peano imply peano all meta x indeed meta a qed end math ]"} \subsection{Peano arithmetic} \subsubsection{Lemma M3.2(a)} Lemma "[ intro mendelson three two a index "M3.2(a)" pyk "mendelson three two a" tex " M3.2(a)" end intro ]" and the associated hypothetical lemma "[ intro hypothetical three two a index "M3.2(a)" pyk "hypothetical three two a" tex " M3.2(a)_h" end intro ]" read: \statement{"[ math in theory system prime s rule mendelson three two a says all meta t indeed meta t peano is meta t end rule end math ]"} \statement{"[ math in theory system prime s lemma hypothetical three two a says all meta h indeed all meta t indeed meta h peano imply meta t peano is meta t end lemma end math ]"} Above we cheat in stating "[ math mendelson three two a end math ]" as a rule and not as a lemma. A reasonable way to construct a large proof is to start stating everything as rules and then changing the rules to lemmas one at a time until only the rules of the theory are left. \statement{"[ math system prime s proof of hypothetical three two a reads arbitrary meta h end line arbitrary meta t end line line ell a because mendelson three two a indeed meta t peano is meta t end line because hypothesize modus ponens ell a indeed meta h peano imply meta t peano is meta t qed end math ]"} \subsubsection{Lemma M3.2(b)} Lemma "[ intro hypothetical three two b index "M3.2(b)" pyk "hypothetical three two b" tex " M3.2(b)_h" end intro ]" reads: \statement{"[ math in theory system prime s rule hypothetical three two b says all meta h indeed all meta t indeed all meta r indeed meta h peano imply meta t peano is meta r infer meta h peano imply meta r peano is meta t end rule end math ]"} \statement{"[ math system prime s proof of hypothetical three two b reads arbitrary meta h end line arbitrary meta t end line arbitrary meta r end line line ell a premise meta h peano imply meta t peano is meta r end line line ell b because axiom prime s one indeed meta t peano is meta r peano imply meta t peano is meta t peano imply meta r peano is meta t end line line ell c because hypothesize modus ponens ell b indeed meta h peano imply meta t peano is meta r peano imply meta t peano is meta t peano imply meta r peano is meta t end line line ell d because ell c hypothetical modus ponens ell a indeed meta h peano imply meta t peano is meta t peano imply meta r peano is meta t end line line ell e because hypothetical three two a indeed meta h peano imply meta t peano is meta t end line because ell d hypothetical modus ponens ell e indeed meta h peano imply meta r peano is meta t qed end math ]"} \subsubsection{Lemma M3.1(S1)} Lemma "[ intro hypothetical three one s one index "M3.1(S1)" pyk "hypothetical three one s one" tex " M3.1(S1')_h" end intro ]" is the hypothetical version of Mendelson Lemma $3.1(S1')$: \statement{"[ math in theory system prime s rule hypothetical three one s one says all meta h indeed all meta t indeed all meta r indeed all meta s indeed meta h peano imply meta t peano is meta r infer meta h peano imply meta t peano is meta s infer meta h peano imply meta r peano is meta s end rule end math ]"} \subsubsection{Lemma M3.2(c)} Lemma "[ intro hypothetical three two c index "M3.2(c)" pyk "hypothetical three two c" tex " M3.2(c)_h" end intro ]" is the hypothetical version of Mendelson Lemma 3.2(c) which expresses ordinary transitivity: \statement{"[ math in theory system prime s rule hypothetical three two c says all meta h indeed all meta t indeed all meta r indeed all meta s indeed meta h peano imply meta t peano is meta r infer meta h peano imply meta r peano is meta s infer meta h peano imply meta t peano is meta s end rule end math ]"} \subsubsection{Lemma M3.1(S2)} Lemma "[ intro hypothetical three one s two index "M3.1(S2)" pyk "hypothetical three one s two" tex " M3.1(S2')_h" end intro ]" is the hypothetical version of Mendelson Lemma $3.1(S2')$: \statement{"[ math in theory system prime s rule hypothetical three one s two says all meta h indeed all meta t indeed all meta r indeed meta h peano imply meta t peano is meta r infer meta h peano imply meta t peano succ peano is meta r peano succ end rule end math ]"} \subsubsection{Lemma M3.1(S5)} Lemma "[ intro hypothetical three one s five index "M3.1(S5)" pyk "hypothetical three one s five" tex " M3.1(S5')_h" end intro ]" is the hypothetical version of Mendelson Lemma $3.1(S5')$: \statement{"[ math in theory system prime s rule hypothetical three one s five says all meta h indeed all meta t indeed meta h peano imply meta t peano plus peano zero peano is meta t end rule end math ]"} \subsubsection{Lemma M3.1(S6)} Lemma "[ intro hypothetical three one s six index "M3.1(S6)" pyk "hypothetical three one s six" tex " M3.1(S6')_h" end intro ]" is the hypothetical version of Mendelson Lemma $3.1(S6')$: \statement{"[ math in theory system prime s rule hypothetical three one s six says all meta h indeed all meta t indeed all meta r indeed meta h peano imply meta t peano plus meta r peano succ peano is parenthesis meta t peano plus meta r end parenthesis peano succ end rule end math ]"} \subsubsection{Lemma M3.2(f)} Lemma "[ intro mendelson three two f index "M3.2(f)" pyk "mendelson three two f" tex " M3.2(f)" end intro ]" is the closure of Mendelson Lemma 3.2(f) for the concrete variable "[ bracket peano t end bracket ]": \statement{"[ math in theory system prime s lemma mendelson three two f says peano all peano t indeed peano t peano is peano zero peano plus peano t end lemma end math ]"} The proof below uses local macro definitions. \statement{"[ math system prime s proof of mendelson three two f reads locally define meta z as var x peano imply var x peano imply var x end line line ell a because axiom prime a one indeed meta z end line line ell b because hypothetical three one s five indeed meta z peano imply peano zero peano plus peano zero peano is peano zero end line line ell c because hypothetical three two b modus ponens ell b indeed meta z peano imply peano zero peano is peano zero peano plus peano zero end line line ell z because ell c macro modus ponens ell a indeed peano zero peano is peano zero peano plus peano zero end line locally define meta h as peano t peano is peano zero peano plus peano t end line line ell d because mendelson one seven indeed meta h peano imply peano t peano is peano zero peano plus peano t end line line ell e because hypothetical three one s two modus ponens ell d indeed meta h peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell f because hypothetical three one s six indeed meta h peano imply peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell g because hypothetical three two b modus ponens ell f indeed meta h peano imply parenthesis peano zero peano plus peano t end parenthesis peano succ peano is peano zero peano plus peano t peano succ end line line ell h because hypothetical three two c modus ponens ell e modus ponens ell g indeed meta h peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end line line ell i because rule prime gen modus ponens ell h indeed peano all peano t indeed parenthesis meta h peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end line line ell j because axiom prime s nine indeed peano zero peano is peano zero peano plus peano zero peano imply peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis peano imply peano all peano t indeed peano t peano is peano zero peano plus peano t end line line ell k because ell j macro modus ponens ell z indeed peano all peano t indeed parenthesis meta h peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis peano imply peano all peano t indeed peano t peano is peano zero peano plus peano t end line because ell k macro modus ponens ell i indeed peano all peano t indeed peano t peano is peano zero peano plus peano t 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 index "b" pyk "peano b" tex " \dot{\mathit{b}}" end intro ]", "[ intro peano c index "c" pyk "peano c" tex " \dot{\mathit{c}}" end intro ]", "[ intro peano d index "d" pyk "peano d" tex " \dot{\mathit{d}}" end intro ]", "[ intro peano e index "e" pyk "peano e" tex " \dot{\mathit{e}}" end intro ]", "[ intro peano f index "f" pyk "peano f" tex " \dot{\mathit{f}}" end intro ]", "[ intro peano g index "g" pyk "peano g" tex " \dot{\mathit{g}}" end intro ]", "[ intro peano h index "h" pyk "peano h" tex " \dot{\mathit{h}}" end intro ]", "[ intro peano i index "i" pyk "peano i" tex " \dot{\mathit{i}}" end intro ]", "[ intro peano j index "j" pyk "peano j" tex " \dot{\mathit{j}}" end intro ]", "[ intro peano k index "k" pyk "peano k" tex " \dot{\mathit{k}}" end intro ]", "[ intro peano l index "l" pyk "peano l" tex " \dot{\mathit{l}}" end intro ]", "[ intro peano m index "m" pyk "peano m" tex " \dot{\mathit{m}}" end intro ]", "[ intro peano n index "n" pyk "peano n" tex " \dot{\mathit{n}}" end intro ]", "[ intro peano o index "o" pyk "peano o" tex " \dot{\mathit{o}}" end intro ]", "[ intro peano p index "p" pyk "peano p" tex " \dot{\mathit{p}}" end intro ]", "[ intro peano q index "q" pyk "peano q" tex " \dot{\mathit{q}}" end intro ]", "[ intro peano r index "r" pyk "peano r" tex " \dot{\mathit{r}}" end intro ]", "[ intro peano s index "s" pyk "peano s" tex " \dot{\mathit{s}}" end intro ]", "[ intro peano t index "t" pyk "peano t" tex " \dot{\mathit{t}}" end intro ]", "[ intro peano u index "u" pyk "peano u" tex " \dot{\mathit{u}}" end intro ]", "[ intro peano v index "v" pyk "peano v" tex " \dot{\mathit{v}}" end intro ]", "[ intro peano w index "w" pyk "peano w" tex " \dot{\mathit{w}}" end intro ]", "[ intro peano x index "x" pyk "peano x" tex " \dot{\mathit{x}}" end intro ]", "[ intro peano y index "y" pyk "peano y" tex " \dot{\mathit{y}}" end intro ]", and "[ intro peano z index "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} \item \mbox{} \end{list} \subsection{Test} \begin{list}{}{ \setlength{\leftmargin}{5em} \setlength{\itemindent}{-5em}} \immediate\closeout\outest \input{./page.tst} \item \mbox{} \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"