"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
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 math define pyk of peano zero as text "peano zero" end text end define end math
then math define tex of peano zero as text "
\dot{0}" end text end define end math
end ",
successor "
begin math define pyk of var x peano succ as text "* peano succ" end text end define end math
then math define tex of var x peano succ as text "#1.'" end text end define end math
end ",
plus "
begin math define pyk of var x peano plus var y as text "* peano plus *" end text end define end math
then math define tex of var x peano plus var y as text "#1.
\mathop{\dot{+}} #2." end text end define end math
end ", and
times "
begin math define pyk of var x peano times var y as text "* peano times *" end text end define end math
then math define tex of var x peano times var y as text "#1.
\mathop{\dot{\cdot}} #2." end text end define end math
end ".
Formulas of Peano arithmeric are constructed from
equality "
begin math define pyk of var x peano is var y as text "* peano is *" end text end define end math
then math define tex of var x peano is var y as text "#1.
\stackrel{p}{=} #2." end text end define end math
end ",
negation "
begin math define pyk of peano not var x as text "peano not *" end text end define end math
then math define tex of peano not var x as text "
\dot{\neg}\, #1." end text end define end math
end ",
implication "
begin math define pyk of var x peano imply var y as text "* peano imply *" end text end define end math
then math define tex of var x peano imply var y as text "#1.
\mathrel{\dot{\Rightarrow}} #2." end text end define end math
end ", and
universal quantification "
begin math define pyk of peano all var x indeed var y as text "peano all * indeed *" end text end define end math
then math define tex of peano all var x indeed var y as text "
\dot{\forall} #1.
\colon #2." end text end define end math
end ".
From these constructs we macro define
one "
begin math define pyk of peano one as text "peano one" end text end define end math
then math define tex of peano one as text "
\dot{1}" end text end define end math
end ",
two "
begin math define pyk of peano two as text "peano two" end text end define end math
then math define tex of peano two as text "
\dot{2}" end text end define end math
end ",
conjunction "
begin math define pyk of var x peano and var y as text "* peano and *" end text end define end math
then math define tex of var x peano and var y as text "#1.
\mathrel{\dot{\wedge}} #2." end text end define end math
end ",
disjunction "
begin math define pyk of var x peano or var y as text "* peano or *" end text end define end math
then math define tex of var x peano or var y as text "#1.
\mathrel{\dot{\vee}} #2." end text end define end math
end ",
biimplication "
begin math define pyk of var x peano iff var y as text "* peano iff *" end text end define end math
then math define tex of var x peano iff var y as text "#1.
\mathrel{\dot{\Leftrightarrow}} #2." end text end define end math
end ", and
existential quantification "
begin math define pyk of peano exist var x indeed var y as text "peano exist * indeed *" end text end define end math
then math define tex of peano exist var x indeed var y as text "
\dot{\exists} #1.
\colon #2." end text end define end math
end ":
\display{"
begin math define macro of peano one as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano one as peano zero peano succ end define end quote end define end define end math
end "}
\display{"
begin math define macro of peano two as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano two as peano one peano succ end define end quote end define end define end math
end "}
\display{"
begin math define macro of var x peano and var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 quote end define end define end math
end "}
\display{"
begin math define macro of var x peano or var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x peano or var y as peano not var x peano imply var y end define end quote end define end define end math
end "}
\display{"
begin math define macro of var x peano iff var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 quote end define end define end math
end "}
\display{"
begin math define macro of peano exist var x indeed var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano exist var x indeed var y as peano not peano all var x indeed peano not var y end define end quote end define end define end math
end "}
\subsection{Variables}
We now introduce the unary operator "
begin math define pyk of var x peano var as text "* peano var" end text end define end math
then math define tex of var x peano var as text "
\dot{#1.
}" end text end define end math
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 math define pyk of var x is peano var as text "* is peano var" end text end define end math
then math define tex of var x is peano var as text "#1.
{} ^ {\cal P}" end text end define end math
end " is true if "
begin bracket var x end bracket
end " is a Peano variable:
\display{"
begin math define value of 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 math define pyk of peano a as text "peano a" end text end define end math
then math define tex of peano a as text "
\dot{\mathit{a}}" end text end define end math
end " to be a Peano variable:
\display{"
begin math define macro of peano a as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano a as var a peano var end define end quote end define end define end math
end "}%
%
\test{"
begin math test quote var a peano var 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 math define pyk of peano nonfree var x in var y end nonfree as text "peano nonfree * in * end nonfree" end text end define end math
then math define tex of peano nonfree var x in var y end nonfree as text "
\dot{nonfree}(#1.
,#2.
)" end text end define end math
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 math define pyk of peano nonfree star var x in var y end nonfree as text "peano nonfree star * in * end nonfree" end text end define end math
then math define tex of peano nonfree star var x in var y end nonfree as text "
\dot{nonfree}^*(#1.
,#2.
)" end text end define end math
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 define value of peano nonfree var x in var y end nonfree as newline tagged if var y is peano var then not var x term equal var y else newline tagged 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 tagged if var x term equal var y first then true else peano nonfree var x in var y second end nonfree end if end if end if end define end math
end "}
\display{"
begin math define value of peano nonfree star var x in var y end nonfree as var x tagged guard tagged if var y then true else tagged if peano nonfree var x in var y head end nonfree then peano nonfree star var x in var y tail end nonfree else false end if end if end define end math
end "}%
%
\test{"
begin math test peano nonfree quote var x peano var end quote in quote var y peano var peano is var z peano var peano imply peano all var x peano var indeed var x peano var peano is var y peano var end quote end nonfree end test end math
end "}%
%
\test{"
begin math false test peano nonfree quote var x peano var end quote in quote var x peano var peano is var z peano var peano imply peano all var x peano var indeed var x peano var peano is var y peano var end quote end nonfree end test end math
end "}%
%
\test{"
begin math false test peano nonfree quote var x peano var end quote in quote var y peano var peano is var x peano var peano imply peano all var x peano var indeed var x peano var peano is var y peano var end quote end nonfree end test end math
end "}%
%
\test{"
begin math false test peano nonfree quote var x peano var end quote in quote var y peano var peano is var z peano var peano imply peano all var y peano var indeed var x peano var peano is var y peano var end quote end nonfree end test end math
end "}%
"
begin math define pyk of peano free var a set var x to var b end free as text "peano free * set * to * end free" end text end define end math
then math define tex of peano free var a set var x to var b end free as text "
\dot{free}\langle #1.
| #2.
:= #3.
\rangle" end text end define end math
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 math define pyk of peano free star var a set var x to var b end free as text "peano free star * set * to * end free" end text end define end math
then math define tex of peano free star var a set var x to var b end free as text "
\dot{free}{}^*\langle #1.
| #2.
:= #3.
\rangle" end text end define end math
end " is the version where "
begin bracket var a end bracket
end " is a list of terms.
\display{"
begin math define value of peano free var a set var x to var b end free as var x tagged guard var b tagged guard newline tagged if var a is peano var then true else newline tagged 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 tagged if var a first term equal var x then true else newline tagged if peano nonfree var x in var a second end nonfree then true else newline tagged 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 if end if end if end if end if end define end math
end "}
\display{"
begin math define value of 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 tagged if peano free var a head set var x to var b end free then peano free star var a tail set var x to var b end free else false end if end if end define end math
end "}%
%
\test{"
begin math test peano free quote peano all var x peano var indeed var b pair var x peano var pair var c end quote set quote var x peano var end quote to quote var x pair var y peano var pair var z end quote end free end test end math
end "}%
%
\test{"
begin math false test peano free quote peano all var y peano var indeed var b pair var x peano var pair var c end quote set quote var x peano var end quote to quote var x pair var y peano var pair var z end quote end free end test end math
end "}%
%
\test{"
begin math test peano free quote peano all var x peano var indeed var b pair var x peano var pair var c end quote set quote var y peano var end quote to quote var x pair var y peano var pair var z end quote end free end test end math
end "}%
%
\test{"
begin math test peano free quote peano all var y peano var indeed var b pair var x peano var pair var c end quote set quote var y peano var end quote to quote var x pair var y peano var pair var z end quote end free end test end math
end "}%
%
"
begin math define pyk of peano sub var a is var b where var x is var c end sub as text "peano sub * is * where * is * end sub" end text end define end math
then math define tex of peano sub var a is var b where var x is var c end sub as text "#1.
{\equiv}\langle #2.
|#3.
:=#4.
\rangle" end text end define end math
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 math define pyk of peano sub star var a is var b where var x is var c end sub as text "peano sub star * is * where * is * end sub" end text end define end math
then math define tex of peano sub star var a is var b where var x is var c end sub as text "#1.
{\equiv}\langle^* #2.
|#3.
:=#4.
\rangle" end text end define end math
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 define value of 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 tagged if tagged if var b term root equal quote peano all var u indeed var v end quote then var b first term equal var x else false end if then var a term equal var b else newline tagged if var b is peano var and var b term equal var x then var a term equal var c else tagged if newline var a term root equal var b then peano sub star var a tail is var b tail where var x is var c end sub else false end if end if end if end define end math
end "}
\display{"
begin math define value of 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 tagged if peano sub var a head is var b head where var x is var c end sub then peano sub star var a tail is var b tail where var x is var c end sub else false end if end if end define end math
end "}%
%
\test{"
begin math test peano sub var a peano var is var a peano var where var b peano var is var c peano var end sub end test end math
end "}%
%
\test{"
begin math test peano sub var c peano var is var b peano var where var b peano var is var c peano var end sub end test end math
end "}%
%
\test{"
begin math test peano sub all var a peano var indeed var a peano var peano is var b peano var is all var a peano var indeed var a peano var peano is var b peano var where var a peano var is var c peano var end sub end test end math
end "}%
%
\test{"
begin math test peano sub all var a peano var indeed var a peano var peano is var c peano var is all var a peano var indeed var a peano var peano is var b peano var where var b peano var is var c peano var end sub end test end math
end "}%
%
\test{"
begin math test peano sub peano all var a peano var indeed var a peano var peano is peano zero peano plus var a peano var peano imply var c peano var peano times var d peano var peano is peano zero peano plus var c peano var peano times var d peano var is peano all var a peano var indeed var a peano var peano is peano zero peano plus var a peano var peano imply var b peano var peano is peano zero peano plus var b peano var where var b peano var is var c peano var peano times var d peano var end sub end test end math
end "}%
%
\test{"
begin math test peano sub peano all var a peano var indeed var a peano var peano is peano zero peano plus var a peano var peano imply var b peano var peano is peano zero peano plus var b peano var is peano all var a peano var indeed var a peano var peano is peano zero peano plus var a peano var peano imply var b peano var peano is peano zero peano plus var b peano var where var a peano var is var c peano var end sub end test end math
end "}%
%
\subsection{Mendelsons system S}
System "
begin math define pyk of system s as text "system s" end text end define end math
then math define tex of system s as text "
S" end text end define end math
end " of Mendelson \cite{mendelson} expresses Peano arithmetic. It comprises the axioms
"
begin math define pyk of axiom a one as text "axiom a one" end text end define end math
then math define tex of axiom a one as text "
A1" end text end define end math
end ",
"
begin math define pyk of axiom a two as text "axiom a two" end text end define end math
then math define tex of axiom a two as text "
A2" end text end define end math
end ",
"
begin math define pyk of axiom a three as text "axiom a three" end text end define end math
then math define tex of axiom a three as text "
A3" end text end define end math
end ",
"
begin math define pyk of axiom a four as text "axiom a four" end text end define end math
then math define tex of axiom a four as text "
A4" end text end define end math
end ", and
"
begin math define pyk of axiom a five as text "axiom a five" end text end define end math
then math define tex of axiom a five as text "
A5" end text end define end math
end "
and inference rules
"
begin math define pyk of rule mp as text "rule mp" end text end define end math
then math define tex of rule mp as text "
MP" end text end define end math
end " and
"
begin math define pyk of rule gen as text "rule gen" end text end define end math
then math define tex of rule gen as text "
Gen" end text end define end math
end "
of first order predicate calculus. Furthermore, it comprises the proper axioms
"
begin math define pyk of axiom s one as text "axiom s one" end text end define end math
then math define tex of axiom s one as text "
S1" end text end define end math
end ",
"
begin math define pyk of axiom s two as text "axiom s two" end text end define end math
then math define tex of axiom s two as text "
S2" end text end define end math
end ",
"
begin math define pyk of axiom s three as text "axiom s three" end text end define end math
then math define tex of axiom s three as text "
S3" end text end define end math
end ",
"
begin math define pyk of axiom s four as text "axiom s four" end text end define end math
then math define tex of axiom s four as text "
S4" end text end define end math
end ",
"
begin math define pyk of axiom s five as text "axiom s five" end text end define end math
then math define tex of axiom s five as text "
S5" end text end define end math
end ",
"
begin math define pyk of axiom s six as text "axiom s six" end text end define end math
then math define tex of axiom s six as text "
S6" end text end define end math
end ",
"
begin math define pyk of axiom s seven as text "axiom s seven" end text end define end math
then math define tex of axiom s seven as text "
S7" end text end define end math
end ",
"
begin math define pyk of axiom s eight as text "axiom s eight" end text end define end math
then math define tex of axiom s eight as text "
S8" end text end define end math
end ", and
"
begin math define pyk of axiom s nine as text "axiom s nine" end text end define end math
then math define tex of axiom s nine as text "
S9" end text end define end math
end ". System "
begin bracket system s end bracket
end " is defined thus:
\display{"
begin math define statement of system s as var a peano var peano plus var b peano var peano succ peano is var a peano var peano plus var b peano var peano succ rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar rule plus var a peano var peano is var b peano var peano imply var a peano var peano succ peano is var b peano var peano succ rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar rule plus var a peano var peano succ peano is var b peano var peano succ peano imply var a peano var peano is var b peano var rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar rule plus all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed peano nonfree metavar var x end metavar in metavar var a end metavar end nonfree endorse peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano all metavar var x end metavar indeed metavar var b end metavar rule plus var a peano var peano times var b peano var peano succ peano is var a peano var peano times var b peano var peano plus var a peano var rule plus var a peano var peano plus peano zero peano is var a peano var rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar rule plus var a peano var peano is var b peano var peano imply var a peano var peano is var c peano var peano imply var b peano var peano is var c peano var rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var x end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var x end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var x end metavar is metavar var x end metavar peano succ end sub endorse metavar var b end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar rule plus not peano zero peano is var a peano var peano succ rule plus all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer peano all metavar var x end metavar indeed metavar var a end metavar rule plus all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse peano all metavar var x end metavar indeed metavar var b end metavar peano imply metavar var a end metavar rule plus var a peano var peano times peano zero peano is peano zero end define end math
end "}
\display{"
begin math define statement of axiom a one as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end define
then define proof of axiom a one as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom a two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define
then define proof of axiom a two as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom a three as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end define
then define proof of axiom a three as rule tactic end define end math
end "}
The order of quantifiers in the following axiom is such that "
begin bracket metavar var c end metavar end bracket
end " which the current conclusion tactic cannot guess comes first. This allows to supply a value for "
begin bracket metavar var c end metavar end bracket
end " without having to supply values for the other meta-variables.
\display{"
begin math define statement of axiom a four as system s infer all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse peano all metavar var x end metavar indeed metavar var b end metavar peano imply metavar var a end metavar end define
then define proof of axiom a four as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom a five as system s infer all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed peano nonfree metavar var x end metavar in metavar var a end metavar end nonfree endorse peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano all metavar var x end metavar indeed metavar var b end metavar end define
then define proof of axiom a five as rule tactic end define end math
end "}
\display{"
begin math define statement of rule mp as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar end define
then define proof of rule mp as rule tactic end define end math
end "}
\display{"
begin math define statement of rule gen as system s infer all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer peano all metavar var x end metavar indeed metavar var a end metavar end define
then define proof of rule gen as rule tactic end define 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 define statement of axiom s one as system s infer var a peano var peano is var b peano var peano imply var a peano var peano is var c peano var peano imply var b peano var peano is var c peano var end define
then define proof of axiom s one as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom s two as system s infer var a peano var peano is var b peano var peano imply var a peano var peano succ peano is var b peano var peano succ end define
then define proof of axiom s two as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom s three as system s infer not peano zero peano is var a peano var peano succ end define
then define proof of axiom s three as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom s four as system s infer var a peano var peano succ peano is var b peano var peano succ peano imply var a peano var peano is var b peano var end define
then define proof of axiom s four as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom s five as system s infer var a peano var peano plus peano zero peano is var a peano var end define
then define proof of axiom s five as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom s six as system s infer var a peano var peano plus var b peano var peano succ peano is var a peano var peano plus var b peano var peano succ end define
then define proof of axiom s six as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom s seven as system s infer var a peano var peano times peano zero peano is peano zero end define
then define proof of axiom s seven as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom s eight as system s infer var a peano var peano times var b peano var peano succ peano is var a peano var peano times var b peano var peano plus var a peano var end define
then define proof of axiom s eight as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom s nine as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var x end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var x end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var x end metavar is metavar var x end metavar peano succ end sub endorse metavar var b end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar end define
then define proof of axiom s nine as rule tactic end define end math
end "}
\subsection{A lemma and a proof}
We now prove Lemma "
begin math define pyk of lemma l three two a as text "lemma l three two a" end text end define end math
then math define tex of lemma l three two a as text "
L3.2(a)" end text end define end math
end " which is an instance of the corresponding proposition in Mendelson \cite{mendelson}:
\statement{"
begin math define statement of lemma l three two a as system s infer var x peano var peano is var x peano var end define end math
end "}
\statement{"
begin math define proof of lemma l three two a as lambda var c dot lambda var x dot proof expand quote system s infer axiom s five conclude var a peano var peano plus peano zero peano is var a peano var cut rule gen modus ponens var a peano var peano plus peano zero peano is var a peano var conclude peano all var a peano var indeed var a peano var peano plus peano zero peano is var a peano var cut axiom a four at var x peano var conclude peano all var a peano var indeed var a peano var peano plus peano zero peano is var a peano var peano imply var x peano var peano plus peano zero peano is var x peano var cut rule mp modus ponens peano all var a peano var indeed var a peano var peano plus peano zero peano is var a peano var peano imply var x peano var peano plus peano zero peano is var x peano var modus ponens peano all var a peano var indeed var a peano var peano plus peano zero peano is var a peano var conclude var x peano var peano plus peano zero peano is var x peano var cut axiom s one conclude var a peano var peano is var b peano var peano imply var a peano var peano is var c peano var peano imply var b peano var peano is var c peano var cut rule gen modus ponens var a peano var peano is var b peano var peano imply var a peano var peano is var c peano var peano imply var b peano var peano is var c peano var conclude peano all var c peano var indeed var a peano var peano is var b peano var peano imply var a peano var peano is var c peano var peano imply var b peano var peano is var c peano var cut axiom a four at var x peano var conclude peano all var c peano var indeed var a peano var peano is var b peano var peano imply var a peano var peano is var c peano var peano imply var b peano var peano is var c peano var peano imply var a peano var peano is var b peano var peano imply var a peano var peano is var x peano var peano imply var b peano var peano is var x peano var cut rule mp modus ponens peano all var c peano var indeed var a peano var peano is var b peano var peano imply var a peano var peano is var c peano var peano imply var b peano var peano is var c peano var peano imply var a peano var peano is var b peano var peano imply var a peano var peano is var x peano var peano imply var b peano var peano is var x peano var modus ponens peano all var c peano var indeed var a peano var peano is var b peano var peano imply var a peano var peano is var c peano var peano imply var b peano var peano is var c peano var conclude var a peano var peano is var b peano var peano imply var a peano var peano is var x peano var peano imply var b peano var peano is var x peano var cut rule gen modus ponens var a peano var peano is var b peano var peano imply var a peano var peano is var x peano var peano imply var b peano var peano is var x peano var conclude peano all var b peano var indeed var a peano var peano is var b peano var peano imply var a peano var peano is var x peano var peano imply var b peano var peano is var x peano var cut axiom a four at var x peano var conclude peano all var b peano var indeed var a peano var peano is var b peano var peano imply var a peano var peano is var x peano var peano imply var b peano var peano is var x peano var peano imply var a peano var peano is var x peano var peano imply var a peano var peano is var x peano var peano imply var x peano var peano is var x peano var cut rule mp modus ponens peano all var b peano var indeed var a peano var peano is var b peano var peano imply var a peano var peano is var x peano var peano imply var b peano var peano is var x peano var peano imply var a peano var peano is var x peano var peano imply var a peano var peano is var x peano var peano imply var x peano var peano is var x peano var modus ponens peano all var b peano var indeed var a peano var peano is var b peano var peano imply var a peano var peano is var x peano var peano imply var b peano var peano is var x peano var conclude var a peano var peano is var x peano var peano imply var a peano var peano is var x peano var peano imply var x peano var peano is var x peano var cut rule gen modus ponens var a peano var peano is var x peano var peano imply var a peano var peano is var x peano var peano imply var x peano var peano is var x peano var conclude peano all var a peano var indeed var a peano var peano is var x peano var peano imply var a peano var peano is var x peano var peano imply var x peano var peano is var x peano var cut axiom a four at var x peano var peano plus peano zero conclude peano all var a peano var indeed var a peano var peano is var x peano var peano imply var a peano var peano is var x peano var peano imply var x peano var peano is var x peano var peano imply var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano is var x peano var cut rule mp modus ponens peano all var a peano var indeed var a peano var peano is var x peano var peano imply var a peano var peano is var x peano var peano imply var x peano var peano is var x peano var peano imply var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano is var x peano var modus ponens peano all var a peano var indeed var a peano var peano is var x peano var peano imply var a peano var peano is var x peano var peano imply var x peano var peano is var x peano var conclude var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano is var x peano var cut rule mp modus ponens var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano is var x peano var modus ponens var x peano var peano plus peano zero peano is var x peano var conclude var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano is var x peano var cut rule mp modus ponens var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano is var x peano var modus ponens var x peano var peano plus peano zero peano is var x peano var conclude var x peano var peano is var x peano var end quote state proof state cache var c end expand end define end math
end "}
\subsection{An alternative axiomatic system}
System "
begin math define pyk of system prime s as text "system prime s" end text end define end math
then math define tex of system prime s as text "
S'" end text end define end math
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 math define pyk of axiom prime a one as text "axiom prime a one" end text end define end math
then math define tex of axiom prime a one as text "
A1'" end text end define end math
end ",
"
begin math define pyk of axiom prime a two as text "axiom prime a two" end text end define end math
then math define tex of axiom prime a two as text "
A2'" end text end define end math
end ",
"
begin math define pyk of axiom prime a three as text "axiom prime a three" end text end define end math
then math define tex of axiom prime a three as text "
A3'" end text end define end math
end ",
"
begin math define pyk of axiom prime a four as text "axiom prime a four" end text end define end math
then math define tex of axiom prime a four as text "
A4'" end text end define end math
end ", and
"
begin math define pyk of axiom prime a five as text "axiom prime a five" end text end define end math
then math define tex of axiom prime a five as text "
A5'" end text end define end math
end "
and inference rules
"
begin math define pyk of rule prime mp as text "rule prime mp" end text end define end math
then math define tex of rule prime mp as text "
MP'" end text end define end math
end " and
"
begin math define pyk of rule prime gen as text "rule prime gen" end text end define end math
then math define tex of rule prime gen as text "
Gen'" end text end define end math
end "
of first order predicate calculus. Furthermore, it comprises the proper axioms
"
begin math define pyk of axiom prime s one as text "axiom prime s one" end text end define end math
then math define tex of axiom prime s one as text "
S1'" end text end define end math
end ",
"
begin math define pyk of axiom prime s two as text "axiom prime s two" end text end define end math
then math define tex of axiom prime s two as text "
S2'" end text end define end math
end ",
"
begin math define pyk of axiom prime s three as text "axiom prime s three" end text end define end math
then math define tex of axiom prime s three as text "
S3'" end text end define end math
end ",
"
begin math define pyk of axiom prime s four as text "axiom prime s four" end text end define end math
then math define tex of axiom prime s four as text "
S4'" end text end define end math
end ",
"
begin math define pyk of axiom prime s five as text "axiom prime s five" end text end define end math
then math define tex of axiom prime s five as text "
S5'" end text end define end math
end ",
"
begin math define pyk of axiom prime s six as text "axiom prime s six" end text end define end math
then math define tex of axiom prime s six as text "
S6'" end text end define end math
end ",
"
begin math define pyk of axiom prime s seven as text "axiom prime s seven" end text end define end math
then math define tex of axiom prime s seven as text "
S7'" end text end define end math
end ",
"
begin math define pyk of axiom prime s eight as text "axiom prime s eight" end text end define end math
then math define tex of axiom prime s eight as text "
S8'" end text end define end math
end ", and
"
begin math define pyk of axiom prime s nine as text "axiom prime s nine" end text end define end math
then math define tex of axiom prime s nine as text "
S9'" end text end define end math
end ".
System "
begin bracket system prime s end bracket
end " is defined thus:
\display{"
begin math define statement of system prime s as all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano succ peano is metavar var b end metavar peano succ peano imply metavar var a end metavar peano is metavar var b end metavar rule plus all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar rule plus all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed peano nonfree quote metavar var x end metavar end quote in quote metavar var a end metavar end quote end nonfree endorse peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano all metavar var x end metavar indeed metavar var b end metavar rule plus all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano plus metavar var r end metavar peano succ peano is metavar var t end metavar peano plus metavar var r end metavar peano succ rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano times metavar var b end metavar peano succ peano is metavar var a end metavar peano times metavar var b end metavar peano plus metavar var a end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar rule plus all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var t end metavar peano succ peano is metavar var r end metavar peano succ rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano plus metavar var b end metavar peano succ peano is metavar var a end metavar peano plus metavar var b end metavar peano succ rule plus all metavar var a end metavar indeed not peano zero peano is metavar var a end metavar peano succ rule plus all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer peano all metavar var x end metavar indeed metavar var a end metavar rule plus all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse peano all metavar var x end metavar indeed metavar var b end metavar peano imply metavar var a end metavar rule plus all metavar var h end metavar indeed all metavar var t end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano plus peano zero peano is metavar var t end metavar rule plus all metavar var a end metavar indeed metavar var a end metavar peano times peano zero peano is peano zero rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar rule plus all metavar var t end metavar indeed metavar var t end metavar peano is metavar var t end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var x end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var x end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var x end metavar is metavar var x end metavar peano succ end sub endorse metavar var b end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar rule plus all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar infer metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar rule plus all metavar var a end metavar indeed metavar var a end metavar peano plus peano zero peano is metavar var a end metavar end define end math
end "}
\display{"
begin math define statement of axiom prime a one as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end define
then define proof of axiom prime a one as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a two as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define
then define proof of axiom prime a two as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a three as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end define
then define proof of axiom prime a three as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a four as system prime s infer all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse peano all metavar var x end metavar indeed metavar var b end metavar peano imply metavar var a end metavar end define
then define proof of axiom prime a four as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a five as system prime s infer all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed peano nonfree quote metavar var x end metavar end quote in quote metavar var a end metavar end quote end nonfree endorse peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano all metavar var x end metavar indeed metavar var b end metavar end define
then define proof of axiom prime a five as rule tactic end define end math
end "}
\display{"
begin math define statement of rule prime mp as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar end define
then define proof of rule prime mp as rule tactic end define end math
end "}
\display{"
begin math define statement of rule prime gen as system prime s infer all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer peano all metavar var x end metavar indeed metavar var a end metavar end define
then define proof of rule prime gen as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s one as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar end define
then define proof of axiom prime s one as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s two as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ end define
then define proof of axiom prime s two as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s three as system prime s infer all metavar var a end metavar indeed not peano zero peano is metavar var a end metavar peano succ end define
then define proof of axiom prime s three as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s four as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano succ peano is metavar var b end metavar peano succ peano imply metavar var a end metavar peano is metavar var b end metavar end define
then define proof of axiom prime s four as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s five as system prime s infer all metavar var a end metavar indeed metavar var a end metavar peano plus peano zero peano is metavar var a end metavar end define
then define proof of axiom prime s five as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s six as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano plus metavar var b end metavar peano succ peano is metavar var a end metavar peano plus metavar var b end metavar peano succ end define
then define proof of axiom prime s six as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s seven as system prime s infer all metavar var a end metavar indeed metavar var a end metavar peano times peano zero peano is peano zero end define
then define proof of axiom prime s seven as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s eight as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano times metavar var b end metavar peano succ peano is metavar var a end metavar peano times metavar var b end metavar peano plus metavar var a end metavar end define
then define proof of axiom prime s eight as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s nine as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var x end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var x end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var x end metavar is metavar var x end metavar peano succ end sub endorse metavar var b end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar end define
then define proof of axiom prime s nine as rule tactic end define 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 metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end bracket
end " and the latter says "
begin bracket system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar 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 math define pyk of lemma prime l three two a as text "lemma prime l three two a" end text end define end math
then math define tex of lemma prime l three two a as text "
L3.2(a)'" end text end define end math
end ":
\statement{"
begin math define statement of lemma prime l three two a as system prime s infer all metavar var a end metavar indeed metavar var a end metavar peano is metavar var a end metavar end define end math
end "}
\statement{"
begin math define proof of lemma prime l three two a as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed axiom prime s five conclude metavar var a end metavar peano plus peano zero peano is metavar var a end metavar cut axiom prime s one conclude metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano is metavar var a end metavar cut rule prime mp modus ponens metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano is metavar var a end metavar modus ponens metavar var a end metavar peano plus peano zero peano is metavar var a end metavar conclude metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano is metavar var a end metavar cut rule prime mp modus ponens metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano is metavar var a end metavar modus ponens metavar var a end metavar peano plus peano zero peano is metavar var a end metavar conclude metavar var a end metavar peano is metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "}
\section{Formal development}
\subsection{Propositional calculus}
\subsubsection{Modus ponens}
We use "
begin math define pyk of var x macro modus ponens var y as text "* macro modus ponens *" end text end define end math
then math define tex of var x macro modus ponens var y as text "#1.
\unrhd #2." end text end define end math
end " as shorthand for modus ponens:
\display{"
begin math define macro of var x macro modus ponens var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x macro modus ponens var y as rule prime mp modus ponens var x modus ponens var y end define end quote end define end define end math
end "}
\subsubsection{Lemma M1.7}
Lemma "
begin math define pyk of mendelson one seven as text "mendelson one seven" end text end define end math
then math define tex of mendelson one seven as text "
M1.7" end text end define end math
end " (i.e.\ Lemma 1.7 in Mendelson \cite{mendelson}) reads:
\statement{"
begin math define statement of mendelson one seven as system prime s infer all metavar var b end metavar indeed metavar var b end metavar peano imply metavar var b end metavar end define end math
end "}
\statement{"
begin math define proof of mendelson one seven as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var b end metavar indeed axiom prime a one conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut axiom prime a two conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut axiom prime a one conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var b end metavar end quote state proof state cache var c end expand end define end math
end "}
\subsubsection{Hypothetical modus ponens}
The hypothetical version "
begin math define pyk of hypothetical rule prime mp as text "hypothetical rule prime mp" end text end define end math
then math define tex of hypothetical rule prime mp as text "
MP'_h" end text end define end math
end " of modus ponens "
begin math rule prime mp end math
end " has a hypothesis "
begin math metavar var h end metavar end math
end " on each premise and on the conclusion:
\statement{"
begin math define statement of hypothetical rule prime mp as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer metavar var h end metavar peano imply metavar var a end metavar infer metavar var h end metavar peano imply metavar var b end metavar end define end math
end "}
\statement{"
begin math define proof of hypothetical rule prime mp as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer metavar var h end metavar peano imply metavar var a end metavar infer axiom prime a two conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar modus ponens metavar var h end metavar peano imply metavar var a end metavar conclude metavar var h end metavar peano imply metavar var b end metavar end quote state proof state cache var c end expand end define end math
end "}
We use "
begin math define pyk of var x hypothetical modus ponens var y as text "* hypothetical modus ponens *" end text end define end math
then math define tex of var x hypothetical modus ponens var y as text "#1.
\unrhd_h #2." end text end define end math
end " as shorthand for hypothetical modus ponens:
\display{"
begin math define macro of var x hypothetical modus ponens var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 quote end define end define end math
end "}
\subsubsection{Turning lemmas to hypothetical lemmas}
Lemma "
begin math define pyk of hypothesize as text "hypothesize" end text end define end math
then math define tex of hypothesize as text "
Hypothesize" end text end define end math
end " turns a lemma with no premises into one that assumes the hypothesis "
begin bracket metavar var h end metavar end bracket
end " to hold:
\statement{"
begin math define statement of hypothesize as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer metavar var h end metavar peano imply metavar var a end metavar end define end math
end "}
\statement{"
begin math define proof of hypothesize as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer axiom prime a one conclude metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar modus ponens metavar var a end metavar conclude metavar var h end metavar peano imply metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "}
\subsection{First order predicate calculus}
\subsubsection{Hypothetical generalization}
The hypothetical version "
begin math define pyk of hypothetical rule prime gen as text "hypothetical rule prime gen" end text end define end math
then math define tex of hypothetical rule prime gen as text "
Gen'_h" end text end define end math
end " of generalisation "
begin math rule prime gen end math
end " has a hypothesis "
begin math metavar var h end metavar end math
end " on premise and conclusion:
\statement{"
begin math define statement of hypothetical rule prime gen as system prime s infer all metavar var h end metavar indeed all metavar var x end metavar indeed all metavar var a end metavar indeed peano nonfree quote metavar var x end metavar end quote in quote metavar var h end metavar end quote end nonfree endorse metavar var h end metavar peano imply metavar var a end metavar infer metavar var h end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar end define end math
end "}
\statement{"
begin math define proof of hypothetical rule prime gen as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var x end metavar indeed all metavar var a end metavar indeed peano nonfree quote metavar var x end metavar end quote in quote metavar var h end metavar end quote end nonfree endorse metavar var h end metavar peano imply metavar var a end metavar infer axiom prime a five modus probans peano nonfree quote metavar var x end metavar end quote in quote metavar var h end metavar end quote end nonfree conclude peano all metavar var x end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar cut rule prime gen modus ponens metavar var h end metavar peano imply metavar var a end metavar conclude peano all metavar var x end metavar indeed metavar var h end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens peano all metavar var x end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar modus ponens peano all metavar var x end metavar indeed metavar var h end metavar peano imply metavar var a end metavar conclude metavar var h end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "}
\subsection{Peano arithmetic}
\subsubsection{Lemma M3.2(a)}
Lemma "
begin math define pyk of mendelson three two a as text "mendelson three two a" end text end define end math
then math define tex of mendelson three two a as text "
M3.2(a)" end text end define end math
end " and the associated hypothetical lemma "
begin math define pyk of hypothetical three two a as text "hypothetical three two a" end text end define end math
then math define tex of hypothetical three two a as text "
M3.2(a)_h" end text end define end math
end " read:
\statement{"
begin math define statement of mendelson three two a as system prime s infer all metavar var t end metavar indeed metavar var t end metavar peano is metavar var t end metavar end define
then define proof of mendelson three two a as rule tactic end define end math
end "}
\statement{"
begin math define statement of hypothetical three two a as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar end define 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 define proof of hypothetical three two a as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed mendelson three two a conclude metavar var t end metavar peano is metavar var t end metavar cut hypothesize modus ponens metavar var t end metavar peano is metavar var t end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar end quote state proof state cache var c end expand end define end math
end "}
\subsubsection{Lemma M3.2(b)}
Lemma "
begin math define pyk of hypothetical three two b as text "hypothetical three two b" end text end define end math
then math define tex of hypothetical three two b as text "
M3.2(b)_h" end text end define end math
end " reads:
\statement{"
begin math define statement of hypothetical three two b as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end define
then define proof of hypothetical three two b as rule tactic end define end math
end "}
\statement{"
begin math define proof of hypothetical three two b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer axiom prime s one conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut hypothesize modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut hypothetical three two a conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar conclude metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end quote state proof state cache var c end expand end define end math
end "}
\subsubsection{Lemma M3.1(S1)}
Lemma "
begin math define pyk of hypothetical three one s one as text "hypothetical three one s one" end text end define end math
then math define tex of hypothetical three one s one as text "
M3.1(S1')_h" end text end define end math
end " is the hypothetical version of Mendelson Lemma $3.1(S1')$:
\statement{"
begin math define statement of hypothetical three one s one as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end define
then define proof of hypothetical three one s one as rule tactic end define end math
end "}
\subsubsection{Lemma M3.2(c)}
Lemma "
begin math define pyk of hypothetical three two c as text "hypothetical three two c" end text end define end math
then math define tex of hypothetical three two c as text "
M3.2(c)_h" end text end define end math
end " is the hypothetical version of Mendelson Lemma 3.2(c) which expresses ordinary transitivity:
\statement{"
begin math define statement of hypothetical three two c as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar infer metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end define
then define proof of hypothetical three two c as rule tactic end define end math
end "}
\subsubsection{Lemma M3.1(S2)}
Lemma "
begin math define pyk of hypothetical three one s two as text "hypothetical three one s two" end text end define end math
then math define tex of hypothetical three one s two as text "
M3.1(S2')_h" end text end define end math
end " is the hypothetical version of Mendelson Lemma $3.1(S2')$:
\statement{"
begin math define statement of hypothetical three one s two as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var t end metavar peano succ peano is metavar var r end metavar peano succ end define
then define proof of hypothetical three one s two as rule tactic end define end math
end "}
\subsubsection{Lemma M3.1(S5)}
Lemma "
begin math define pyk of hypothetical three one s five as text "hypothetical three one s five" end text end define end math
then math define tex of hypothetical three one s five as text "
M3.1(S5')_h" end text end define end math
end " is the hypothetical version of Mendelson Lemma $3.1(S5')$:
\statement{"
begin math define statement of hypothetical three one s five as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano plus peano zero peano is metavar var t end metavar end define
then define proof of hypothetical three one s five as rule tactic end define end math
end "}
\subsubsection{Lemma M3.1(S6)}
Lemma "
begin math define pyk of hypothetical three one s six as text "hypothetical three one s six" end text end define end math
then math define tex of hypothetical three one s six as text "
M3.1(S6')_h" end text end define end math
end " is the hypothetical version of Mendelson Lemma $3.1(S6')$:
\statement{"
begin math define statement of hypothetical three one s six as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano plus metavar var r end metavar peano succ peano is metavar var t end metavar peano plus metavar var r end metavar peano succ end define
then define proof of hypothetical three one s six as rule tactic end define end math
end "}
\subsubsection{Lemma M3.2(f)}
Lemma "
begin math define pyk of mendelson three two f as text "mendelson three two f" end text end define end math
then math define tex of mendelson three two f as text "
M3.2(f)" end text end define end math
end " is the closure of Mendelson Lemma 3.2(f) for the concrete variable "
begin bracket var t peano var end bracket
end ":
\statement{"
begin math define statement of mendelson three two f as system prime s infer peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var end define end math
end "}
The proof below uses local macro definitions.
\statement{"
begin math define proof of mendelson three two f as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime a one conclude var x peano imply var x peano imply var x cut hypothetical three one s five conclude var x peano imply var x peano imply var x peano imply peano zero peano plus peano zero peano is peano zero cut hypothetical three two b modus ponens var x peano imply var x peano imply var x peano imply peano zero peano plus peano zero peano is peano zero conclude var x peano imply var x peano imply var x peano imply peano zero peano is peano zero peano plus peano zero cut rule prime mp modus ponens var x peano imply var x peano imply var x peano imply peano zero peano is peano zero peano plus peano zero modus ponens var x peano imply var x peano imply var x conclude peano zero peano is peano zero peano plus peano zero cut mendelson one seven conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var cut hypothetical three one s two modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut hypothetical three one s six conclude var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut hypothetical three two b modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut hypothetical three two c modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut rule prime gen modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut axiom prime s nine conclude peano zero peano is peano zero peano plus peano zero peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var cut rule prime mp modus ponens peano zero peano is peano zero peano plus peano zero peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var modus ponens peano zero peano is peano zero peano plus peano zero conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var cut rule prime mp modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var end quote state proof state cache var c end expand end define end math
end "}
\appendix
\section{Chores}
\subsection{The name of the page}
This defines the name of the page:
\display{"
begin math define pyk of peano as text "peano" end text end define end math
end "}
\subsection{Variables of Peano arithmetic}\label{section:VariablesOfPeanoArithmetic}
We use
"
begin math define pyk of peano b as text "peano b" end text end define end math
then math define tex of peano b as text "
\dot{\mathit{b}}" end text end define end math
end ",
"
begin math define pyk of peano c as text "peano c" end text end define end math
then math define tex of peano c as text "
\dot{\mathit{c}}" end text end define end math
end ",
"
begin math define pyk of peano d as text "peano d" end text end define end math
then math define tex of peano d as text "
\dot{\mathit{d}}" end text end define end math
end ",
"
begin math define pyk of peano e as text "peano e" end text end define end math
then math define tex of peano e as text "
\dot{\mathit{e}}" end text end define end math
end ",
"
begin math define pyk of peano f as text "peano f" end text end define end math
then math define tex of peano f as text "
\dot{\mathit{f}}" end text end define end math
end ",
"
begin math define pyk of peano g as text "peano g" end text end define end math
then math define tex of peano g as text "
\dot{\mathit{g}}" end text end define end math
end ",
"
begin math define pyk of peano h as text "peano h" end text end define end math
then math define tex of peano h as text "
\dot{\mathit{h}}" end text end define end math
end ",
"
begin math define pyk of peano i as text "peano i" end text end define end math
then math define tex of peano i as text "
\dot{\mathit{i}}" end text end define end math
end ",
"
begin math define pyk of peano j as text "peano j" end text end define end math
then math define tex of peano j as text "
\dot{\mathit{j}}" end text end define end math
end ",
"
begin math define pyk of peano k as text "peano k" end text end define end math
then math define tex of peano k as text "
\dot{\mathit{k}}" end text end define end math
end ",
"
begin math define pyk of peano l as text "peano l" end text end define end math
then math define tex of peano l as text "
\dot{\mathit{l}}" end text end define end math
end ",
"
begin math define pyk of peano m as text "peano m" end text end define end math
then math define tex of peano m as text "
\dot{\mathit{m}}" end text end define end math
end ",
"
begin math define pyk of peano n as text "peano n" end text end define end math
then math define tex of peano n as text "
\dot{\mathit{n}}" end text end define end math
end ",
"
begin math define pyk of peano o as text "peano o" end text end define end math
then math define tex of peano o as text "
\dot{\mathit{o}}" end text end define end math
end ",
"
begin math define pyk of peano p as text "peano p" end text end define end math
then math define tex of peano p as text "
\dot{\mathit{p}}" end text end define end math
end ",
"
begin math define pyk of peano q as text "peano q" end text end define end math
then math define tex of peano q as text "
\dot{\mathit{q}}" end text end define end math
end ",
"
begin math define pyk of peano r as text "peano r" end text end define end math
then math define tex of peano r as text "
\dot{\mathit{r}}" end text end define end math
end ",
"
begin math define pyk of peano s as text "peano s" end text end define end math
then math define tex of peano s as text "
\dot{\mathit{s}}" end text end define end math
end ",
"
begin math define pyk of peano t as text "peano t" end text end define end math
then math define tex of peano t as text "
\dot{\mathit{t}}" end text end define end math
end ",
"
begin math define pyk of peano u as text "peano u" end text end define end math
then math define tex of peano u as text "
\dot{\mathit{u}}" end text end define end math
end ",
"
begin math define pyk of peano v as text "peano v" end text end define end math
then math define tex of peano v as text "
\dot{\mathit{v}}" end text end define end math
end ",
"
begin math define pyk of peano w as text "peano w" end text end define end math
then math define tex of peano w as text "
\dot{\mathit{w}}" end text end define end math
end ",
"
begin math define pyk of peano x as text "peano x" end text end define end math
then math define tex of peano x as text "
\dot{\mathit{x}}" end text end define end math
end ",
"
begin math define pyk of peano y as text "peano y" end text end define end math
then math define tex of peano y as text "
\dot{\mathit{y}}" end text end define end math
end ", and
"
begin math define pyk of peano z as text "peano z" end text end define end math
then math define tex of peano z as text "
\dot{\mathit{z}}" end text end define end math
end " to denote variables of Peano arithmetic:
"
begin math define macro of peano b as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano b as var b peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano c as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano c as var c peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano d as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano d as var d peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano e as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano e as var e peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano f as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano f as var f peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano g as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano g as var g peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano h as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano h as var h peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano i as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano i as var i peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano j as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano j as var j peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano k as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano k as var k peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano l as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano l as var l peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano m as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano m as var m peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano n as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano n as var n peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano o as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano o as var o peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano p as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano p as var p peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano q as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano q as var q peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano r as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano r as var r peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano s as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano s as var s peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano t as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano t as var t peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano u as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano u as var u peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano v as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano v as var v peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano w as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano w as var w peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano x as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano x as var x peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano y as var y peano var end define end quote end define end define end math
end ", and
"
begin math define macro of peano z as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano z as var z peano var end define end quote end define 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 define priority of peano as 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 define 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,