"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 peano t indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t end parenthesis end math
end "
}
}
\author {Kasper Frederiksen, tofu@diku.dk}
\maketitle
\tableofcontents
"
begin ragged right expansion
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 in theory system prime s lemma lemma prime l three two h says peano all peano t indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t end parenthesis end lemma 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 meta a end math
end ", "
begin math meta b end math
end ", "
begin math meta c end math
end ",$\ldots$\\
$ \mathrm{ specific terms }: a, b, c, ... $ & $\to$ & "
begin math peano a end math
end ", "
begin math peano b end math
end ", "
begin math peano c end math
end ",$\ldots$\\
$ \forall a: a + 0 = a $ & $\to$ & "
begin math peano all peano a indeed parenthesis peano a peano plus peano zero peano is peano a end parenthesis end math
end " \\
$ \neg(1 \cdot 0 = 1) $ & $\to$ & "
begin math peano not parenthesis peano one peano times peano zero peano is peano one end parenthesis 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 one 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 theory system prime s end theory end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a one says all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a two says all meta a indeed all meta b indeed all meta c indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a three says all meta a indeed all meta b indeed parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a four says all meta c indeed all meta a indeed all meta x indeed all meta b indeed peano sub quote meta a end quote is quote meta b end quote where quote meta x end quote is quote meta c end quote end sub endorse peano all meta x indeed meta b peano imply meta a end rule end math
end "}
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 peano t end math
end "
$\to$
"
begin math peano all peano q indeed peano q peano is peano q peano imply peano t peano is peano t end math
end "
\display{"
begin math in theory system prime s rule axiom prime a five says all meta x indeed all meta a indeed all meta b indeed peano nonfree quote meta x end quote in quote meta a end quote end nonfree endorse peano all meta x indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply peano all meta x indeed meta b end rule end math
end "}
This axiom is not used in this report.
\display{"
begin math in theory system prime s rule rule prime mp says all meta a indeed all meta b indeed meta a peano imply meta b infer meta a infer meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule rule prime gen says all meta x indeed all meta a indeed meta a infer peano all meta x indeed meta a end rule end math
end "}
This is the generalization rule, that allows us to add a universal kvantor in front
of a proof line.
\display{"
begin math in theory system prime s rule axiom prime s one says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta a peano is meta c peano imply meta b peano is meta c end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s two says all meta a indeed all meta b indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s three says all meta a indeed not peano zero peano is meta a peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s four says all meta a indeed all meta b indeed meta a peano succ peano is meta b peano succ peano imply meta a peano is meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s five says all meta a indeed meta a peano plus peano zero peano is meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s six says all meta a indeed all meta b indeed meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s seven says all meta a indeed meta a peano times peano zero peano is peano zero end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s eight says all meta a indeed all meta b indeed meta a peano times parenthesis meta b peano succ end parenthesis peano is parenthesis meta a peano times meta b end parenthesis peano plus meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s nine says all meta a indeed all meta b indeed all meta c indeed all meta x indeed macro newline peano sub meta b is meta a where meta x is peano zero end sub endorse peano sub meta c is meta a where meta x is meta x peano succ end sub endorse macro newline meta b peano imply peano all meta x indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta x indeed meta a end rule end math
end "}
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 parenthesis meta b infer meta c end parenthesis end math
end ",
in to a proof of the lemma
"
begin math system prime s infer meta b peano imply meta c 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 intro corollary one point ten a index "C1.10a" pyk "corollary one point ten a" tex "C1.10a" end intro
end "
is taken from \cite{mendelson} page 38.
\display{"
begin math in theory system prime s lemma corollary one point ten a says all meta b indeed all meta c indeed all meta d indeed parenthesis meta b peano imply meta c infer meta c peano imply meta d infer meta b peano imply meta d end parenthesis end lemma end math
end "}
"
begin math system prime s proof of corollary one point ten a reads arbitrary meta b end line arbitrary meta c end line arbitrary meta d end line line ell a premise meta b peano imply meta c end line line ell b premise meta c peano imply meta d end line line ell c because axiom prime a one indeed parenthesis meta c peano imply meta d end parenthesis peano imply parenthesis meta b peano imply parenthesis meta c peano imply meta d end parenthesis end parenthesis end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed meta b peano imply parenthesis meta c peano imply meta d end parenthesis end line line ell e because axiom prime a two indeed parenthesis meta b peano imply parenthesis meta c peano imply meta d end parenthesis end parenthesis peano imply parenthesis parenthesis meta b peano imply meta c end parenthesis peano imply parenthesis meta b peano imply meta d end parenthesis end parenthesis end line line ell f because rule prime mp modus ponens ell e modus ponens ell d indeed parenthesis meta b peano imply meta c end parenthesis peano imply parenthesis meta b peano imply meta d end parenthesis end line because rule prime mp modus ponens ell f modus ponens ell a indeed meta b peano imply meta d qed end math
end "
\subsection{Corollary "
begin math corollary one point ten b end math
end "}
The lemma
"
begin intro corollary one point ten b index "C1.10(b)" pyk "corollary one point ten b" tex "C1.10(b)" end intro
end "
is taken from \cite{mendelson} page 38.
\display{"
begin math in theory system prime s lemma corollary one point ten b says all meta b indeed all meta c indeed all meta d indeed parenthesis meta b peano imply parenthesis meta c peano imply meta d end parenthesis infer meta c infer meta b peano imply meta d end parenthesis end lemma end math
end "}
"
begin math system prime s proof of corollary one point ten b reads arbitrary meta b end line arbitrary meta c end line arbitrary meta d end line line ell a premise meta b peano imply parenthesis meta c peano imply meta d end parenthesis end line line ell b premise meta c end line line ell c because axiom prime a one indeed meta c peano imply parenthesis meta b peano imply meta c end parenthesis end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed meta b peano imply meta c end line line ell e because axiom prime a two indeed parenthesis meta b peano imply parenthesis meta c peano imply meta d end parenthesis end parenthesis peano imply parenthesis parenthesis meta b peano imply meta c end parenthesis peano imply parenthesis meta b peano imply meta d end parenthesis end parenthesis end line line ell f because rule prime mp modus ponens ell e modus ponens ell a indeed parenthesis meta b peano imply meta c end parenthesis peano imply parenthesis meta b peano imply meta d end parenthesis end line because rule prime mp modus ponens ell f modus ponens ell d indeed meta b peano imply meta d qed end math
end "
\subsection{Lemma "
begin math lemma prime a one star end math
end "}
The lemma
"
begin intro lemma prime a one star index "{A1'}^*" pyk "lemma prime a one star" tex "{A1'}^*" end intro
end "
is used during the deduction algorithm, when one wishes to add a hypothesis, "
begin math meta h end math
end ", to a
line of a proof. This will shorten the proof by one line.
\display{"
begin math in theory system prime s lemma lemma prime a one star says all meta a indeed all meta h indeed parenthesis meta a infer meta h peano imply meta a end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime a one star reads arbitrary meta a end line arbitrary meta h end line line ell a premise meta a end line line ell b because axiom prime a one indeed meta a peano imply parenthesis meta h peano imply meta a end parenthesis end line because rule prime mp modus ponens ell b modus ponens ell a indeed meta h peano imply meta a qed 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 intro lemma prime a two star index "{A2'}^*" pyk "lemma prime a two star" tex "{A2'}^*" end intro
end "
, then the modus ponens is not necessary.
\display{"
begin math in theory system prime s lemma lemma prime a two star says all meta h indeed all meta a indeed all meta b indeed parenthesis meta h peano imply parenthesis meta a peano imply meta b end parenthesis end parenthesis infer parenthesis parenthesis meta h peano imply meta a end parenthesis peano imply parenthesis meta h peano imply meta b end parenthesis end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime a two star reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line line ell a premise meta h peano imply parenthesis meta a peano imply meta b end parenthesis end line line ell b because axiom prime a two indeed parenthesis meta h peano imply parenthesis meta a peano imply meta b end parenthesis end parenthesis peano imply parenthesis parenthesis meta h peano imply meta a end parenthesis peano imply parenthesis meta h peano imply meta b end parenthesis end parenthesis end line because rule prime mp modus ponens ell b modus ponens ell a indeed parenthesis meta h peano imply meta a end parenthesis peano imply parenthesis meta h peano imply meta b end parenthesis qed end math
end "
\subsection{Lemma "
begin math lemma double hyp end math
end "}
The lemma
"
begin intro lemma double hyp index "Double Hypothesis" pyk "lemma double hyp" tex "Double Hypothesis" end intro
end "
is used during the deduction algorithm, when one wishes to add a hypothesis, "
begin math meta h end math
end ",
to a proof line of the form "
begin math meta a peano imply meta b end math
end ". This will shorten the proof
by one line.
\display{"
begin math in theory system prime s lemma lemma double hyp says all meta a indeed all meta b indeed all meta h indeed parenthesis meta a peano imply meta b infer parenthesis parenthesis meta h peano imply meta a end parenthesis peano imply parenthesis meta h peano imply meta b end parenthesis end parenthesis end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma double hyp reads arbitrary meta a end line arbitrary meta b end line arbitrary meta h end line line ell a premise meta a peano imply meta b end line line ell b because lemma prime a one star modus ponens ell a indeed meta h peano imply parenthesis meta a peano imply meta b end parenthesis end line because lemma prime a two star modus ponens ell b indeed parenthesis meta h peano imply meta a end parenthesis peano imply parenthesis meta h peano imply meta b end parenthesis qed end math
end "
\subsection{Lemma "
begin math lemma one point eight end math
end "}
Lemma
"
begin intro lemma one point eight index "L1.8" pyk "lemma one point eight" tex "L1.8" end intro
end "
from \cite{mendelson} page 36, is used to introduce the premise at the start of the deduction
algorithm.
\display{
"
begin math in theory system prime s lemma lemma one point eight says all meta b indeed parenthesis meta b peano imply meta b end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma one point eight reads arbitrary meta b end line line ell a because axiom prime a two indeed parenthesis meta b peano imply parenthesis parenthesis meta b peano imply meta b end parenthesis peano imply meta b end parenthesis end parenthesis peano imply parenthesis parenthesis meta b peano imply parenthesis meta b peano imply meta b end parenthesis end parenthesis peano imply parenthesis meta b peano imply meta b end parenthesis end parenthesis end line line ell b because axiom prime a one indeed meta b peano imply parenthesis parenthesis meta b peano imply meta b end parenthesis peano imply meta b end parenthesis end line line ell c because rule prime mp modus ponens ell a modus ponens ell b indeed parenthesis meta b peano imply parenthesis meta b peano imply meta b end parenthesis end parenthesis peano imply parenthesis meta b peano imply meta b end parenthesis end line line ell d because axiom prime a one indeed meta b peano imply parenthesis meta b peano imply meta b end parenthesis end line because rule prime mp modus ponens ell c modus ponens ell d indeed meta b peano imply meta b qed end math
end "
\subsection{Lemma "
begin math tautology one end math
end "}
The lemma that I call
"
begin intro tautology one index "Tautology 1" pyk "tautology one" tex "Tautology 1" end intro
end "
is an all-round useful lemma.
\display{"
begin math in theory system prime s lemma tautology one says all meta a indeed all meta b indeed all meta c indeed parenthesis parenthesis meta a peano imply parenthesis meta b peano imply meta c end parenthesis end parenthesis infer parenthesis meta b peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end parenthesis end lemma end math
end "}
"
begin math system prime s proof of tautology one reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply parenthesis meta b peano imply meta c end parenthesis end line line ell b because axiom prime a two indeed parenthesis meta a peano imply parenthesis meta b peano imply meta c end parenthesis end parenthesis peano imply parenthesis parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end line line ell c because rule prime mp modus ponens ell b modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end line line ell d because axiom prime a one indeed parenthesis parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis peano imply parenthesis meta b peano imply parenthesis parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end parenthesis end line line ell e because rule prime mp modus ponens ell d modus ponens ell c indeed meta b peano imply parenthesis parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end line line ell f because axiom prime a two indeed parenthesis meta b peano imply parenthesis parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end parenthesis peano imply parenthesis parenthesis meta b peano imply parenthesis meta a peano imply meta b end parenthesis end parenthesis peano imply parenthesis meta b peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end parenthesis end line line ell g because rule prime mp modus ponens ell f modus ponens ell e indeed parenthesis meta b peano imply parenthesis meta a peano imply meta b end parenthesis end parenthesis peano imply parenthesis meta b peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end line line ell h because axiom prime a one indeed meta b peano imply parenthesis meta a peano imply meta b end parenthesis end line because rule prime mp modus ponens ell g modus ponens ell h indeed meta b peano imply parenthesis meta a peano imply meta c end parenthesis qed 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 intro lemma prime l three two b index "L3.2(b)'" pyk "lemma prime l three two b" tex "L3.2(b)'" end intro
end "
\display{"
begin math in theory system prime s lemma lemma prime l three two b says all meta t indeed all meta r indeed meta t peano is meta r peano imply meta r peano is meta t end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two b reads arbitrary meta t end line arbitrary meta r end line line ell a because axiom prime s one indeed meta t peano is meta r peano imply parenthesis meta t peano is meta t peano imply meta r peano is meta t end parenthesis end line line ell b because lemma prime l three two a indeed meta t peano is meta t end line because corollary one point ten b modus ponens ell a modus ponens ell b indeed meta t peano is meta r peano imply meta r peano is meta t qed end math
end "
\subsection{Lemma "
begin math lemma prime l three two c end math
end "}
"
begin intro lemma prime l three two c index "L3.2(c)'" pyk "lemma prime l three two c" tex "L3.2(c)'" end intro
end "
\display{"
begin math in theory system prime s lemma lemma prime l three two c says all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r peano imply parenthesis meta r peano is meta s peano imply meta t peano is meta s end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two c reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a because axiom prime s one indeed meta r peano is meta t peano imply parenthesis meta r peano is meta s peano imply meta t peano is meta s end parenthesis end line line ell b because lemma prime l three two b indeed meta t peano is meta r peano imply meta r peano is meta t end line because corollary one point ten a modus ponens ell b modus ponens ell a indeed meta t peano is meta r peano imply parenthesis meta r peano is meta s peano imply meta t peano is meta s end parenthesis qed end math
end "
\subsection{Lemma "
begin math lemma prime l three two d end math
end "}
"
begin intro lemma prime l three two d index "L3.2(d)'" pyk "lemma prime l three two d" tex "L3.2(d)'" end intro
end "
\display{"
begin math in theory system prime s lemma lemma prime l three two d says all meta t indeed all meta r indeed all meta s indeed meta r peano is meta t peano imply parenthesis meta s peano is meta t peano imply meta r peano is meta s end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two d reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a because lemma prime l three two c indeed meta r peano is meta t peano imply parenthesis meta t peano is meta s peano imply meta r peano is meta s end parenthesis end line line ell b because tautology one modus ponens ell a indeed meta t peano is meta s peano imply parenthesis meta r peano is meta t peano imply meta r peano is meta s end parenthesis end line line ell c because lemma prime l three two b indeed meta s peano is meta t peano imply meta t peano is meta s end line line ell d because corollary one point ten a modus ponens ell c modus ponens ell b indeed meta s peano is meta t peano imply parenthesis meta r peano is meta t peano imply meta r peano is meta s end parenthesis end line because tautology one modus ponens ell d indeed meta r peano is meta t peano imply parenthesis meta s peano is meta t peano imply meta r peano is meta s end parenthesis qed end math
end "
\subsection{Lemma "
begin math lemma prime l three two f end math
end "}
To prove
"
begin intro lemma prime l three two f index "L3.2(f)'" pyk "lemma prime l three two f" tex "L3.2(f)'" end intro
end "
using induction, we will need to prove the base case
"
begin intro lemma prime l three two f base index "{L3.2(f)'}_{BASE}" pyk "lemma prime l three two f base" tex "{L3.2(f)'}_{BASE}" end intro
end " (section \ref{f.base})
and the induction step
"
begin intro lemma prime l three two f hyp index "{L3.2(f)'}_{HYP}" pyk "lemma prime l three two f hyp" tex "{L3.2(f)'}_{HYP}" end intro
end " (section \ref{f.hyp}).
\display{"
begin math in theory system prime s lemma lemma prime l three two f says peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two f reads line ell a because lemma prime l three two f base indeed peano zero peano is peano zero peano plus peano zero end line line ell b because lemma prime l three two f hyp indeed peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end line line ell c because axiom prime s nine indeed parenthesis peano zero peano is peano zero peano plus peano zero end parenthesis peano imply parenthesis parenthesis peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end parenthesis peano imply parenthesis peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t end parenthesis end parenthesis end parenthesis end line line ell d because rule prime mp modus ponens ell c modus ponens ell a indeed parenthesis peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end parenthesis peano imply parenthesis peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t end parenthesis end parenthesis end line because rule prime mp modus ponens ell d modus ponens ell b indeed peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t end parenthesis qed 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 in theory system prime s lemma lemma prime l three two f base says peano zero peano is peano zero peano plus peano zero end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two f base reads line ell a because axiom prime s five indeed peano zero peano plus peano zero peano is peano zero end line line ell b because lemma prime l three two b indeed peano zero peano plus peano zero peano is peano zero peano imply peano zero peano is peano zero peano plus peano zero end line because rule prime mp modus ponens ell b modus ponens ell a indeed peano zero peano is peano zero peano plus peano zero qed 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 in theory system prime s lemma lemma prime l three two f hyp says peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two f hyp reads line ell a because lemma one point eight indeed peano t peano is peano zero peano plus peano t peano imply peano t peano is peano zero peano plus peano t end line line ell b because axiom prime s six indeed peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell c because axiom prime a one indeed parenthesis peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end parenthesis peano imply parenthesis peano t peano is peano zero peano plus peano t peano imply parenthesis peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end parenthesis end parenthesis end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed peano t peano is peano zero peano plus peano t peano imply parenthesis peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end parenthesis end line line ell e because axiom prime s two indeed peano t peano is parenthesis peano zero peano plus peano t end parenthesis peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell f because axiom prime a one indeed parenthesis peano t peano is parenthesis peano zero peano plus peano t end parenthesis peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end parenthesis peano imply parenthesis peano t peano is peano zero peano plus peano t peano imply parenthesis peano t peano is parenthesis peano zero peano plus peano t end parenthesis peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end parenthesis end parenthesis end line line ell g because rule prime mp modus ponens ell f modus ponens ell e indeed peano t peano is peano zero peano plus peano t peano imply parenthesis peano t peano is parenthesis peano zero peano plus peano t end parenthesis peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end parenthesis end line line ell h because lemma prime a two star modus ponens ell g indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano is peano zero peano plus peano t end parenthesis peano imply parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end parenthesis end line line ell i because rule prime mp modus ponens ell h modus ponens ell a indeed peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell j because lemma prime l three two d indeed peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply parenthesis peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end line line ell k because hypothesize modus ponens ell j indeed peano t peano is peano zero peano plus peano t peano imply parenthesis peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply parenthesis peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end parenthesis end line line ell l because lemma prime a two star modus ponens ell k indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end parenthesis peano imply parenthesis peano t peano is peano zero peano plus peano t peano imply parenthesis peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end parenthesis end line line ell m because rule prime mp modus ponens ell l modus ponens ell i indeed peano t peano is peano zero peano plus peano t peano imply parenthesis peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end line line ell n because lemma prime a two star modus ponens ell m indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end parenthesis peano imply parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end line line ell o because rule prime mp modus ponens ell n modus ponens ell d indeed peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end line because rule prime gen modus ponens ell o indeed peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis qed end math
end "
\subsection{Lemma "
begin math lemma prime l three two g end math
end "}
To prove
"
begin intro lemma prime l three two g index "L3.2(g)'" pyk "lemma prime l three two g" tex "L3.2(g)'" end intro
end "
using induction, we will need to prove the base case
"
begin intro lemma prime l three two g index "{L3.2(g)'}_{BASE}" pyk "lemma prime l three two g" tex "{L3.2(g)'}_{BASE}" end intro
end "(section \ref{g.base})
and the induction step
"
begin intro lemma prime l three two g hyp index "{L3.2(g)'}_{HYP}" pyk "lemma prime l three two g hyp" tex "{L3.2(g)'}_{HYP}" end intro
end "(section \ref{g.hyp}).
\display{"
begin math in theory system prime s lemma lemma prime l three two g says peano all peano t indeed peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two g reads line ell a because lemma prime l three two g indeed peano all peano t indeed parenthesis peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end parenthesis end line line ell b because lemma prime l three two g hyp indeed peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis end line line ell c because axiom prime s nine indeed peano all peano t indeed parenthesis peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end parenthesis peano imply parenthesis peano all peano r indeed parenthesis parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano imply parenthesis peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis end parenthesis peano imply parenthesis peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis end parenthesis end parenthesis end line line ell d because rule prime mp modus ponens ell c modus ponens ell a indeed peano all peano r indeed parenthesis parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano imply parenthesis peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis end parenthesis peano imply parenthesis peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis end parenthesis end line line ell e because rule prime mp modus ponens ell d modus ponens ell b indeed peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis end line because rule prime gen modus ponens ell e indeed peano all peano t indeed peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis qed end math
end "
\subsubsection{Base case of "
begin math lemma prime l three two g end math
end "\label{g.base}}
\display{"
begin math in theory system prime s lemma lemma prime l three two g says peano all peano t indeed parenthesis peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two g reads line ell a because axiom prime s five indeed peano t peano succ peano plus peano zero peano is peano t peano succ end line line ell b because axiom prime s five indeed peano t peano plus peano zero peano is peano t end line line ell c because axiom prime s two indeed peano t peano plus peano zero peano is peano t peano imply parenthesis peano t peano plus peano zero end parenthesis peano succ peano is peano t peano succ end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed parenthesis peano t peano plus peano zero end parenthesis peano succ peano is peano t peano succ end line line ell e because lemma prime l three two d indeed parenthesis peano t peano succ peano plus peano zero end parenthesis peano is peano t peano succ peano imply parenthesis parenthesis peano t peano plus peano zero end parenthesis peano succ peano is peano t peano succ peano imply parenthesis peano t peano succ peano plus peano zero end parenthesis peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end parenthesis end line line ell f because rule prime mp modus ponens ell e modus ponens ell a indeed parenthesis peano t peano plus peano zero end parenthesis peano succ peano is peano t peano succ peano imply parenthesis peano t peano succ peano plus peano zero end parenthesis peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end line line ell g because rule prime mp modus ponens ell f modus ponens ell d indeed peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end line because rule prime gen modus ponens ell g indeed peano all peano t indeed parenthesis peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end parenthesis qed end math
end "
\subsubsection{Induction step of "
begin math lemma prime l three two g end math
end "\label{g.hyp}}
\display{"
begin math in theory system prime s lemma lemma prime l three two g hyp says peano all peano r indeed parenthesis parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano imply parenthesis peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two g hyp reads locally define meta h as peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell a because lemma one point eight indeed meta h peano imply meta h end line line ell b because axiom prime s six indeed peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ end line line ell c because lemma prime a one star modus ponens ell b indeed meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ end line line ell d because axiom prime s two indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end line line ell e because lemma prime a one star modus ponens ell d indeed meta h peano imply parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis end line line ell f because lemma prime a two star modus ponens ell e indeed parenthesis meta h peano imply peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano imply parenthesis meta h peano imply parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis end line line ell g because rule prime mp modus ponens ell f modus ponens ell a indeed meta h peano imply parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end line line ell h because lemma prime l three two c indeed peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano imply parenthesis parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis end line line ell i because lemma prime a one star modus ponens ell h indeed meta h peano imply parenthesis peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano imply parenthesis parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis end parenthesis end line line ell j because lemma prime a two star modus ponens ell i indeed parenthesis meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ end parenthesis peano imply parenthesis meta h peano imply parenthesis parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis end parenthesis end line line ell k because rule prime mp modus ponens ell j modus ponens ell c indeed meta h peano imply parenthesis parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis end line line ell l because lemma prime a two star modus ponens ell k indeed parenthesis meta h peano imply parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis peano imply parenthesis meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis end line line ell m because rule prime mp modus ponens ell l modus ponens ell g indeed meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end line line ell n because axiom prime s six indeed peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell o because lemma prime a one star modus ponens ell n indeed meta h peano imply peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell p because axiom prime s two indeed peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end line line ell q because lemma prime a one star modus ponens ell p indeed meta h peano imply parenthesis peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis end line line ell r because lemma prime a two star indeed parenthesis meta h peano imply peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano imply parenthesis meta h peano imply parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis end line line ell s because rule prime mp modus ponens ell r modus ponens ell o indeed meta h peano imply parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end line line ell t because lemma prime l three two d indeed peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ peano imply parenthesis parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis end line line ell u because lemma prime a one star modus ponens ell t indeed meta h peano imply parenthesis peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ peano imply parenthesis parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis end parenthesis end line line ell v because lemma prime a two star modus ponens ell u indeed parenthesis meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis peano imply parenthesis meta h peano imply parenthesis parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis end parenthesis end line line ell w because rule prime mp modus ponens ell v modus ponens ell m indeed meta h peano imply parenthesis parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis end line line ell x because lemma prime a two star modus ponens ell w indeed parenthesis meta h peano imply parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end parenthesis peano imply parenthesis meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis end line line ell y because rule prime mp modus ponens ell x modus ponens ell s indeed meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end line because rule prime gen modus ponens ell y indeed peano all peano r indeed parenthesis meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis qed end math
end "
\subsection{Lemma "
begin math lemma prime l three two h end math
end "\label{res.lemma}}
To prove
"
begin intro lemma prime l three two h index "L3.2(h)'" pyk "lemma prime l three two h" tex "L3.2(h)'" end intro
end "
using induction, we will need to prove the base case
"
begin intro lemma prime l three two h base index "{L3.2(h)'}_{BASE}" pyk "lemma prime l three two h base" tex "{L3.2(h)'}_{BASE}" end intro
end "(section \ref{h.base})
and the induction step
"
begin intro lemma prime l three two h hyp index "{L3.2(h)'}_{HYP}" pyk "lemma prime l three two h hyp" tex "{L3.2(h)'}_{HYP}" end intro
end "(section \ref{h.hyp}).
\display{"
begin math in theory system prime s lemma lemma prime l three two h says peano all peano t indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two h reads line ell a because lemma prime l three two h base indeed peano all peano t indeed parenthesis peano t peano plus peano zero peano is peano zero peano plus peano t end parenthesis end line line ell b because lemma prime l three two h hyp indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis end line line ell c because axiom prime s nine indeed peano all peano t indeed parenthesis peano t peano plus peano zero peano is peano zero peano plus peano t end parenthesis peano imply parenthesis parenthesis peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis end parenthesis peano imply peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t end parenthesis end parenthesis end line line ell d because rule prime mp modus ponens ell c modus ponens ell a indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis peano imply peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t end parenthesis end line line ell e because rule prime mp modus ponens ell d modus ponens ell b indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t end parenthesis end line because rule prime gen modus ponens ell e indeed peano all peano t indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t end parenthesis qed end math
end "
\subsubsection{Base case of "
begin math lemma prime l three two h end math
end "\label{h.base}}
\display{"
begin math in theory system prime s lemma lemma prime l three two h base says peano all peano t indeed parenthesis peano t peano plus peano zero peano is peano zero peano plus peano t end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two h base reads line ell a because axiom prime s five indeed peano t peano plus peano zero peano is peano t end line line ell b because lemma prime l three two f indeed peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t end parenthesis end line line ell c because axiom prime a four at peano t indeed parenthesis peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t end parenthesis end parenthesis peano imply parenthesis peano t peano is peano zero peano plus peano t end parenthesis end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed peano t peano is peano zero peano plus peano t end line line ell e because lemma prime l three two c indeed peano t peano plus peano zero peano is peano t peano imply parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano plus peano zero peano is peano zero peano plus peano t end parenthesis end line line ell f because rule prime mp modus ponens ell e modus ponens ell a indeed peano t peano is peano zero peano plus peano t peano imply peano t peano plus peano zero peano is peano zero peano plus peano t end line line ell g because rule prime mp modus ponens ell f modus ponens ell d indeed peano t peano plus peano zero peano is peano zero peano plus peano t end line because rule prime gen modus ponens ell g indeed peano all peano t indeed parenthesis peano t peano plus peano zero peano is peano zero peano plus peano t end parenthesis qed 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 intro lemma prime l three two h hyp index "L3.2h_{SWAP}" pyk "lemma prime l three two h hyp" tex "L3.2h_{SWAP}" end intro
end ".
\display{"
begin math in theory system prime s lemma lemma prime l three two h hyp says peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ infer peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two h hyp reads line ell a premise peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell b because rule prime gen modus ponens ell a indeed peano all peano t indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis end line line ell c because axiom prime a four at peano q indeed peano all peano t indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano imply peano q peano succ peano plus peano r peano is parenthesis peano q peano plus peano r end parenthesis peano succ end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed peano q peano succ peano plus peano r peano is parenthesis peano q peano plus peano r end parenthesis peano succ end line line ell e because rule prime gen modus ponens ell d indeed peano all peano r indeed parenthesis peano q peano succ peano plus peano r peano is parenthesis peano q peano plus peano r end parenthesis peano succ end parenthesis end line line ell f because axiom prime a four at peano t indeed peano all peano r indeed parenthesis peano q peano succ peano plus peano r peano is parenthesis peano q peano plus peano r end parenthesis peano succ end parenthesis peano imply peano q peano succ peano plus peano t peano is parenthesis peano q peano plus peano t end parenthesis peano succ end line line ell g because rule prime mp modus ponens ell f modus ponens ell e indeed peano q peano succ peano plus peano t peano is parenthesis peano q peano plus peano t end parenthesis peano succ end line line ell h because rule prime gen modus ponens ell g indeed peano all peano q indeed parenthesis peano q peano succ peano plus peano t peano is parenthesis peano q peano plus peano t end parenthesis peano succ end parenthesis end line line ell i because axiom prime a four at peano r indeed peano all peano q indeed parenthesis peano q peano succ peano plus peano t peano is parenthesis peano q peano plus peano t end parenthesis peano succ end parenthesis peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line because rule prime mp modus ponens ell i modus ponens ell h indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ qed end math
end "\\
$\quad$\\
Now we are ready to prove the induction step.
$\quad$\\
\display{"
begin math in theory system prime s lemma lemma prime l three two h hyp says peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis end lemma end math
end "}
"
begin math system prime s proof of lemma prime l three two h hyp reads locally define meta h as peano t peano plus peano r peano is peano r peano plus peano t end line line ell a because lemma one point eight indeed meta h peano imply meta h end line line ell b because axiom prime s six indeed peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell c because lemma prime a one star modus ponens ell b indeed meta h peano imply peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell d because axiom prime s two indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell e because lemma double hyp modus ponens ell d indeed parenthesis meta h peano imply peano t peano plus peano r peano is peano r peano plus peano t end parenthesis peano imply parenthesis meta h peano imply parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis end parenthesis end line line ell e because rule prime mp modus ponens ell e modus ponens ell a indeed meta h peano imply parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis end line line ell f because lemma prime l three two c indeed peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis end line line ell g because lemma double hyp modus ponens ell f indeed parenthesis meta h peano imply peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano imply parenthesis meta h peano imply parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis end parenthesis end line line ell h because rule prime mp modus ponens ell g modus ponens ell c indeed meta h peano imply parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis end line line ell i because lemma prime a two star modus ponens ell h indeed parenthesis meta h peano imply parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano imply parenthesis meta h peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis end line line ell j because rule prime mp modus ponens ell i modus ponens ell e indeed meta h peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell k because lemma prime l three two d indeed peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis end line line ell l because lemma double hyp modus ponens ell k indeed parenthesis meta h peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano imply parenthesis meta h peano imply parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis end parenthesis end line line ell m because rule prime mp modus ponens ell l modus ponens ell j indeed meta h peano imply parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis end line line ell n because lemma prime l three two g indeed peano all peano t indeed peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis end line line ell o because axiom prime a four at peano t indeed peano all peano t indeed peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano imply peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis end line line ell o because axiom prime a four at peano t indeed peano all peano t indeed peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano imply peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis end line line ell p because rule prime mp modus ponens ell o modus ponens ell n indeed peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis end line line ell q because axiom prime a four at peano r indeed peano all peano r indeed parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano imply parenthesis peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis end line line ell r because rule prime mp modus ponens ell q modus ponens ell p indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell big r because lemma prime l three two h hyp modus ponens ell r indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell s because lemma prime a one star modus ponens ell big r indeed meta h peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell t because lemma prime a two star modus ponens ell m indeed parenthesis meta h peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano imply parenthesis meta h peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis end line line ell u because rule prime mp modus ponens ell t modus ponens ell s indeed meta h peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end line because rule prime gen modus ponens ell u indeed peano all peano r indeed parenthesis meta h peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis qed end math
end "
\section{Conclusion}
We have now successfully proved the lemma:
\begin{center}
"
begin math in theory system prime s lemma lemma prime l three two h says peano all peano t indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t end parenthesis end lemma 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 pyk define logik rapport as "logik rapport" 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,