"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
"
begin ragged right expansion
end "
\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 "
begin intro peano zero pyk "peano zero" tex "
\dot{0}" end intro
end ",
successor "
begin intro var x peano succ pyk "* peano succ" tex "#1.'" end intro
end ",
plus "
begin intro var x peano plus var y pyk "* peano plus *" tex "#1.
\mathop{\dot{+}} #2." end intro
end ", and
times "
begin intro var x peano times var y pyk "* peano times *" tex "#1.
\mathop{\dot{\cdot}} #2." end intro
end ".
Formulas of Peano arithmeric are constructed from
equality "
begin intro var x peano is var y index "p" pyk "* peano is *" tex "#1.
\stackrel{p}{=} #2." end intro
end ",
negation "
begin intro peano not var x pyk "peano not *" tex "
\dot{\neg}\, #1." end intro
end ",
implication "
begin intro var x peano imply var y pyk "* peano imply *" tex "#1.
\mathrel{\dot{\Rightarrow}} #2." end intro
end ", and
universal quantification "
begin intro peano all var x indeed var y pyk "peano all * indeed *" tex "
\dot{\forall} #1.
\colon #2." end intro
end ".
From these constructs we macro define
one "
begin intro peano one pyk "peano one" tex "
\dot{1}" end intro
end ",
two "
begin intro peano two pyk "peano two" tex "
\dot{2}" end intro
end ",
conjunction "
begin intro var x peano and var y pyk "* peano and *" tex "#1.
\mathrel{\dot{\wedge}} #2." end intro
end ",
disjunction "
begin intro var x peano or var y pyk "* peano or *" tex "#1.
\mathrel{\dot{\vee}} #2." end intro
end ",
biimplication "
begin intro var x peano iff var y pyk "* peano iff *" tex "#1.
\mathrel{\dot{\Leftrightarrow}} #2." end intro
end ", and
existential quantification "
begin intro peano exist var x indeed var y pyk "peano exist * indeed *" tex "
\dot{\exists} #1.
\colon #2." end intro
end ":
\display{"
begin math macro define peano one as peano zero peano succ end define end math
end "}
\display{"
begin math macro define peano two as peano one peano succ end define end math
end "}
\display{"
begin 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
end "}
\display{"
begin math macro define var x peano or var y as peano not var x peano imply var y end define end math
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\subsection{Variables}
We now introduce the unary operator "
begin intro var x peano var pyk "* peano var" tex "
\dot{#1.
}" end intro
end " and define that a term is a \index{variable, Peano}\indexintro{Peano variable} (i.e.\ a variable of Peano arithmetic) if it has the "
begin bracket var x peano var end bracket
end " operator in its root. "
begin intro var x is peano var index "P" pyk "* is peano var" tex "#1.
{} ^ {\cal P}" end intro
end " is true if "
begin bracket var x end bracket
end " is a Peano variable:
\display{"
begin 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
end "}
We macro define "
begin intro peano a index "a" pyk "peano a" tex "
\dot{\mathit{a}}" end intro
end " to be a Peano variable:
\display{"
begin math macro define peano a as var a peano var end define end math
end "}%
%
\test{"
begin math test quote peano a end quote is peano var end test end math
end "}%
%
\test{"
begin math false test quote var a end quote is peano var end test end math
end "}
Appendix \ref{section:VariablesOfPeanoArithmetic} defines Peano variables for the other letters of the English alphabet.
"
begin 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
end " is true if the Peano variable "
begin bracket var x end bracket
end " does not occur free in the Peano term/formula "
begin bracket var y end bracket
end ". "
begin 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
end " is true if the Peano variable "
begin bracket var x end bracket
end " does not occur free in the list "
begin bracket var y end bracket
end " of Peano terms/formulas.
\display{"
begin 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
end "}
\display{"
begin 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
end "}%
%
\test{"
begin 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
end "}%
%
\test{"
begin 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
end "}%
%
\test{"
begin 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
end "}%
%
\test{"
begin 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
end "}%
"
begin 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
end " is true if the substitution "
begin bracket substitute var a set var x to var b end substitute end bracket
end " is free. "
begin 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
end " is the version where "
begin bracket var a end bracket
end " is a list of terms.
\display{"
begin 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
end "}
\display{"
begin 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
end "}%
%
\test{"
begin 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
end "}%
%
\test{"
begin 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
end "}%
%
\test{"
begin 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
end "}%
%
\test{"
begin 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
end "}%
%
"
begin 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
end " is true if "
begin bracket var a end bracket
end " equals "
begin bracket substitute var b set var x to var c end substitute end bracket
end ". "
begin 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
end " is the version where "
begin bracket var a end bracket
end " and "
begin bracket var b end bracket
end " are lists.
\display{"
begin 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
end "}
\display{"
begin 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
end "}%
%
\test{"
begin math test peano sub peano a is peano a where peano b is peano c end sub end test end math
end "}%
%
\test{"
begin math test peano sub peano c is peano b where peano b is peano c end sub end test end math
end "}%
%
\test{"
begin 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
end "}%
%
\test{"
begin 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
end "}%
%
\test{"
begin 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
end "}%
%
\test{"
begin 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
end "}%
%
\subsection{Mendelsons system S}
System "
begin intro system s index "S" pyk "system s" tex "
S" end intro
end " of Mendelson \cite{mendelson} expresses Peano arithmetic. It comprises the axioms
"
begin intro axiom a one index "A1" pyk "axiom a one" tex "
A1" end intro
end ",
"
begin intro axiom a two index "A2" pyk "axiom a two" tex "
A2" end intro
end ",
"
begin intro axiom a three index "A3" pyk "axiom a three" tex "
A3" end intro
end ",
"
begin intro axiom a four index "A4" pyk "axiom a four" tex "
A4" end intro
end ", and
"
begin intro axiom a five index "A5" pyk "axiom a five" tex "
A5" end intro
end "
and inference rules
"
begin intro rule mp index "MP" pyk "rule mp" tex "
MP" end intro
end " and
"
begin intro rule gen index "Gen" pyk "rule gen" tex "
Gen" end intro
end "
of first order predicate calculus. Furthermore, it comprises the proper axioms
"
begin intro axiom s one index "S1" pyk "axiom s one" tex "
S1" end intro
end ",
"
begin intro axiom s two index "S2" pyk "axiom s two" tex "
S2" end intro
end ",
"
begin intro axiom s three index "S3" pyk "axiom s three" tex "
S3" end intro
end ",
"
begin intro axiom s four index "S4" pyk "axiom s four" tex "
S4" end intro
end ",
"
begin intro axiom s five index "S5" pyk "axiom s five" tex "
S5" end intro
end ",
"
begin intro axiom s six index "S6" pyk "axiom s six" tex "
S6" end intro
end ",
"
begin intro axiom s seven index "S7" pyk "axiom s seven" tex "
S7" end intro
end ",
"
begin intro axiom s eight index "S8" pyk "axiom s eight" tex "
S8" end intro
end ", and
"
begin intro axiom s nine index "S9" pyk "axiom s nine" tex "
S9" end intro
end ". System "
begin bracket system s end bracket
end " is defined thus:
\display{"
begin math theory system s end theory end math
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
The order of quantifiers in the following axiom is such that "
begin bracket meta c end bracket
end " which the current conclusion tactic cannot guess comes first. This allows to supply a value for "
begin bracket meta c end bracket
end " without having to supply values for the other meta-variables.
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
Axiom "
begin bracket axiom s one end bracket
end " to "
begin bracket axiom s eight end bracket
end " 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{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin math in theory system s rule axiom s three says not peano zero peano is peano a peano succ end rule end math
end "}
\display{"
begin 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
end "}
\display{"
begin math in theory system s rule axiom s five says peano a peano plus peano zero peano is peano a end rule end math
end "}
\display{"
begin 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
end "}
\display{"
begin math in theory system s rule axiom s seven says peano a peano times peano zero peano is peano zero end rule end math
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\subsection{A lemma and a proof}
We now prove Lemma "
begin intro lemma l three two a index "L3.2(a)" pyk "lemma l three two a" tex "
L3.2(a)" end intro
end " which is an instance of the corresponding proposition in Mendelson \cite{mendelson}:
\statement{"
begin math in theory system s lemma lemma l three two a says peano x peano is peano x end lemma end math
end "}
\statement{"
begin 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
end "}
\subsection{An alternative axiomatic system}
System "
begin intro system prime s index "S'" pyk "system prime s" tex "
S'" end intro
end " is system "
begin bracket system s end bracket
end " in which the proper axioms are taken from Lemma 3.1 in Mendelson \cite{mendelson}. It comprises the axioms
"
begin intro axiom prime a one index "A1'" pyk "axiom prime a one" tex "
A1'" end intro
end ",
"
begin intro axiom prime a two index "A2'" pyk "axiom prime a two" tex "
A2'" end intro
end ",
"
begin intro axiom prime a three index "A3'" pyk "axiom prime a three" tex "
A3'" end intro
end ",
"
begin intro axiom prime a four index "A4'" pyk "axiom prime a four" tex "
A4'" end intro
end ", and
"
begin intro axiom prime a five index "A5'" pyk "axiom prime a five" tex "
A5'" end intro
end "
and inference rules
"
begin intro rule prime mp index "MP'" pyk "rule prime mp" tex "
MP'" end intro
end " and
"
begin intro rule prime gen index "Gen'" pyk "rule prime gen" tex "
Gen'" end intro
end "
of first order predicate calculus. Furthermore, it comprises the proper axioms
"
begin intro axiom prime s one index "S1'" pyk "axiom prime s one" tex "
S1'" end intro
end ",
"
begin intro axiom prime s two index "S2'" pyk "axiom prime s two" tex "
S2'" end intro
end ",
"
begin intro axiom prime s three index "S3'" pyk "axiom prime s three" tex "
S3'" end intro
end ",
"
begin intro axiom prime s four index "S4'" pyk "axiom prime s four" tex "
S4'" end intro
end ",
"
begin intro axiom prime s five index "S5'" pyk "axiom prime s five" tex "
S5'" end intro
end ",
"
begin intro axiom prime s six index "S6'" pyk "axiom prime s six" tex "
S6'" end intro
end ",
"
begin intro axiom prime s seven index "S7'" pyk "axiom prime s seven" tex "
S7'" end intro
end ",
"
begin intro axiom prime s eight index "S8'" pyk "axiom prime s eight" tex "
S8'" end intro
end ", and
"
begin intro axiom prime s nine index "S9'" pyk "axiom prime s nine" tex "
S9'" end intro
end ".
System "
begin bracket system prime s end bracket
end " is defined thus:
\display{"
begin math theory system prime s end theory end math
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
\display{"
begin 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
end "}
Note that "
begin bracket axiom a one end bracket
end " and "
begin bracket axiom prime a one end bracket
end " are distinct. The former says "
begin bracket system s infer all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end bracket
end " and the latter says "
begin 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
end ".
\subsection{Restatement of lemma and proof}
We now prove Lemma "
begin bracket lemma l three two a end bracket
end " once again under the name of "
begin intro lemma prime l three two a index "L3.2(a)'" pyk "lemma prime l three two a" tex "
L3.2(a)'" end intro
end ":
\statement{"
begin 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
end "}
\statement{"
begin 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
end "}
\section{Formal development}
\subsection{Propositional calculus}
\subsubsection{Modus ponens}
We use "
begin intro var x macro modus ponens var y pyk "* macro modus ponens *" tex "#1.
\unrhd #2." end intro
end " as shorthand for modus ponens:
\display{"
begin 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
end "}
\subsubsection{Lemma M1.7}
Lemma "
begin intro mendelson one seven index "M1.7" pyk "mendelson one seven" tex "
M1.7" end intro
end " (i.e.\ Lemma 1.7 in Mendelson \cite{mendelson}) reads:
\statement{"
begin 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
end "}
\statement{"
begin 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
end "}
\subsubsection{Hypothetical modus ponens}
The hypothetical version "
begin intro hypothetical rule prime mp index "MP" pyk "hypothetical rule prime mp" tex "
MP'_h" end intro
end " of modus ponens "
begin math rule prime mp end math
end " has a hypothesis "
begin math meta h end math
end " on each premise and on the conclusion:
\statement{"
begin 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
end "}
\statement{"
begin 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
end "}
We use "
begin intro var x hypothetical modus ponens var y pyk "* hypothetical modus ponens *" tex "#1.
\unrhd_h #2." end intro
end " as shorthand for hypothetical modus ponens:
\display{"
begin 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
end "}
\subsubsection{Turning lemmas to hypothetical lemmas}
Lemma "
begin intro hypothesize index "hypothesize" pyk "hypothesize" tex "
Hypothesize" end intro
end " turns a lemma with no premises into one that assumes the hypothesis "
begin bracket meta h end bracket
end " to hold:
\statement{"
begin 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
end "}
\statement{"
begin 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
end "}
\subsection{First order predicate calculus}
\subsubsection{Hypothetical generalization}
The hypothetical version "
begin intro hypothetical rule prime gen index "Gen" pyk "hypothetical rule prime gen" tex "
Gen'_h" end intro
end " of generalisation "
begin math rule prime gen end math
end " has a hypothesis "
begin math meta h end math
end " on premise and conclusion:
\statement{"
begin 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
end "}
\statement{"
begin 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
end "}
\subsection{Peano arithmetic}
\subsubsection{Lemma M3.2(a)}
Lemma "
begin intro mendelson three two a index "M3.2(a)" pyk "mendelson three two a" tex "
M3.2(a)" end intro
end " and the associated hypothetical lemma "
begin intro hypothetical three two a index "M3.2(a)" pyk "hypothetical three two a" tex "
M3.2(a)_h" end intro
end " read:
\statement{"
begin 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
end "}
\statement{"
begin 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
end "}
Above we cheat in stating "
begin math mendelson three two a end math
end " 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{"
begin 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
end "}
\subsubsection{Lemma M3.2(b)}
Lemma "
begin intro hypothetical three two b index "M3.2(b)" pyk "hypothetical three two b" tex "
M3.2(b)_h" end intro
end " reads:
\statement{"
begin 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
end "}
\statement{"
begin 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
end "}
\subsubsection{Lemma M3.1(S1)}
Lemma "
begin intro hypothetical three one s one index "M3.1(S1)" pyk "hypothetical three one s one" tex "
M3.1(S1')_h" end intro
end " is the hypothetical version of Mendelson Lemma $3.1(S1')$:
\statement{"
begin 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
end "}
\subsubsection{Lemma M3.2(c)}
Lemma "
begin intro hypothetical three two c index "M3.2(c)" pyk "hypothetical three two c" tex "
M3.2(c)_h" end intro
end " is the hypothetical version of Mendelson Lemma 3.2(c) which expresses ordinary transitivity:
\statement{"
begin 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
end "}
\subsubsection{Lemma M3.1(S2)}
Lemma "
begin intro hypothetical three one s two index "M3.1(S2)" pyk "hypothetical three one s two" tex "
M3.1(S2')_h" end intro
end " is the hypothetical version of Mendelson Lemma $3.1(S2')$:
\statement{"
begin 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
end "}
\subsubsection{Lemma M3.1(S5)}
Lemma "
begin intro hypothetical three one s five index "M3.1(S5)" pyk "hypothetical three one s five" tex "
M3.1(S5')_h" end intro
end " is the hypothetical version of Mendelson Lemma $3.1(S5')$:
\statement{"
begin 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
end "}
\subsubsection{Lemma M3.1(S6)}
Lemma "
begin intro hypothetical three one s six index "M3.1(S6)" pyk "hypothetical three one s six" tex "
M3.1(S6')_h" end intro
end " is the hypothetical version of Mendelson Lemma $3.1(S6')$:
\statement{"
begin 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
end "}
\subsubsection{Lemma M3.2(f)}
Lemma "
begin intro mendelson three two f index "M3.2(f)" pyk "mendelson three two f" tex "
M3.2(f)" end intro
end " is the closure of Mendelson Lemma 3.2(f) for the concrete variable "
begin bracket peano t end bracket
end ":
\statement{"
begin 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
end "}
The proof below uses local macro definitions.
\statement{"
begin 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
end "}
\appendix
\section{Chores}
\subsection{The name of the page}
This defines the name of the page:
\display{"
begin math pyk define peano as "peano" end define end math
end "}
\subsection{Variables of Peano arithmetic}\label{section:VariablesOfPeanoArithmetic}
We use
"
begin intro peano b index "b" pyk "peano b" tex "
\dot{\mathit{b}}" end intro
end ",
"
begin intro peano c index "c" pyk "peano c" tex "
\dot{\mathit{c}}" end intro
end ",
"
begin intro peano d index "d" pyk "peano d" tex "
\dot{\mathit{d}}" end intro
end ",
"
begin intro peano e index "e" pyk "peano e" tex "
\dot{\mathit{e}}" end intro
end ",
"
begin intro peano f index "f" pyk "peano f" tex "
\dot{\mathit{f}}" end intro
end ",
"
begin intro peano g index "g" pyk "peano g" tex "
\dot{\mathit{g}}" end intro
end ",
"
begin intro peano h index "h" pyk "peano h" tex "
\dot{\mathit{h}}" end intro
end ",
"
begin intro peano i index "i" pyk "peano i" tex "
\dot{\mathit{i}}" end intro
end ",
"
begin intro peano j index "j" pyk "peano j" tex "
\dot{\mathit{j}}" end intro
end ",
"
begin intro peano k index "k" pyk "peano k" tex "
\dot{\mathit{k}}" end intro
end ",
"
begin intro peano l index "l" pyk "peano l" tex "
\dot{\mathit{l}}" end intro
end ",
"
begin intro peano m index "m" pyk "peano m" tex "
\dot{\mathit{m}}" end intro
end ",
"
begin intro peano n index "n" pyk "peano n" tex "
\dot{\mathit{n}}" end intro
end ",
"
begin intro peano o index "o" pyk "peano o" tex "
\dot{\mathit{o}}" end intro
end ",
"
begin intro peano p index "p" pyk "peano p" tex "
\dot{\mathit{p}}" end intro
end ",
"
begin intro peano q index "q" pyk "peano q" tex "
\dot{\mathit{q}}" end intro
end ",
"
begin intro peano r index "r" pyk "peano r" tex "
\dot{\mathit{r}}" end intro
end ",
"
begin intro peano s index "s" pyk "peano s" tex "
\dot{\mathit{s}}" end intro
end ",
"
begin intro peano t index "t" pyk "peano t" tex "
\dot{\mathit{t}}" end intro
end ",
"
begin intro peano u index "u" pyk "peano u" tex "
\dot{\mathit{u}}" end intro
end ",
"
begin intro peano v index "v" pyk "peano v" tex "
\dot{\mathit{v}}" end intro
end ",
"
begin intro peano w index "w" pyk "peano w" tex "
\dot{\mathit{w}}" end intro
end ",
"
begin intro peano x index "x" pyk "peano x" tex "
\dot{\mathit{x}}" end intro
end ",
"
begin intro peano y index "y" pyk "peano y" tex "
\dot{\mathit{y}}" end intro
end ", and
"
begin intro peano z index "z" pyk "peano z" tex "
\dot{\mathit{z}}" end intro
end " to denote variables of Peano arithmetic:
"
begin math macro define peano b as var b peano var end define end math
end ",
"
begin math macro define peano c as var c peano var end define end math
end ",
"
begin math macro define peano d as var d peano var end define end math
end ",
"
begin math macro define peano e as var e peano var end define end math
end ",
"
begin math macro define peano f as var f peano var end define end math
end ",
"
begin math macro define peano g as var g peano var end define end math
end ",
"
begin math macro define peano h as var h peano var end define end math
end ",
"
begin math macro define peano i as var i peano var end define end math
end ",
"
begin math macro define peano j as var j peano var end define end math
end ",
"
begin math macro define peano k as var k peano var end define end math
end ",
"
begin math macro define peano l as var l peano var end define end math
end ",
"
begin math macro define peano m as var m peano var end define end math
end ",
"
begin math macro define peano n as var n peano var end define end math
end ",
"
begin math macro define peano o as var o peano var end define end math
end ",
"
begin math macro define peano p as var p peano var end define end math
end ",
"
begin math macro define peano q as var q peano var end define end math
end ",
"
begin math macro define peano r as var r peano var end define end math
end ",
"
begin math macro define peano s as var s peano var end define end math
end ",
"
begin math macro define peano t as var t peano var end define end math
end ",
"
begin math macro define peano u as var u peano var end define end math
end ",
"
begin math macro define peano v as var v peano var end define end math
end ",
"
begin math macro define peano w as var w peano var end define end math
end ",
"
begin math macro define peano x as var x peano var end define end math
end ",
"
begin math macro define peano y as var y peano var end define end math
end ", and
"
begin math macro define peano z as var z peano var end define end math
end ".
\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}
"
begin flush left math priority table preassociative priority peano equal priority base equal priority bracket x end bracket equal priority big bracket x end bracket equal priority math x end math equal priority flush left x end left equal priority var x equal priority var y equal priority var z equal priority proclaim x as x end proclaim equal priority define x of x as x end define equal priority pyk equal priority tex equal priority tex name equal priority priority equal priority x equal priority true equal priority if x then x else x end if equal priority introduce x of x as x end introduce equal priority value equal priority claim equal priority bottom equal priority function f of x end function equal priority identity x end identity equal priority false equal priority untagged zero equal priority untagged one equal priority untagged two equal priority untagged three equal priority untagged four equal priority untagged five equal priority untagged six equal priority untagged seven equal priority untagged eight equal priority untagged nine equal priority zero equal priority one equal priority two equal priority three equal priority four equal priority five equal priority six equal priority seven equal priority eight equal priority nine equal priority var a equal priority var b equal priority var c equal priority var d equal priority var e equal priority var f equal priority var g equal priority var h equal priority var i equal priority var j equal priority var k equal priority var l equal priority var m equal priority var n equal priority var o equal priority var p equal priority var q equal priority var r equal priority var s equal priority var t equal priority var u equal priority var v equal priority var w equal priority tagged parenthesis x end tagged equal priority tagged if x then x else x end if equal priority array x is x end array equal priority left equal priority center equal priority right equal priority empty equal priority substitute x set x to x end substitute equal priority map tag x end tag equal priority raw map untag x end untag equal priority map untag x end untag equal priority normalizing untag x end untag equal priority apply x to x end apply equal priority apply one x to x end apply equal priority identifier x end identifier equal priority identifier one x plus id x end identifier equal priority array plus x and x end plus equal priority array remove x array x level x end remove equal priority array put x value x array x level x end put equal priority array add x value x index x value x level x end add equal priority bit x of x end bit equal priority bit one x of x end bit equal priority example rack equal priority vector hook equal priority bibliography hook equal priority dictionary hook equal priority body hook equal priority codex hook equal priority expansion hook equal priority code hook equal priority cache hook equal priority diagnose hook equal priority pyk aspect equal priority tex aspect equal priority texname aspect equal priority value aspect equal priority message aspect equal priority macro aspect equal priority definition aspect equal priority unpack aspect equal priority claim aspect equal priority priority aspect equal priority lambda identifier equal priority apply identifier equal priority true identifier equal priority if identifier equal priority quote identifier equal priority proclaim identifier equal priority define identifier equal priority introduce identifier equal priority hide identifier equal priority pre identifier equal priority post identifier equal priority eval x stack x cache x end eval equal priority eval two x ref x id x stack x cache x end eval equal priority eval three x function x stack x cache x end eval equal priority eval four x arguments x stack x cache x end eval equal priority lookup x stack x default x end lookup equal priority abstract x term x stack x cache x end abstract equal priority quote x end quote equal priority expand x state x cache x end expand equal priority expand two x definition x state x cache x end expand equal priority expand list x state x cache x end expand equal priority macro equal priority macro state equal priority zip x with x end zip equal priority assoc one x address x index x end assoc equal priority protect x end protect equal priority self equal priority macro define x as x end define equal priority value define x as x end define equal priority intro define x as x end define equal priority pyk define x as x end define equal priority tex define x as x end define equal priority tex name define x as x end define equal priority priority table x end table equal priority macro define one equal priority macro define two x end define equal priority macro define three x end define equal priority macro define four x state x cache x definition x end define equal priority state expand x state x cache x end expand equal priority quote expand x term x stack x end expand equal priority quote expand two x term x stack x end expand equal priority quote expand three x term x stack x value x end expand equal priority quote expand star x term x stack x end expand equal priority parenthesis x end parenthesis equal priority aspect x subcodex x end aspect equal priority aspect x term x cache x end aspect equal priority tuple x end tuple equal priority tuple one x end tuple equal priority tuple two x end tuple equal priority let two x apply x end let equal priority let one x apply x end let equal priority claim define x as x end define equal priority checker equal priority check x cache x end check equal priority check two x cache x def x end check equal priority check three x cache x def x end check equal priority check list x cache x end check equal priority check list two x cache x value x end check equal priority test x end test equal priority false test x end test equal priority raw test x end test equal priority message equal priority message define x as x end define equal priority the statement aspect equal priority statement equal priority statement define x as x end define equal priority example axiom equal priority example scheme equal priority example rule equal priority absurdity equal priority contraexample equal priority example theory primed equal priority example lemma equal priority metavar x end metavar equal priority meta a equal priority meta b equal priority meta c equal priority meta d equal priority meta e equal priority meta f equal priority meta g equal priority meta h equal priority meta i equal priority meta j equal priority meta k equal priority meta l equal priority meta m equal priority meta n equal priority meta o equal priority meta p equal priority meta q equal priority meta r equal priority meta s equal priority meta t equal priority meta u equal priority meta v equal priority meta w equal priority meta x equal priority meta y equal priority meta z equal priority sub x set x to x end sub equal priority sub star x set x to x end sub equal priority the empty set equal priority example remainder equal priority make visible x end visible equal priority intro x index x pyk x tex x end intro equal priority intro x pyk x tex x end intro equal priority error x term x end error equal priority error two x term x end error equal priority proof x term x cache x end proof equal priority proof two x term x end proof equal priority sequent eval x term x end eval equal priority seqeval init x term x end eval equal priority seqeval modus x term x end eval equal priority seqeval modus one x term x sequent x end eval equal priority seqeval verify x term x end eval equal priority seqeval verify one x term x sequent x end eval equal priority sequent eval plus x term x end eval equal priority seqeval plus one x term x sequent x end eval equal priority seqeval minus x term x end eval equal priority seqeval minus one x term x sequent x end eval equal priority seqeval deref x term x end eval equal priority seqeval deref one x term x sequent x end eval equal priority seqeval deref two x term x sequent x def x end eval equal priority seqeval at x term x end eval equal priority seqeval at one x term x sequent x end eval equal priority seqeval infer x term x end eval equal priority seqeval infer one x term x premise x sequent x end eval equal priority seqeval endorse x term x end eval equal priority seqeval endorse one x term x side x sequent x end eval equal priority seqeval est x term x end eval equal priority seqeval est one x term x name x sequent x end eval equal priority seqeval est two x term x name x sequent x def x end eval equal priority seqeval all x term x end eval equal priority seqeval all one x term x variable x sequent x end eval equal priority seqeval cut x term x end eval equal priority seqeval cut one x term x forerunner x end eval equal priority seqeval cut two x term x forerunner x sequent x end eval equal priority computably true x end true equal priority claims x cache x ref x end claims equal priority claims two x cache x ref x end claims equal priority the proof aspect equal priority proof equal priority lemma x says x end lemma equal priority proof of x reads x end proof equal priority in theory x lemma x says x end lemma equal priority in theory x antilemma x says x end antilemma equal priority in theory x rule x says x end rule equal priority in theory x antirule x says x end antirule equal priority verifier equal priority verify one x end verify equal priority verify two x proofs x end verify equal priority verify three x ref x sequents x diagnose x end verify equal priority verify four x premises x end verify equal priority verify five x ref x array x sequents x end verify equal priority verify six x ref x list x sequents x end verify equal priority verify seven x ref x id x sequents x end verify equal priority cut x and x end cut equal priority head x end head equal priority tail x end tail equal priority rule one x theory x end rule equal priority rule x subcodex x end rule equal priority rule tactic equal priority plus x and x end plus equal priority theory x end theory equal priority theory two x cache x end theory equal priority theory three x name x end theory equal priority theory four x name x sum x end theory equal priority example axiom lemma primed equal priority example scheme lemma primed equal priority example rule lemma primed equal priority contraexample lemma primed equal priority example axiom lemma equal priority example scheme lemma equal priority example rule lemma equal priority contraexample lemma equal priority example theory equal priority ragged right equal priority ragged right expansion equal priority parameter term x stack x seed x end parameter equal priority parameter term star x stack x seed x end parameter equal priority instantiate x with x end instantiate equal priority instantiate star x with x end instantiate equal priority occur x in x substitution x end occur equal priority occur star x in x substitution x end occur equal priority unify x with x substitution x end unify equal priority unify star x with x substitution x end unify equal priority unify two x with x substitution x end unify equal priority ell a equal priority ell b equal priority ell c equal priority ell d equal priority ell e equal priority ell f equal priority ell g equal priority ell h equal priority ell i equal priority ell j equal priority ell k equal priority ell l equal priority ell m equal priority ell n equal priority ell o equal priority ell p equal priority ell q equal priority ell r equal priority ell s equal priority ell t equal priority ell u equal priority ell v equal priority ell w equal priority ell x equal priority ell y equal priority ell z equal priority ell big a equal priority ell big b equal priority ell big c equal priority ell big d equal priority ell big e equal priority ell big f equal priority ell big g equal priority ell big h equal priority ell big i equal priority ell big j equal priority ell big k equal priority ell big l equal priority ell big m equal priority ell big n equal priority ell big o equal priority ell big p equal priority ell big q equal priority ell big r equal priority ell big s equal priority ell big t equal priority ell big u equal priority ell big v equal priority ell big w equal priority ell big x equal priority ell big y equal priority ell big z equal priority ell dummy equal priority sequent reflexivity equal priority tactic reflexivity equal priority sequent commutativity equal priority tactic commutativity equal priority the tactic aspect equal priority tactic equal priority tactic define x as x end define equal priority proof expand x state x cache x end expand equal priority proof expand list x state x cache x end expand equal priority proof state equal priority conclude one x cache x end conclude equal priority conclude two x proves x cache x end conclude equal priority conclude three x proves x lemma x substitution x end conclude equal priority conclude four x lemma x end conclude equal priority peano zero equal priority peano one equal priority peano two equal priority peano a equal priority peano b equal priority peano c equal priority peano d equal priority peano e equal priority peano f equal priority peano g equal priority peano h equal priority peano i equal priority peano j equal priority peano k equal priority peano l equal priority peano m equal priority peano n equal priority peano o equal priority peano p equal priority peano q equal priority peano r equal priority peano s equal priority peano t equal priority peano u equal priority peano v equal priority peano w equal priority peano x equal priority peano y equal priority peano z equal priority peano nonfree x in x end nonfree equal priority peano nonfree star x in x end nonfree equal priority peano free x set x to x end free equal priority peano free star x set x to x end free equal priority peano sub x is x where x is x end sub equal priority peano sub star x is x where x is x end sub equal priority system s equal priority axiom a one equal priority axiom a two equal priority axiom a three equal priority axiom a four equal priority axiom a five equal priority axiom s one equal priority axiom s two equal priority axiom s three equal priority axiom s four equal priority axiom s five equal priority axiom s six equal priority axiom s seven equal priority axiom s eight equal priority axiom s nine equal priority rule mp equal priority rule gen equal priority lemma l three two a equal priority system prime s equal priority axiom prime a one equal priority axiom prime a two equal priority axiom prime a three equal priority axiom prime a four equal priority axiom prime a five equal priority axiom prime s one equal priority axiom prime s two equal priority axiom prime s three equal priority axiom prime s four equal priority axiom prime s five equal priority axiom prime s six equal priority axiom prime s seven equal priority axiom prime s eight equal priority axiom prime s nine equal priority rule prime mp equal priority rule prime gen equal priority lemma prime l three two a equal priority mendelson one seven equal priority hypothetical rule prime mp equal priority hypothesize equal priority hypothetical rule prime gen equal priority mendelson three two a equal priority hypothetical three two a equal priority hypothetical three two b equal priority hypothetical three one s one equal priority hypothetical three two c equal priority hypothetical three one s two equal priority hypothetical three one s five equal priority hypothetical three one s six equal priority mendelson three two f end priority greater than preassociative priority x sub x end sub equal priority x prime equal priority x assoc x end assoc equal priority x set x to x end set equal priority x set multi x to x end set equal priority x peano var end priority greater than preassociative priority unicode start of text x end unicode text equal priority unicode end of text equal priority text x end text equal priority text x plus x equal priority text x plus indent x equal priority
unicode newline x equal priority unicode space x equal priority unicode exclamation mark x equal priority unicode quotation mark x equal priority unicode number sign x equal priority unicode dollar sign x equal priority unicode percent x equal priority unicode ampersand x equal priority unicode apostrophe x equal priority unicode left parenthesis x equal priority unicode right parenthesis x equal priority unicode asterisk x equal priority unicode plus sign x equal priority unicode comma x equal priority unicode hyphen x equal priority unicode period x equal priority unicode slash x equal priority unicode zero x equal priority unicode one x equal priority unicode two x equal priority unicode three x equal priority unicode four x equal priority unicode five x equal priority unicode six x equal priority unicode seven x equal priority unicode eight x equal priority unicode nine x equal priority unicode colon x equal priority unicode semicolon x equal priority unicode less than x equal priority unicode equal sign x equal priority unicode greater than x equal priority unicode question mark x equal priority unicode commercial at x equal priority unicode capital a x equal priority unicode capital b x equal priority unicode capital c x equal priority unicode capital d x equal priority unicode capital e x equal priority unicode capital f x equal priority unicode capital g x equal priority unicode capital h x equal priority unicode capital i x equal priority unicode capital j x equal priority unicode capital k x equal priority unicode capital l x equal priority unicode capital m x equal priority unicode capital n x equal priority unicode capital o x equal priority unicode capital p x equal priority unicode capital q x equal priority unicode capital r x equal priority unicode capital s x equal priority unicode capital t x equal priority unicode capital u x equal priority unicode capital v x equal priority unicode capital w x equal priority unicode capital x x equal priority unicode capital y x equal priority unicode capital z x equal priority unicode left bracket x equal priority unicode backslash x equal priority unicode right bracket x equal priority unicode circumflex x equal priority unicode underscore x equal priority unicode grave accent x equal priority unicode small a x equal priority unicode small b x equal priority unicode small c x equal priority unicode small d x equal priority unicode small e x equal priority unicode small f x equal priority unicode small g x equal priority unicode small h x equal priority unicode small i x equal priority unicode small j x equal priority unicode small k x equal priority unicode small l x equal priority unicode small m x equal priority unicode small n x equal priority unicode small o x equal priority unicode small p x equal priority unicode small q x equal priority unicode small r x equal priority unicode small s x equal priority unicode small t x equal priority unicode small u x equal priority unicode small v x equal priority unicode small w x equal priority unicode small x x equal priority unicode small y x equal priority unicode small z x equal priority unicode left brace x equal priority unicode vertical line x equal priority unicode right brace x equal priority unicode tilde x equal priority preassociative x greater than x equal priority postassociative x greater than x equal priority priority x equal x equal priority priority x end priority equal priority newline x equal priority macro newline x end priority greater than preassociative priority x bit nil equal priority x bit one equal priority binary equal priority x color x end color equal priority x color star x end color end priority greater than preassociative priority x apply x equal priority x tagged apply x end priority greater than preassociative priority x raw head equal priority x raw tail equal priority x cardinal untag equal priority x head equal priority x tail equal priority x is singular equal priority x is cardinal equal priority x is data equal priority x is atomic equal priority x cardinal retract equal priority x tagged retract equal priority x boolean retract equal priority x ref equal priority x id equal priority x debug equal priority x root equal priority x zeroth equal priority x first equal priority x second equal priority x third equal priority x fourth equal priority x fifth equal priority x sixth equal priority x seventh equal priority x eighth equal priority x ninth equal priority x is error equal priority x is metavar equal priority x is metaclosed equal priority x is metaclosed star equal priority x peano succ end priority greater than preassociative priority x times x equal priority x times zero x equal priority x peano times x end priority greater than preassociative priority x plus x equal priority x plus zero x equal priority x plus one x equal priority x minus x equal priority x minus zero x equal priority x minus one x equal priority x peano plus x end priority greater than preassociative priority x term plus x end plus equal priority x term union x equal priority x term minus x end minus end priority greater than postassociative priority x raw pair x equal priority x eager pair x equal priority x tagged pair x equal priority x untagged double x equal priority x pair x equal priority x double x end priority greater than postassociative priority x comma x end priority greater than preassociative priority x boolean equal x equal priority x data equal x equal priority x cardinal equal x equal priority x peano equal x equal priority x tagged equal x equal priority x math equal x equal priority x reduce to x equal priority x term equal x equal priority x term list equal x equal priority x term root equal x equal priority x term in x equal priority x term subset x equal priority x term set equal x equal priority x sequent equal x equal priority x free in x equal priority x free in star x equal priority x free for x in x equal priority x free for star x in x equal priority x claim in x equal priority x less x equal priority x less zero x equal priority x less one x equal priority x peano is x equal priority x is peano var end priority greater than preassociative priority not x equal priority peano not x end priority greater than preassociative priority x and x equal priority x macro and x equal priority x simple and x equal priority x claim and x equal priority x peano and x end priority greater than preassociative priority x or x equal priority x parallel x equal priority x macro or x equal priority x peano or x end priority greater than preassociative priority peano all x indeed x equal priority peano exist x indeed x end priority greater than postassociative priority x macro imply x equal priority x peano imply x equal priority x peano iff x end priority greater than postassociative priority x guard x equal priority x tagged guard x end priority greater than preassociative priority x select x else x end select end priority greater than preassociative priority lambda x dot x equal priority tagging x equal priority open if x then x else x equal priority let x be x in x equal priority let x abbreviate x in x end priority greater than preassociative priority x init equal priority x modus equal priority x verify equal priority x curry plus equal priority x curry minus equal priority x dereference end priority greater than preassociative priority x at x equal priority x modus ponens x equal priority x modus probans x equal priority x conclude x equal priority x macro modus ponens x equal priority x hypothetical modus ponens x end priority greater than postassociative priority x infer x equal priority x endorse x equal priority x id est x end priority greater than preassociative priority all x indeed x end priority greater than postassociative priority x rule plus x end priority greater than postassociative priority x cut x end priority greater than preassociative priority x proves x end priority greater than preassociative priority x proof of x reads x equal priority line x because x indeed x end line x equal priority because x indeed x qed equal priority line x premise x end line x equal priority line x side condition x end line x equal priority arbitrary x end line x equal priority locally define x as x end line x end priority greater than postassociative priority x
then x equal priority x
begin x
end x end priority greater than preassociative priority x tab x end priority greater than preassociative priority x row
x end priority greater than unicode end of text end table end math end left
end "
\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"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,