"File page.tex
\documentclass [fleqn]{article}
\setlength {\overfullrule }{1mm}
\input{lgwinclude}
\usepackage{latexsym}
\usepackage{parskip}
\parindent=0pt % Ingen indrykkning
\frenchspacing
%\usepackage{verbatim}
%\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 {Logic - Peano Arithmetic\\
$\quad$\\
{\large
"
begin math peano all var t peano var indeed peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var end math
end "
}
}
\author {Kasper Frederiksen, tofu@diku.dk}
\maketitle
\tableofcontents
"
begin ragged right
end "
\clearpage
\section{Introduction}
This report proves proposition "
begin math lemma prime l three two h end math
end " in \cite{mendelson}, page 156. That is:
\display{"
begin math define statement of lemma prime l three two h as system prime s infer peano all var t peano var indeed peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var end define end math
end "}
The successful proof of this lemma can be seen in section
\ref{res.lemma}.
The entire text has been verified as mathematically correct by the
LogiWeb system. The source code can be obtained from the online
version of this text:
\begin{center}
\verb|http://www.diku.dk/hjemmesider/studerende/tofu/Logik/|
\end{center}
\subsection{About LogiWeb}
The LogiWeb system is being developed by Klaus Grue (DIKU) and is
fully defined on the LogiWeb {\bf base page}
\footnote{This report uses the version of base page that has the time stamp {\scriptsize \bf GRD-2005-06-22-UTC-06-58-05-413682}}
written by Klaus Grue:
\begin{center}
\verb|http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/latest/|
\end{center}
From a users point of view LogiWeb consists of two parts, a compiler
and a (web)server. The user will write his text using latex syntax
and whenever he wishes to express mathematics this will be written
amongst the ordinary text, but using \verb|pyk| syntax. When the
source file is compiled two things happen. The pyk part of the file is
translated into latex and given to the latex compiler along with the
rest of the text, also the mathematics expressed by the pyk is
checked for correctness.
The LogiWeb system allows the user to reference mathematical constructs
defined on other pages. The task of managing requests for these pages
falls to the LogiWeb server. The LogiWeb server on DIKU has a
graphical front-end in the form of a webserver, that can be accessed
through the links given above.
\subsection{About the proof system}
All proofs in this text have been completed in the axiomatic
arithmetic system called "
begin math system prime s end math
end ". This
system is a Peano Arithmetic system and is fully defined on the {\bf
peano page} \footnote{This report uses the version of peano page that
has the time stamp {\scriptsize \bf GRD-2005-06-22-UTC-07-23-31-271829
}} written by Klaus Grue: \begin{center}
\verb|http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/|
\end{center}
It should be noted that the peano page redefines all the arithmetic
and logical operators from base page in special ``peano
versions''. These new operators are identical to their classical
counterparts. To avoid any confusion figure (\ref{aaa}) gives an
overview of the new operators.
\begin{figure}[h]
\centering
\begin{tabular}{|ccc|}
\hline
$ False \Rightarrow True $ & $\to$ & "
begin math false peano imply true end math
end " \\
$ \mathrm{ arbitrary variable }: A, B, C,... $ & $\to$ & "
begin math metavar var a end metavar end math
end ", "
begin math metavar var b end metavar end math
end ", "
begin math metavar var c end metavar end math
end ",$\ldots$\\
$ \mathrm{ specific terms }: a, b, c, ... $ & $\to$ & "
begin math var a peano var end math
end ", "
begin math var b peano var end math
end ", "
begin math var c peano var end math
end ",$\ldots$\\
$ \forall a: a + 0 = a $ & $\to$ & "
begin math peano all var a peano var indeed var a peano var peano plus peano zero peano is var a peano var end math
end " \\
$ \neg(1 \cdot 0 = 1) $ & $\to$ & "
begin math peano not peano zero peano succ peano times peano zero peano is peano zero peano succ end math
end "\\
\hline
\end{tabular}
\caption{The new version of the operators}
\label{aaa}
\end{figure}
Peano arithmetic is only defined on natural numbers, and the successor
operation is written like this: "
begin math peano zero peano succ peano is peano zero peano succ end math
end ".
This peano page also defines the axioms and rules of the "
begin math system prime s end math
end " system. These are identical to those defined
in \cite{mendelson}, chapters two and three. Below I repeat the theory
as it is defined on the peano page. Since the pyk syntax is not always
obvious I have included some comments.
System "
begin bracket system prime s end bracket
end " is defined thus:
\display{"
begin math define statement of system prime s as var x 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 "}
This axiom allows us to remove a universal kvantor and replace the quantified
variable with a specific term, as long as this does not cause a variable clash.
When using the axiom, you must state which term you wish to substitute into
the place of the quantified variable. The axiom is used like this:\\
"
begin math axiom prime a four at var t peano var end math
end "
$\to$
"
begin math peano all var q peano var indeed var q peano var peano is var q peano var peano imply var t peano var peano is var t peano var 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 "}
This axiom is not used in this report.
\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 "}
This is the generalization rule, that allows us to add a universal kvantor in front
of a proof line.
\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 "}
This is the induction axiom. What it basically says is ``base case'' $\Rightarrow$ ``induction step'' $\Rightarrow$ ``conclusion''.
\section{The Deduction Algorithm}
Mendelson introduces the {\bf Deduction Theorem} for first-order
theories in \cite{mendelson} page 74. The proof is stated in the form
of an algorithm that will turn a proof of the the lemma
"
begin math system prime s infer metavar var b end metavar infer metavar var c end metavar end math
end ",
in to a proof of the lemma
"
begin math system prime s infer metavar var b end metavar peano imply metavar var c end metavar end math
end ".
While it would be possible to implement this automatic proof converter in
pyk, as a part of this text, Klaus has advised that we do not attempt
this. We are going to follow this advise. Instead we run the algorithm
by hand and type in the converted proofs.
A god description of the deduction algorithm can be found at:
\begin{center}
\verb|http://www.diku.dk/undervisning/2005s/235/deduction.html|
\end{center}
\section{Supporting Lemmas\label{support}}
Before we start proving the lemmas in section \ref{main.lemmas}. Let
us first prove a number of lemmas that will help make the following
proofs shorter.
Pleas note that many of the lemmas in this section were included on
a when-needed basis. If, in section \ref{main.lemmas}, you notice a
situation where one of the following lemmas could have been used to
shorten the proof, then that is an ``older'' proof from before the
supporting lemma was included.
\subsection{Corollary "
begin math corollary one point ten a end math
end "}
The lemma
"
begin math define pyk of corollary one point ten a as text "corollary one point ten a" end text end define end math
then math define tex of corollary one point ten a as text "C1.10a" end text end define end math
end "
is taken from \cite{mendelson} page 38.
\display{"
begin math define statement of corollary one point ten a as system prime s infer all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed metavar var b end metavar peano imply metavar var c end metavar infer metavar var c end metavar peano imply metavar var d end metavar infer metavar var b end metavar peano imply metavar var d end metavar end define end math
end "}
"
begin math define proof of corollary one point ten a as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed metavar var b end metavar peano imply metavar var c end metavar infer metavar var c end metavar peano imply metavar var d end metavar infer axiom prime a one conclude metavar var c end metavar peano imply metavar var d end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar cut rule prime mp modus ponens metavar var c end metavar peano imply metavar var d end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar modus ponens metavar var c end metavar peano imply metavar var d end metavar conclude metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar cut axiom prime a two conclude metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var d end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var d end metavar modus ponens metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar conclude metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var d end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var d end metavar modus ponens metavar var b end metavar peano imply metavar var c end metavar conclude metavar var b end metavar peano imply metavar var d end metavar end quote state proof state cache var c end expand end define end math
end "
\subsection{Corollary "
begin math corollary one point ten b end math
end "}
The lemma
"
begin math define pyk of corollary one point ten b as text "corollary one point ten b" end text end define end math
then math define tex of corollary one point ten b as text "C1.10(b)" end text end define end math
end "
is taken from \cite{mendelson} page 38.
\display{"
begin math define statement of corollary one point ten b as system prime s infer all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar infer metavar var c end metavar infer metavar var b end metavar peano imply metavar var d end metavar end define end math
end "}
"
begin math define proof of corollary one point ten b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar infer metavar var c end metavar infer axiom prime a one conclude metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var c end metavar conclude metavar var b end metavar peano imply metavar var c end metavar cut axiom prime a two conclude metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var d end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var d end metavar modus ponens metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar conclude metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var d end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var d end metavar modus ponens metavar var b end metavar peano imply metavar var c end metavar conclude metavar var b end metavar peano imply metavar var d end metavar end quote state proof state cache var c end expand end define end math
end "
\subsection{Lemma "
begin math lemma prime a one star end math
end "}
The lemma
"
begin math define pyk of lemma prime a one star as text "lemma prime a one star" end text end define end math
then math define tex of lemma prime a one star as text "{A1'}^*" end text end define end math
end "
is used during the deduction algorithm, when one wishes to add a hypothesis, "
begin math metavar var h end metavar end math
end ", to a
line of a proof. This will shorten the proof by one line.
\display{"
begin math define statement of lemma prime a one star as system prime s infer all metavar var a end metavar indeed all metavar var h 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 "}
"
begin math define proof of lemma prime a one star as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var h 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{Lemma "
begin math lemma prime a two star end math
end "}
Use of the axiom "
begin math axiom prime a two end math
end " is often followed
by a use of the modus ponens rule. If we instead use lemma
"
begin math define pyk of lemma prime a two star as text "lemma prime a two star" end text end define end math
then math define tex of lemma prime a two star as text "{A2'}^*" end text end define end math
end "
, then the modus ponens is not necessary.
\display{"
begin math define statement of lemma prime a two star 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 peano imply metavar var h end metavar peano imply metavar var b end metavar end define end math
end "}
"
begin math define proof of lemma prime a two star 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 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 end quote state proof state cache var c end expand end define end math
end "
\subsection{Lemma "
begin math lemma double hyp end math
end "}
The lemma
"
begin math define pyk of lemma double hyp as text "lemma double hyp" end text end define end math
then math define tex of lemma double hyp as text "Double Hypothesis" end text end define end math
end "
is used during the deduction algorithm, when one wishes to add a hypothesis, "
begin math metavar var h end metavar end math
end ",
to a proof line of the form "
begin math metavar var a end metavar peano imply metavar var b end metavar end math
end ". This will shorten the proof
by one line.
\display{"
begin math define statement of lemma double hyp as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var h end metavar indeed 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 peano imply metavar var h end metavar peano imply metavar var b end metavar end define end math
end "}
"
begin math define proof of lemma double hyp as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var h end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer lemma prime a one star modus ponens 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 b end metavar cut lemma prime a two star 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 end quote state proof state cache var c end expand end define end math
end "
\subsection{Lemma "
begin math lemma one point eight end math
end "}
Lemma
"
begin math define pyk of lemma one point eight as text "lemma one point eight" end text end define end math
then math define tex of lemma one point eight as text "L1.8" end text end define end math
end "
from \cite{mendelson} page 36, is used to introduce the premise at the start of the deduction
algorithm.
\display{
"
begin math define statement of lemma one point eight 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 "}
"
begin math define proof of lemma one point eight 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 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 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 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 "
\subsection{Lemma "
begin math tautology one end math
end "}
The lemma that I call
"
begin math define pyk of tautology one as text "tautology one" end text end define end math
then math define tex of tautology one as text "Tautology 1" end text end define end math
end "
is an all-round useful lemma.
\display{"
begin math define statement of tautology 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 imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
"
begin math define proof of tautology one as lambda var c dot lambda var x dot proof expand quote 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 infer axiom prime a two conclude 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 cut rule prime mp modus ponens 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 modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude 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 cut axiom prime a one conclude 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 peano imply metavar var b 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 cut rule prime mp modus ponens 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 peano imply metavar var b 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 modus ponens 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 conclude metavar var b 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 cut axiom prime a two conclude metavar var b 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 peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var b 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 peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var b 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 conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut axiom prime a one conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\section{The Main Proofs \label{main.lemmas}}
The purpose of this report is the proof of "
begin math lemma prime l three two h end math
end " in section \ref{res.lemma}. In order to get that far
we must first prove a number of the lemmas that precede it in
\cite{mendelson}. Of these lemma "
begin math lemma prime l three two a end math
end " has been proved by Klaus on the peano page and lemma L3.2(e)'
is not needed. Taking into account the support lemmas proved in
section \ref{support}, this leaves parts (b), (c), (d), (f), (g) and
of course (h), still to be proven.
Of these lemmas (f), (g) and (h) are proved using induction, which
means that we will need the Deduction Algorithm.
All of these lemmas are proved in \cite{mendelson}, so the task of
this report has been to rewrite Mendelson's proofs in explicit form
and use the deduction algorithm where necessary.
\subsection{Lemma "
begin math lemma prime l three two b end math
end "}
"
begin math define pyk of lemma prime l three two b as text "lemma prime l three two b" end text end define end math
then math define tex of lemma prime l three two b as text "L3.2(b)'" end text end define end math
end "
\display{"
begin math define statement of lemma prime l three two b as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end define end math
end "}
"
begin math define proof of lemma prime l three two b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed 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 lemma prime l three two a conclude metavar var t end metavar peano is metavar var t end metavar cut corollary one point ten b 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 modus ponens metavar var t end metavar peano is metavar var t end metavar conclude metavar var t end metavar peano is metavar var r 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 "
\subsection{Lemma "
begin math lemma prime l three two c end math
end "}
"
begin math define pyk of lemma prime l three two c as text "lemma prime l three two c" end text end define end math
then math define tex of lemma prime l three two c as text "L3.2(c)'" end text end define end math
end "
\display{"
begin math define statement of lemma prime l three two c as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end define end math
end "}
"
begin math define proof of lemma prime l three two c as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed axiom prime s one conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut lemma prime l three two b conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut corollary one point ten a modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar modus ponens metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define end math
end "
\subsection{Lemma "
begin math lemma prime l three two d end math
end "}
"
begin math define pyk of lemma prime l three two d as text "lemma prime l three two d" end text end define end math
then math define tex of lemma prime l three two d as text "L3.2(d)'" end text end define end math
end "
\display{"
begin math define statement of lemma prime l three two d as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var r end metavar peano is metavar var t end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end define end math
end "}
"
begin math define proof of lemma prime l three two d as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed lemma prime l three two c conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut tautology one modus ponens metavar var r end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut lemma prime l three two b conclude metavar var s end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut corollary one point ten a modus ponens metavar var s end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar modus ponens metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut tautology one modus ponens metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define end math
end "
\subsection{Lemma "
begin math lemma prime l three two f end math
end "}
To prove
"
begin math define pyk of lemma prime l three two f as text "lemma prime l three two f" end text end define end math
then math define tex of lemma prime l three two f as text "L3.2(f)'" end text end define end math
end "
using induction, we will need to prove the base case
"
begin math define pyk of lemma prime l three two f base as text "lemma prime l three two f base" end text end define end math
then math define tex of lemma prime l three two f base as text "{L3.2(f)'}_{BASE}" end text end define end math
end " (section \ref{f.base})
and the induction step
"
begin math define pyk of lemma prime l three two f hyp as text "lemma prime l three two f hyp" end text end define end math
then math define tex of lemma prime l three two f hyp as text "{L3.2(f)'}_{HYP}" end text end define end math
end " (section \ref{f.hyp}).
\display{"
begin math define statement of lemma prime l 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 "}
"
begin math define proof of lemma prime l three two f as lambda var c dot lambda var x dot proof expand quote system prime s infer lemma prime l three two f base conclude peano zero peano is peano zero peano plus peano zero cut lemma prime l three two f hyp 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 "
\subsubsection{The base case of "
begin math lemma prime l three two f end math
end "\label{f.base}}
\display{"
begin math define statement of lemma prime l three two f base as system prime s infer peano zero peano is peano zero peano plus peano zero end define end math
end "}
"
begin math define proof of lemma prime l three two f base as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude peano zero peano plus peano zero peano is peano zero cut lemma prime l three two b conclude peano zero peano plus peano zero peano is peano zero peano imply peano zero peano is peano zero peano plus peano zero cut rule prime mp modus ponens peano zero peano plus peano zero peano is peano zero peano imply peano zero peano is peano zero peano plus peano zero modus ponens peano zero peano plus peano zero peano is peano zero conclude peano zero peano is peano zero peano plus peano zero end quote state proof state cache var c end expand end define end math
end "
\subsubsection{The induction step of "
begin math lemma prime l three two f end math
end "\label{f.hyp}}
\display{"
begin math define statement of lemma prime l three two f hyp 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 peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ end define end math
end "}
"
begin math define proof of lemma prime l three two f hyp as lambda var c dot lambda var x dot proof expand quote system prime s infer lemma one point eight 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 axiom prime s six conclude peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut axiom prime a one conclude peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply 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 rule prime mp modus ponens peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply 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 modus ponens 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 axiom prime s two 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 axiom prime a one 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 peano imply 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 peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut rule prime mp 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 peano imply 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 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 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 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 lemma prime a two star 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 peano imply 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 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 peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut rule prime mp 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 peano imply 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 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 lemma prime l three two d conclude var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut hypothesize modus ponens var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply 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 peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut lemma prime a two star 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 peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply 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 peano imply 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 peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut rule prime mp 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 peano imply 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 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 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 peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut lemma prime a two star 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 peano imply 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 peano imply 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 mp 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 peano imply 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 end quote state proof state cache var c end expand end define end math
end "
\subsection{Lemma "
begin math lemma prime l three two g end math
end "}
To prove
"
begin math define pyk of lemma prime l three two g as text "lemma prime l three two g" end text end define end math
then math define tex of lemma prime l three two g as text "L3.2(g)'" end text end define end math
end "
using induction, we will need to prove the base case
"
begin math define pyk of lemma prime l three two g as text "lemma prime l three two g" end text end define end math
then math define tex of lemma prime l three two g as text "{L3.2(g)'}_{BASE}" end text end define end math
end "(section \ref{g.base})
and the induction step
"
begin math define pyk of lemma prime l three two g hyp as text "lemma prime l three two g hyp" end text end define end math
then math define tex of lemma prime l three two g hyp as text "{L3.2(g)'}_{HYP}" end text end define end math
end "(section \ref{g.hyp}).
\display{"
begin math define statement of lemma prime l three two g as system prime s infer peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ end define end math
end "}
"
begin math define proof of lemma prime l three two g as lambda var c dot lambda var x dot proof expand quote system prime s infer lemma prime l three two g conclude peano all var t peano var indeed var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ cut lemma prime l three two g hyp conclude peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut axiom prime s nine conclude peano all var t peano var indeed var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut rule prime mp modus ponens peano all var t peano var indeed var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ modus ponens peano all var t peano var indeed var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ conclude peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut rule prime mp modus ponens peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ modus ponens peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut rule prime gen modus ponens peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ conclude peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Base case of "
begin math lemma prime l three two g end math
end "\label{g.base}}
\display{"
begin math define statement of lemma prime l three two g as system prime s infer peano all var t peano var indeed var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ end define end math
end "}
"
begin math define proof of lemma prime l three two g as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var t peano var peano succ peano plus peano zero peano is var t peano var peano succ cut axiom prime s five conclude var t peano var peano plus peano zero peano is var t peano var cut axiom prime s two conclude var t peano var peano plus peano zero peano is var t peano var peano imply var t peano var peano plus peano zero peano succ peano is var t peano var peano succ cut rule prime mp modus ponens var t peano var peano plus peano zero peano is var t peano var peano imply var t peano var peano plus peano zero peano succ peano is var t peano var peano succ modus ponens var t peano var peano plus peano zero peano is var t peano var conclude var t peano var peano plus peano zero peano succ peano is var t peano var peano succ cut lemma prime l three two d conclude var t peano var peano succ peano plus peano zero peano is var t peano var peano succ peano imply var t peano var peano plus peano zero peano succ peano is var t peano var peano succ peano imply var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ cut rule prime mp modus ponens var t peano var peano succ peano plus peano zero peano is var t peano var peano succ peano imply var t peano var peano plus peano zero peano succ peano is var t peano var peano succ peano imply var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ modus ponens var t peano var peano succ peano plus peano zero peano is var t peano var peano succ conclude var t peano var peano plus peano zero peano succ peano is var t peano var peano succ peano imply var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ cut rule prime mp modus ponens var t peano var peano plus peano zero peano succ peano is var t peano var peano succ peano imply var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ modus ponens var t peano var peano plus peano zero peano succ peano is var t peano var peano succ conclude var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ cut rule prime gen modus ponens var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ conclude peano all var t peano var indeed var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Induction step of "
begin math lemma prime l three two g end math
end "\label{g.hyp}}
\display{"
begin math define statement of lemma prime l three two g hyp as system prime s infer peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ end define end math
end "}
"
begin math define proof of lemma prime l three two g hyp as lambda var c dot lambda var x dot proof expand quote system prime s infer lemma one point eight conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut axiom prime s six conclude var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ cut lemma prime a one star modus ponens var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ cut axiom prime s two conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime a one star modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime a two star modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut rule prime mp modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime l three two c conclude var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime a one star modus ponens var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime a two star modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut rule prime mp modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime a two star modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut rule prime mp modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut axiom prime s six conclude var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ cut lemma prime a one star modus ponens var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ cut axiom prime s two conclude var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime a one star modus ponens var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime a two star conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut rule prime mp modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime l three two d conclude var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime a one star modus ponens var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime a two star modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut rule prime mp modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime a two star modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut rule prime mp modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut rule prime gen modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ end quote state proof state cache var c end expand end define end math
end "
\subsection{Lemma "
begin math lemma prime l three two h end math
end "\label{res.lemma}}
To prove
"
begin math define pyk of lemma prime l three two h as text "lemma prime l three two h" end text end define end math
then math define tex of lemma prime l three two h as text "L3.2(h)'" end text end define end math
end "
using induction, we will need to prove the base case
"
begin math define pyk of lemma prime l three two h base as text "lemma prime l three two h base" end text end define end math
then math define tex of lemma prime l three two h base as text "{L3.2(h)'}_{BASE}" end text end define end math
end "(section \ref{h.base})
and the induction step
"
begin math define pyk of lemma prime l three two h hyp as text "lemma prime l three two h hyp" end text end define end math
then math define tex of lemma prime l three two h hyp as text "{L3.2(h)'}_{HYP}" end text end define end math
end "(section \ref{h.hyp}).
\display{"
begin math define statement of lemma prime l three two h as system prime s infer peano all var t peano var indeed peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var end define end math
end "}
"
begin math define proof of lemma prime l three two h as lambda var c dot lambda var x dot proof expand quote system prime s infer lemma prime l three two h base conclude peano all var t peano var indeed var t peano var peano plus peano zero peano is peano zero peano plus var t peano var cut lemma prime l three two h hyp conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut axiom prime s nine conclude peano all var t peano var indeed var t peano var peano plus peano zero peano is peano zero peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var cut rule prime mp modus ponens peano all var t peano var indeed var t peano var peano plus peano zero peano is peano zero peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var modus ponens peano all var t peano var indeed var t peano var peano plus peano zero peano is peano zero peano plus var t peano var conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var cut rule prime mp modus ponens peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var modus ponens peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var cut rule prime gen modus ponens peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var conclude peano all var t peano var indeed peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Base case of "
begin math lemma prime l three two h end math
end "\label{h.base}}
\display{"
begin math define statement of lemma prime l three two h base as system prime s infer peano all var t peano var indeed var t peano var peano plus peano zero peano is peano zero peano plus var t peano var end define end math
end "}
"
begin math define proof of lemma prime l three two h base as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var t peano var peano plus peano zero peano is var t peano var cut lemma prime l three two f conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var cut axiom prime a four at var t peano var 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 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 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 conclude var t peano var peano is peano zero peano plus var t peano var cut lemma prime l three two c conclude var t peano var peano plus peano zero peano is var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano plus peano zero peano is peano zero peano plus var t peano var cut rule prime mp modus ponens var t peano var peano plus peano zero peano is var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano plus peano zero peano is peano zero peano plus var t peano var modus ponens var t peano var peano plus peano zero peano is 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 plus peano zero peano is peano zero peano plus var t peano var cut rule prime mp modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano plus peano zero peano is peano zero peano plus var t peano var modus ponens var t peano var peano is peano zero peano plus var t peano var conclude var t peano var peano plus peano zero peano is peano zero peano plus var t peano var cut rule prime gen modus ponens var t peano var peano plus peano zero peano is peano zero peano plus var t peano var conclude peano all var t peano var indeed var t peano var peano plus peano zero 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 "
\subsubsection{Induction step of "
begin math lemma prime l three two h end math
end "\label{h.hyp}}
For proving the induction step, we will need the lemma
"
begin math define pyk of lemma prime l three two h hyp as text "lemma prime l three two h hyp" end text end define end math
then math define tex of lemma prime l three two h hyp as text "L3.2h_{SWAP}" end text end define end math
end ".
\display{"
begin math define statement of lemma prime l three two h hyp as system prime s infer var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ infer var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ end define end math
end "}
"
begin math define proof of lemma prime l three two h hyp as lambda var c dot lambda var x dot proof expand quote system prime s infer var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ infer rule prime gen modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ conclude peano all var t peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut axiom prime a four at var q peano var conclude peano all var t peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var q peano var peano succ peano plus var r peano var peano is var q peano var peano plus var r peano var peano succ cut rule prime mp modus ponens peano all var t peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var q peano var peano succ peano plus var r peano var peano is var q peano var peano plus var r peano var peano succ modus ponens peano all var t peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ conclude var q peano var peano succ peano plus var r peano var peano is var q peano var peano plus var r peano var peano succ cut rule prime gen modus ponens var q peano var peano succ peano plus var r peano var peano is var q peano var peano plus var r peano var peano succ conclude peano all var r peano var indeed var q peano var peano succ peano plus var r peano var peano is var q peano var peano plus var r peano var peano succ cut axiom prime a four at var t peano var conclude peano all var r peano var indeed var q peano var peano succ peano plus var r peano var peano is var q peano var peano plus var r peano var peano succ peano imply var q peano var peano succ peano plus var t peano var peano is var q peano var peano plus var t peano var peano succ cut rule prime mp modus ponens peano all var r peano var indeed var q peano var peano succ peano plus var r peano var peano is var q peano var peano plus var r peano var peano succ peano imply var q peano var peano succ peano plus var t peano var peano is var q peano var peano plus var t peano var peano succ modus ponens peano all var r peano var indeed var q peano var peano succ peano plus var r peano var peano is var q peano var peano plus var r peano var peano succ conclude var q peano var peano succ peano plus var t peano var peano is var q peano var peano plus var t peano var peano succ cut rule prime gen modus ponens var q peano var peano succ peano plus var t peano var peano is var q peano var peano plus var t peano var peano succ conclude peano all var q peano var indeed var q peano var peano succ peano plus var t peano var peano is var q peano var peano plus var t peano var peano succ cut axiom prime a four at var r peano var conclude peano all var q peano var indeed var q peano var peano succ peano plus var t peano var peano is var q peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ cut rule prime mp modus ponens peano all var q peano var indeed var q peano var peano succ peano plus var t peano var peano is var q peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ modus ponens peano all var q peano var indeed var q peano var peano succ peano plus var t peano var peano is var q peano var peano plus var t peano var peano succ conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ end quote state proof state cache var c end expand end define end math
end "\\
$\quad$\\
Now we are ready to prove the induction step.
$\quad$\\
\display{"
begin math define statement of lemma prime l three two h hyp as system prime s infer peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var end define end math
end "}
"
begin math define proof of lemma prime l three two h hyp as lambda var c dot lambda var x dot proof expand quote system prime s infer lemma one point eight conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var cut axiom prime s six conclude var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ cut lemma prime a one star modus ponens var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ cut axiom prime s two conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut lemma double hyp modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut rule prime mp modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut lemma prime l three two c conclude var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut lemma double hyp modus ponens var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut rule prime mp modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut lemma prime a two star modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut rule prime mp modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut lemma prime l three two d conclude var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut lemma double hyp modus ponens var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut rule prime mp modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut lemma prime l three two g conclude peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut axiom prime a four at var t peano var conclude peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut axiom prime a four at var t peano var conclude peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut rule prime mp modus ponens peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ modus ponens peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ conclude peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut axiom prime a four at var r peano var conclude peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut rule prime mp modus ponens peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ modus ponens peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut lemma prime l three two h hyp modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ cut lemma prime a one star modus ponens var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ cut lemma prime a two star modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut rule prime mp modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut rule prime gen modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var end quote state proof state cache var c end expand end define end math
end "
\section{Conclusion}
We have now successfully proved the lemma:
\begin{center}
"
begin math define statement of lemma prime l three two h as system prime s infer peano all var t peano var indeed peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var end define end math
end "
\end{center}
In retrospect some of the proofs could have been made shorter/simpler,
but this does not alter the fact that the LogiWeb system has verified that
this text is correct.
\clearpage
\appendix
\section{The name of the page}
This defines the name of the page:
\display{"
begin math define pyk of logik rapport as text "logik rapport" end text end define end math
end "}
\section{The Bibliography}
\begin{thebibliography}{99}
\bibitem[Mendelson, 2001]{mendelson} E. Mendelson,\\
Introduction to Mathematical Logic, fourth edition.\\
Chapman and Hall 2001.
\end{thebibliography}
\end{document}
End of file
File page.sty
% thebibliography environment from
% /usr/share/texmf/tex/latex/base/book.cls
% with \chapter removed
End of file
latex page
latex page
latex page"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,