"File page.sty
% thebibliography environment from
% /usr/share/texmf/tex/latex/base/book.cls
% with \chapter removed
\renewenvironment{thebibliography}[1]
{\list{\@biblabel{\@arabic\c@enumiv}}%
{\settowidth\labelwidth{\@biblabel{#1}}%
\leftmargin\labelwidth
\advance\leftmargin\labelsep
\@openbib@code
\usecounter{enumiv}%
\let\p@enumiv\@empty
\renewcommand\theenumiv{\@arabic\c@enumiv}}%
\sloppy
\clubpenalty4000
\@clubpenalty \clubpenalty
\widowpenalty4000%
\sfcode`\.\@m}
{\def\@noitemerr
{\@latex@warning{Empty `thebibliography' environment}}%
\endlist}
End of file
File page.tex
\documentclass [fleqn]{article}
\setlength {\overfullrule }{1mm}
\input{lgwinclude}
\usepackage{latexsym}
\usepackage[danish]{babel}
\usepackage{euler}
\usepackage{url}
%\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=A Logiweb base page}
\hypersetup{colorlinks=true}
\bibliographystyle{plain}
% \tex{something} writes something to page.otx for later inclusion
\newwrite\outex
\newtoks\toktex
\immediate\openout\outex=page.otx
\newcommand{\tex}[1]{\toktex={\item #1}\immediate\write\outex{\the\toktex}}
% \test{something} writes something to page.tst for later inclusion
\newwrite\outest
\immediate\openout\outest=page.tst
\newcommand{\test}[1]{\toktex={\item #1}\immediate\write\outest{\the\toktex}}
% Concerning \catcode`\@=11 : See the TeXbook, Appendix B (page 344).
% \afterheading suppresses indentation once, c.f. latex.ltx.
% \display{something} displays something as a displayed equation except
% that linebreaking is possible and displaymath is not turned on by default.
% The first paragraph after \display{something} is unindented.
% Glue below formulas may be wrong. The definition of \display misses
% something like \addvspace{\belowdisplayskip}.
\catcode`\@=11
\def\afterheading{\@afterheading}
\catcode`\@=12
\newcommand{\display}[1]{\begin{list}{}{\setlength{\leftmargin}{\mathindent}}
\item #1\end{list}
\afterheading}
\newcommand{\statement}[1]{\begin{list}{}{\setlength{\leftmargin}{0mm}}
\item #1\end{list}
\afterheading}
\begin{document}
\title{Peano Commutativity in "
begin bracket system prime s end bracket
end "}
\author{Martin R{\o}pcke}
\maketitle
\tableofcontents
"
begin ragged right
end "
\newpage
%%%%%%%%%% Introduction %%%%%%%%%%
\section{Introduction}
This report is turned in for credit for the course ``Logic'' at DIKU
summer 2005. In short, the assignment is to prove the commutativity of
addition within peano arithmetic using the Logiweb system developed by
Klaus Grue. Logiweb will be introduced shortly. That is, in this report
we shall carry out a proof of the proposition that for all natural
number the following holds:
\begin{equation}\label{eq:commu}
t + r = r + t,
\end{equation}
and we shall use Klaus Grue's Logiweb system to check our proof.
Cf.~\cite{grue:check}. However, we use "
begin bracket var x peano var end bracket
end " and
"
begin bracket var y peano var end bracket
end " as our variables.
During the course we have been introduced to mathematical logic using
the text book \emph{Introduction to Mathematical Logic} by Elliot
Mendelson, cf.~\cite{mendelson}. In order to get the full of this report
we thus assume an elementary knowledge of logic as it is introduced in
this book. However, we do give short introductions to some basic
topics---Logiweb as well as logic---making this report
selfcontained---at least to a graduate student of computer science at
DIKU.
The report has been written from June 23rd to July 3rd. Due to this
short period of time the proof is carried out as simpel as possible
discarding any fancy solutions even before they have been fully
conceived of. The commutativity of addition is part of Proposition 3.2
in~\cite{mendelson}, p. 156, which is proved immediately afterwards on
pp. 157f. We follow this proof backchaining from the actual proof of
(\ref{eq:commu}) through other results of the proposition and necessary
lemmas and theorems contained in the book. Besides Mendelson's
propositions we only make use of two tautologies and one lemma in the
final proof.
We hope our intentions have been reached and that this report carries
just a little of the fun it has been working with Logiweb. As Klaus
always invites the Logiweb user to we do also: ``Have fun''.
\section{The Logiweb System}
In this section we give a short introduction to the Logiweb system, a
web-based system for distribution of mathematical definitions, lemmas,
and proofs writing web-pages. Cf.~\cite{grue:check}. For further details
and elaboration on the myriad of intricacies and topics concerning the
system we refer to Klaus Grue's introduction to Logiweb, namely the
\href{\lgwCheckUrl}{check} page. Alternatively, we recommend the
\href{\lgwPeanoUrl}{peano} page introducing peano arithmetic, which is
displays well the system ``at work''. In order to obtain a thorough
knowledge of the system one is adviced to follow the course ``Logic'' or
read the \href{\lgwBaseUrl}{base} page (cf.~\cite{grue:base}), but
probably the best choice would be to devour the exercise of writing a
page proving some proposition of choice chosen from~\cite{mendelson}
using Logiweb. After such an exercise any logiweb work and the hardship
of doing so will most likely depend on the level of mathematics one is
working with.
\subsection{References}
As hinted at above Logiweb is a system in which users world wide can
distribute their own mathematical work and reuse the work of others.
Mathematics in Logiweb is publicized by submitting a \emph{logiweb page}
to the Logiweb system, that is, to a \emph{Logiweb server}. Abstractly
speaking, in a logiweb page one can define a mathematical theory or
system\footnote{We shall use \emph{theory} and \emph{system}
interchangeably, as is the case with \emph{Logiweb system} and
\emph{Logiweb}.} and a language of this system within which one can then
define, state, and prove mathematical lemmas, theorems, propositions,
etc. A theory must defined in one page. The proofs within a theory will
be proof checked upon submission (actually they will be proof checked
when compiling the page locally) to the Logiweb system and one then
knows if the contents of a page are correct within the theory. A page
can refer to other logiweb pages in which a needed theory, results,
functionalities etc. are defined. Thus, Logiweb works much like the
world wide web where pages refer to each other using hyperlinks. The
mesh of Logiweb servers translate Logiweb references to http urls making
sure a page can find its references and that they together form a
directed acyclic graph from top (the base) to bottom (a logiweb page).
Essentially, the Logiweb reference of a page is global hash key computed
on the basis of the contents of the specific page. This ensures that
each page has a unique key, that is, reference. The reference of this
page in the special \emph{kana}\footnote{For details on kana we refer to
\url{http://yoa.dk/logiweb/doc/misc/kana.html}.} format is:
\display{\tt\lgwPeanoCommutativityKana}
\texttt{Kana} is a format developed for Logiweb making it possible to
speak or pronounce a reference. This is done because Logiweb has been
developed with the possibility of using a microphone as input tool in
mind.
Also, one can refer to this page using the well-known http url:
\begin{quote}
{\scriptsize http://www.diku.dk/~grue/logiweb/20050502/home/ \\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
mrmr/peano-commutativity/latest/vector/page.lgw}
\end{quote}
Two last ways to refer to a page is using the reference expressed in
so-called \emph{mixed endian hexadecimal} or using a decimal reference.
Cf.~\cite{grue:check} and the \texttt{Reference} section in the source
or \texttt{pyk} code in a Logiweb page. The reference section---known as
the \texttt{BIBLIOGRAPHY}---of a Logiweb page will be introduced shortly.
\subsection{The Base Page}
Now, in the previous section we mentioned \emph{the base} of the mesh of
Logiweb pages. This is a certain part of Logiweb, which implements the
basic and necessary functionalities of the mathematical part of the
Logiweb system. That is, the \emph{base page}---as it is
denoted---defines the proof checker and most of what makes the
mathematics of Logiweb possible. Actually, there is possibly more than
one base page, but the one Klaus Grue has written will probably be
\emph{the} base page to begin with. But one is free to write a base
page making up a different (or a similar) system. A base page is a page
without references to other pages and thus form the base of a
mathematical system within Logiweb. For more on this we refer to the
\href{\lgwBaseUrl}{base} page, Section 1.4 in particular.
\\
\noindent
We now know the necessary basics of the Logiweb system. Next, we take a
closer look at the structure of a Logiweb page.
%%%%%%%%%% A Logiweb Page %%%%%%%%%%%
\section{A Logiweb Page}
In this section we shortly describe the most important details of a
Logiweb page. That is, we introduce the Logiweb page, the language used
in Logiweb, and the predefined structure all pages must be written
according to. This introduction is adequate for getting started with
Logiweb, but is in no manner satisfactory to the serious user of
the Logiweb system.
\subsection{``Main Menu''}
In the Logiweb system each page has a so-called \emph{main menu}, e.g.,
the main menu of this page is at:
\begin{quote}
{\scriptsize
\url{http://www.diku.dk/~grue/logiweb/20050502/home/mrmr/peano-commutativity/latest/}}
\end{quote}
From the main menu one can browse and find numerous kinds of information
about the page. The most important of which to begin with is the page in
\texttt{pdf} format and (for Logiweb newbie) the source code.
A Logiweb page is written in mixture of {\LaTeX} and the language
\texttt{pyk} developed by Klaus Grue. \texttt{pyk} is then the language
in which the mathematics to be checked by a computer of a Logiweb page
is written. The best way to get a feeling for this mixture is to read
the source code of a Logiweb page. This is found under \texttt{Source}
$\rightarrow$ \texttt{Actual Source} from the Logiweb main menu of a Logiweb
page, e.g., the \href{\lgwCheckUrl}{check} page.
One can also read the \texttt{pyk} text of a page, which is found under
\texttt{Body} $\rightarrow$ \texttt{Pyk} also at the Logiweb main menu. It is
also under \texttt{Body} that one finds the {\TeX} and pdf files of the
page.\footnote{The {\TeX} files are not available through a browser due
to safety precautions.}
\subsection{The Pyk Language}
As mentioned in the previous section the \texttt{pyk} language has been
developed for easy pronounciation or in generel for ``spoken
mathematics'', cf. the \href{\lgwBaseUrl}{base} page, Section 1.1. Thus,
a mathematical expression as we are well-acquaintated with such as:
\[ ( x + y ) ^ 2 = x ^ 2 + 2 x y + y ^ 2 \]
\noindent may be the equivalent of the following \texttt{pyk} expression:
\begin{quote}
parenthesis var x plus var y end parenthesis square equals var x square
plus two times var x times var y plus var y square\footnote{This example
has been taken from~\cite{grue:base}.}
\end{quote}
Thus, in time one can ``tell'' one's mathematics to a computer and it
will generate a file written in \texttt{pyk}, which will then be the
source for precisely one Logiweb page. This is also the reason why
\texttt{pyk} is case sensitive, that is, the \texttt{pyk} code cannot be
in capital letters.
We thus see that \texttt{pyk} is much like any other programming
language. However, in \texttt{pyk} one writes everything out in words
instead of using symbols, e.g., ``parenthesis'' and ``end parenthesis''
instead of ``('' and ``)''. In pdf format the textual representations
will be replaced by their symbolic representations defined by the author
of a Logiweb page. We shall return to this \emph{aspect} of Logiweb in
Section \ref{sec:LogiwebTheory}.
\subsection{The Structure of a Logiweb Page}
A Logiweb page has to be written according to certain standards. Thus, a
specific structural sketch for a Logiweb page has to used, which defines
the specific and necessary parts of a Logiweb source file, that is, a
\texttt{pyk} file. A \texttt{pyk} file has exactly one of each of these
parts or sections, which will be described below. We note that the
section names must be in capital letters. Like the {\TeX} code and
normal text written this is not part of \texttt{pyk} and does not need
to be in small letters.
\begin{description}
\item[\texttt{PAGE}] A Logiweb page has a name which is given in the
\texttt{PAGE} section of the \texttt{pyk} file. For instance, in the
source code for this page one will find the PAGE section at the very top
where it is seen that this page is named ``peano commutativity''.
\item[\texttt{BIBLIOGRAPHY}] The references of a Logiweb page are given
in the \texttt{BIBLIOGRAPHY} section of the \texttt{pyk} file. A page
can refer to every possible Logiweb page, also if one of these pages
refer to once referenced pages. The Logiweb server will make sure no
cyclic references occur.
\item[\texttt{ASSOCIATIVITY}] In the \texttt{ASSOCIATIVITY} section of
the \texttt{pyk} file the constructs of a logiweb page and their
associativity---either POST- or PRE- are the options--- are declared.
The order of the constructs furthermore define their priority.
Constructs declared with comma separation after the same associativity
statement have same priority. (In a sense the \emph{constructs} of a
Logiweb page make up the available \texttt{pyk} code in a page and pages
refering to the page declaring and defining the constructs.) Thus, we
get that:
\begin{quote}
\texttt{PREASSOCIATIVE * plus *, * minus *}
\end{quote}
gives that, e.g., "
begin bracket var x plus var y end bracket
end " have the same
priority as "
begin bracket var x minus var y end bracket
end ", where as:
\begin{quote}
\texttt{PREASSOCIATIVE * times *} \\
\vdots \\
\texttt{PREASSOCIATIVE * plus *}
\end{quote}
gives that, e.g., "
begin bracket var x times var y end bracket
end " have higher
priority than "
begin bracket var x plus var y end bracket
end ". These examples are
from the \href{\lgwBaseUrl}{base} page. In order to use these constructs
in another page they should be entered in the associativity section of
the page in question with \texttt{base} written after the associativity
assignment. The usage of the names of constructs from a page in the
associativity section of another page is to place the priority of new
constructs in a proper hierarcical order. Thus, in the associativity
section this page we put names of, e.g., the lemmas to be proved
together with the \texttt{bracket} declaration, which gives those
constructs the same priority:
\begin{quote}
\texttt{PREASSOCIATIVE base: bracket * end bracket, \\
mendelson lemma one eight
eight}
\end{quote}
\item[\texttt{BODY}] In the \texttt{BODY} section we enter the actual
text and math of the page. Hence, this is the section most readers get
acquianted with, and they probably do so in pdf format. It is also in
this section that the actual \texttt{pyk} coding is done.
\end{description}
We thus get the following preamble for a Logiweb page:
\begin{figure}[ht!]
\centering
{\tiny
\begin{tabular}{lll}
PAGE name \\
\vdots \\
\\
BIBLIOGRAPHY \\
base: nani \\
\hspace{1cm} \ldots \\
\vdots \\
\\
PREASSOCIATIVITY \\
\vdots & & \\
\\
BODY \\
\vdots \\
\end{tabular}
%\caption{.}\label{tab:}
}
\end{figure}
The above only gives a bland taste of the richness of a very complex
system that Logiweb is. But as stated earlier we believe it should be
enough to get the reader started.
Now we proceed to the actual mathematics of this page, namely peano
arithmetic. But before getting into details with this we place the
assignment in a larger frame of reference.
%%%%%%%%%% Propositional Calculus %%%%%%%%%%
\section{Axiomatic Theories}
In this section we give a basic introduction to the concepts with which
we will be working in the rest of the report. In may well be skipped by
the (experienced) logician.
For simple systems of logic we can decide the truth value of a statement
by mere use of truth tables. Rather quickly this is not enough when
expressing more complex systems of logic. Though it took our ancestors a
couple of millenniums to give us the formalistic tools to express only
the simplest of logical statements the basic elements of the so-called
formal axiomatic theories are quite simple. Cf.~\cite{mendelson}, pp.
34ff.
The branch of logic known as \emph{propositional calculus} is simple to
understand and serves well when introducing the concept of axiomatic
theories. The abstract concept of propositions, i.e. the abstract
denotation of sentences like ``Jones is communist'' and ``Jones is an
atheis'', and a few logical connectives, e.g. $\neg$ and $\Rightarrow$,
can be put together with one of more rules of inference in a proper way
and thus form a calculus. The combined logical statements can express
many types of statements, the truth of which we can determine by use of
truth tables. We extend these concepts in the following manner. We
define a formal theory $\mathcal{L}$ when the following conditions are
satisfied:\footnote{We only state the most necessary concepts here,
cf.~\cite{mendelson}, pp. 34f. for an elaborate explanation.}
\begin{enumerate}
\item In $\mathcal{L}$ a countable set of symbols are given, a
finite sequence of which is called an \emph{expression} of
$\mathcal{L}$.
\item A subset of the set of expressions of $\mathcal{L}$ are called the
set of \emph{well-formed formulas} of $\mathcal{L}$ or \emph{wfs} for
short.
\item A set of the wfs are called the \emph{axioms} of $\mathcal{L}$. If
it can effectively be decided whether a wf is an axiom then
$\mathcal{L}$ is said to be an \emph{axiomatic} theory.\footnote{We thus
have that theories defined in Logiweb must be axiomatic theories.}
\item A finite set of relations, $R_1, \ldots, R_n$, among the wfs make
up the \emph{rules of inference}. We say that the wf $\mathcal{B}$ is a
\emph{direct consequence} of a given set of wfs and that it is so by
virtue of $R_i$, if for each $R_i$, there is a unique positive integer
$j$ such that, for every se of $j$ wfs and each $\mathcal{B}$, one can
effectively decide whether the given $j$ wfs are in the relation $R_i$
to $B$.
\end{enumerate}
A \emph{proof} in $\mathcal{L}$ is a sequence $\mathcal{B}_1, \ldots,
\mathcal{B}_k$ of wfs such that, for each $i$, either $B_i$ is an axiom of
$\mathcal{L}$ or $\mathcal{B}_i$ is a direct consequence of some of the
preceding wfs in the sequence by virtue of one of the rules of inference
of $\mathcal{L}$.
A \emph{theorem} of $\mathcal{L}$ is a wf $\mathcal{B}$ such that
$\mathcal{B}$ is the last wf of some proof in $\mathcal{L}$. Such a
proof is called a \emph{proof of $\mathcal{B}$ in $\mathcal{L}$}. If it can
be machine checked whether a given theorem is indeed a theorem of a
given theory then we say that the theory is \emph{decidable}, otherwise
it is said to be \emph{undecidable}.
We say that $\mathcal{C}$ is a \emph{consequence} of a set of wfs,
$\Gamma$, if and only if there is a sequence of wfs,
$\mathcal{B}_1,\ldots, \mathcal{B}_k$, such that $\mathcal{C}$ is
$\mathcal{B}_k$,
and, for each $i$, either $\mathcal{B}_i$ is an axiom or $\mathcal{B}_i$
is a direct consequence by some rule of inference of some of the
preceding wfs in the sequence, which is then called a \emph{proof} or
(\emph{deduction}) of $\mathcal{C}$ from $\Gamma$. The members of
$\Gamma$ are called the \emph{hypotheses} or \emph{premisses} of the
proof.
We now have the prerequicites in order to define an actual theory.
\subsection{The Axiomatic Theory $L$}\label{sec:TheoryL}
The concept of a formal axiomatic theory $L$ for the propositional
calculus can now be introduced:
\begin{enumerate}
\item The symbols of $L$ are $\neg$, $\Rightarrow$, (, ), and the
letters $A_i$, for $i \in N$.
\item Well-formed formulas:
\begin{enumerate}
\item All statement letters are wfs.
\item if $\mathcal{B}$ and $\mathcal{C}$ are wfs, then so are
$(\neg\mathcal{B})$ and $(\mathcal{B} \Rightarrow \mathcal{C})$.
\end{enumerate}
\item If $\mathcal{B}$, $\mathcal{C}$, and $\mathcal{D}$ are wfs of $L$,
then the following are axioms of $L$:
\begin{enumerate}
\item[(A1)] $(\mathcal{B} \Rightarrow ( \mathcal{C} \Rightarrow
\mathcal{B}))$
\item[(A2)] $((\mathcal{B} \Rightarrow (\mathcal{C} \Rightarrow
\mathcal{D})) \Rightarrow ((\mathcal{B} \Rightarrow \mathcal{C})
\Rightarrow (\mathcal{B} \Rightarrow \mathcal{D})))$
\item[(A3)] $(((\neg\mathcal{C}) \Rightarrow (\neg\mathcal{B}))
\Rightarrow ((( \neg\mathcal{C}) \Rightarrow \mathcal{B}) \Rightarrow
\mathcal{C}))$
\end{enumerate}
\item One rule of inference of $L$, namely \emph{modus ponens}, which
says that $\mathcal{C}$ is a direct consequence of $\mathcal{B}$ and
$\mathcal{B} \Rightarrow \mathcal{C}$. This rule is abbriviated by $MP$.
\end{enumerate}
This theory can, of course, be elaborated upon, but we shall not pursue
the details of this any further. Nor shall we make more distinctions in
the logical concepts with which this assignment is concerned. Instead we
shall place it in the Logiweb frame of reference.
\subsection{An Axiomatic Logiweb Theory}\label{sec:LogiwebTheory}
It is in the conceptual framework introduced in the previous subsection
that we shall work in when proving the law commutativity of addition
within peano arithmetic. Since this proof must be carried out within the
system of Logiweb we here give a Logiweb example and prove a very basic
lemma from~\cite{mendelson}, p. 36, namely
"
begin math define pyk of mendelson lemma one eight as text "mendelson lemma one eight" end text end define end math
then math define tex of mendelson lemma one eight as text "M\ Lemma\ 1.8" end text end define end math
end ". (We shall adopt the convention of writing ``M'' in
front of a lemma, proposition etc. to denote ``Mendelson''.)
Now, the appearence of ``M Lemma 1.8'' above is somewhat special. First,
the name of the lemma (actually, it is not a lemma until defined to be
so---now it is merely a \emph{construct} in this page) appeared in brackets and
with a footnote. This is specific to Logiweb and from it we are
introduced to some of the \emph{aspects} of Logiweb. Cf. the
\href{\lgwBaseUrl}{base} page, Section 2.2.1.
If reading the \texttt{pyk} file one can find the declaration of "
begin bracket mendelson lemma one eight end bracket
end " as being part of this Logiweb page
almost at the very top, namely in the associativity section. And at this
point in the text we introduce the construct to Logiweb, that is, from
now on one can refer to the construct by writing some specific
\texttt{pyk} code. One refers to this construct by writing what appears
in the footnote of the construct after the equality sign with ``pyk''
written above it; this is an example of the \emph{pyk aspect} of
Logiweb. As is clear now, it simply defines the \texttt{pyk} code.
Another aspect is the \emph{{\TeX} aspect} of Logiweb, which is simply
how a construct in Logiweb appears in writing, that is, in those formats
one can build from a normal {\TeX} document, e.g., a pdf document. The
{\TeX} aspect is defined by the user or author who within the limits of
{\TeX} single-handedly decides how the construct should appear.
Having made the construct visible or available to Logiweb, we want to
place it some specific framework within which we work, that is, in a
theory or system. We could denote this system $L$ in accordance with
what has been said above and build our theory from the bottom. Instead
we shall make use of the work of Klaus Grue. Thus, we introduce "
begin bracket mendelson lemma one eight end bracket
end " in "
begin bracket system prime s end bracket
end ", which is defined on the
\href{\lgwPeanoUrl}{peano} page. We do this as follows: \\
\noindent
"
begin math define statement of mendelson lemma one 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 "
\\
For now we merely mention in passing that the special symbol
$\dot{\Rightarrow}$ with the little dot appearing above the imply symbol
tells us that this implication is specific to the peano arithmetic
defined in "
begin bracket system prime s end bracket
end ". This system will be the
one within which we will be working, and we shall examine it more in the
next section.
We have now defined the construct "
begin bracket mendelson lemma one eight end bracket
end " to be a lemma in the system "
begin bracket system prime s end bracket
end ". Then we must prove it in order to use it later should we
have the need for that. This is done using axiomatic constructs from the
peano page. For now, we shall use these without further introduction,
which we defer until the next section: \\
\noindent
"
begin math define proof of mendelson lemma one 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 "
\\
We have now seen an example of a proof of a lemma belonging to a certain
theory in Logiweb. In the next section we will take a closer look at the
axiomatic theory "
begin bracket system prime s end bracket
end " in which we will be
working.
%%%%%%%%%% Peano Arithmetic %%%%%%%%%%
\section{Peano Arithmetic}
As stated above the assignment of this report is to prove the law of
commutativity of addition within the natural numbers. More precisely, we
shall prove it within the system of \emph{peano arithmetic} as it is
stated in Chapter 3 of~\cite{mendelson}. Peano arithmetic is based upon
five postulates:
\begin{enumerate}
\item[(P1)] $0$ is a natural number.
\item[(P2)] If $x$ is a natural number, then there is another natural
number denoted by $x^{\prime}$; this is denoted the \emph{successor} of $x$.)
\item[(P3)] $0 \neq x^{\prime}$ for every natural number $x$.
\item[(P4)] If $x^{\prime} = y^{\prime}$, then $x = y$.
\item[(P5)] If $Q$ is a property that may or may not hold for any given
natural number, and if:
\begin{enumerate}
\item[(I)] $0$ has the property $Q$, and
\item[(II)] whenever a natural number $x$ has the property $Q$, then
$x^{\prime}$ has the property $Q$,
\end{enumerate}
then all natural numbers have the property $Q$. This is the mathematical
principle of induction.
\end{enumerate}
Klaus Grue has implemented peano arithmetic making most of the needed
constructs to solve the assignment available to us.
Cf.~\href{\lgwPeanoUrl}{peano}, Section 1.5. The result of his work is
among other things the theory within which we will be working, namely
the aforementioned theory "
begin bracket system prime s end bracket
end ". This
theory is much like the axiomatic theory we met in
Section~\ref{sec:TheoryL}, p.~\pageref{sec:LogiwebTheory}. Only, this
theory has more axioms, a number of theorems we can use, and one more
rule of inference. We repeat the full system in the following for easy
reference.
\subsection{Peano Arithmetic in Logiweb}
Peano arithmetic in Logiweb consists of the axioms, theorems, and rules
of inference that is restated in the following subsections; they are
introduced and defined in \cite{grue:peano}. The appearence of the
constructs is somewhat special. As mentioned above some symbols are
furnished with a little dot. This special {\TeX} aspect need not confuse
us. It only shows that we are working within peano arithemtic as defined
in the \href{\lgwPeanoUrl}{peano} page. Also, the equality symbol of
peano arithmetic is furnished with a small $p$, which serves the same
purpose as the dot.
\subsubsection{S' Axioms}
In peano arithmetic---or in "
begin math define statement of system prime s as var x end define end math
end " or merely "
begin bracket system prime s end bracket
end " as we shall
refer to it from now on---the following five axioms or rules are
available.
\display{"
begin math define statement of axiom prime a one as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end define
then define proof of axiom prime a one as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a two as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define
then define proof of axiom prime a two as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a three as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end define
then define proof of axiom prime a three as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a four as system prime s infer all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse peano all metavar var x end metavar indeed metavar var b end metavar peano imply metavar var a end metavar end define
then define proof of axiom prime a four as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a five as system prime s infer all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed newline 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 "}
These definitions are copied from the \href{\lgwPeanoUrl}{peano} page,
Section 1.5.
%%%%% text... %%%%%
\subsubsection{S' Rules of Inference}
Besides the five axioms "
begin math define statement of system prime s as var x end define end math
end " has two rules of inference. The first is the well-known modus
ponens, which all computer scientists are well-acquainted with. The
second says that a well-formed formula has as a consequence that it is
sound or valid for all variables, $x_i$.
%%%%% ...text %%%%%
\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 "}
These definitions are copied from the \href{\lgwPeanoUrl}{peano} page,
Section 1.5.
%%%%% text... %%%%%
\subsubsection{S' Theorems}
Finally, within "
begin math define statement of system prime s as var x end define end math
end " we
are allowed to use the following theorems. We shall not prove these:
%%%%% ...text %%%%%
\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 "}
These definitions are copied from the \href{\lgwPeanoUrl}{peano} page,
Section 1.5.
\\
We now have the necessary means to solve our assignment, which we will
do in the following sections.
\section{Proof of Commutativity of Addition}
As mentioned in the introduction we shall prove the law of commutativity
of addition in as simple a way as possible. We thus follow Mendelson in
his proof, cf.~\cite{mendelson}, pp. 156ff. Hence, we will prove this
law by proving Proposition 3.2(a)-(h), except Proposition 3.2(e). As we
close in on our goal we will be needing two tautologies and in our last
proof a lemma, which we will state and prove as we go along. We do this
in the following subsections. We explain what goes on as we go along. In
each proof we first introduce the proposition in Logiweb, then we state
the proposition, and finally we prove it.
%\subsection{Mendelson Proposition 3.2(a)}
\subsection{"
begin math mendelson proposition three two a end math
end "}
%%%%%%%%%% 3.2(a) %%%%%%%%%%% OK
The first proposition states that a wf is equal to itself. Since peano
arithmetic is theory with equality this is basic and expected
proposition---and quite logical!
\\
\noindent
"
begin math define pyk of mendelson proposition three two a as text "mendelson proposition three two a" end text end define end math
then math define tex of mendelson proposition three two a as text "M\ Proposition\ 3.2(a)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition three two a as system prime s infer all metavar var t end metavar indeed metavar var t end metavar peano is metavar var t end metavar end define end math
end "
\\
%%%%% Proof of 3.2(a) %%%%%
\noindent
"
begin math define proof of mendelson proposition three two a as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed axiom prime s five conclude metavar var t end metavar peano plus peano zero peano is metavar var t end metavar cut axiom prime s one conclude metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var t end metavar cut rule prime mp modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var t end metavar modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar conclude metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var t end metavar cut rule prime mp modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var t end metavar modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar conclude metavar var t end metavar peano is metavar var t end metavar end quote state proof state cache var c end expand end define end math
end "
\\
Proposition 3.2(a) is used in the proof of Proposition 3.2(b). But
before we can proceed to this we must prove a tautology also.
%%%%%%%%%% Tautology A [3.2(b)] %%%%%%%%%%%
%\subsection{Mendelson Tautology A}
\subsection{"
begin math mendelson tautology a end math
end "}
In~\cite{mendelson}, p. 157 in the proof of Proposition 3.2(b) we see
that a tautology is used. We shall state and prove this tautology for
use in our next and later proofs.
\\
\noindent
"
begin math define pyk of mendelson tautology a as text "mendelson tautology a" end text end define end math
then math define tex of mendelson tautology a as text "M\ Tautology\ A" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson tautology a 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 "
\\
%%%%% Proof of Tautology A %%%%%
\noindent
"
begin math define proof of mendelson tautology a 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 "
\\
We note that "
begin bracket mendelson proposition three two b end bracket
end "
could also be proved by the help of Corollary 1.10(b),
cf.~\cite{mendelson}, p. 38. Mendelson proves this by the use of
Proposition 1.9 also know as the Deduction Theorem,
cf.~\cite{mendelson}, p. 37. We avoid the use of this, though, it would
have been prettier to follow Mendelson completely.
%\subsection{Mendelson Proposition 3.2(b)}
\subsection{"
begin math mendelson proposition three two b end math
end "}
%%%%%%%%%% 3.2(b) %%%%%%%%%%% OK
We now proceed to proving "
begin bracket mendelson proposition three two b end bracket
end " where we will make use of "
begin bracket mendelson tautology a end bracket
end ". \\
\noindent
"
begin math define pyk of mendelson proposition three two b as text "mendelson proposition three two b" end text end define end math
then math define tex of mendelson proposition three two b as text "M\ Proposition\ 3.2(b)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition 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 "
\\
%%%%% Proof of Proposition 3.2(b) %%%%%
\noindent
"
begin math define proof of mendelson proposition 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 mendelson tautology a modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar conclude metavar var t end metavar peano is metavar var t end metavar peano imply 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 mendelson proposition three two a conclude metavar var t end metavar peano is metavar var t end metavar cut rule prime mp modus ponens metavar var t end metavar peano is metavar var t end metavar peano imply 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 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 "
\\
Thus having proved "
begin bracket mendelson proposition three two b end bracket
end " we proceed to "
begin bracket mendelson proposition three two c end bracket
end " in the proof of which the former is used. But before we do
this we need yet another tautology.
%%%%%%%%%% Tautology B [3.2(c)] %%%%%%%%%%%
%\subsection{Mendelson Tautology B}
\subsection{"
begin math mendelson tautology b end math
end "}
In~\cite{mendelson}, p. 157 in the proof of Proposition 3.2(c) we see
that a tautology is used. We shall state and prove this tautology for
use in our next proof.
\\
\noindent
"
begin math define pyk of mendelson tautology b as text "mendelson tautology b" end text end define end math
then math define tex of mendelson tautology b as text "M\ Tautology\ B" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson tautology b as system prime s infer all metavar var d end metavar indeed all metavar var e end metavar indeed all metavar var f end metavar indeed metavar var d end metavar peano imply metavar var e end metavar infer metavar var e end metavar peano imply metavar var f end metavar infer metavar var d end metavar peano imply metavar var f end metavar end define end math
end "
\\
%%%%% Proof of Tautology B %%%%%
\noindent
"
begin math define proof of mendelson tautology b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var d end metavar indeed all metavar var e end metavar indeed all metavar var f end metavar indeed metavar var d end metavar peano imply metavar var e end metavar infer metavar var e end metavar peano imply metavar var f end metavar infer axiom prime a one conclude metavar var e end metavar peano imply metavar var f end metavar peano imply metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar cut rule prime mp modus ponens metavar var e end metavar peano imply metavar var f end metavar peano imply metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar modus ponens metavar var e end metavar peano imply metavar var f end metavar conclude metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar cut axiom prime a two conclude metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar peano imply metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var d end metavar peano imply metavar var f end metavar cut rule prime mp modus ponens metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar peano imply metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var d end metavar peano imply metavar var f end metavar modus ponens metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar conclude metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var d end metavar peano imply metavar var f end metavar cut rule prime mp modus ponens metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var d end metavar peano imply metavar var f end metavar modus ponens metavar var d end metavar peano imply metavar var e end metavar conclude metavar var d end metavar peano imply metavar var f end metavar end quote state proof state cache var c end expand end define end math
end "
\\
We can now prove "
begin bracket mendelson proposition three two c end bracket
end ".
%\subsection{Mendelson Proposition 3.2(c)}
\subsection{"
begin math mendelson proposition three two c end math
end "}
%%%%%%%%%% 3.2(c) %%%%%%%%%%% OK
As noted above we will make use of "
begin bracket mendelson tautology b end bracket
end " in our proof of "
begin bracket mendelson proposition three two c end bracket
end ", which concerns transitivity.
\\
\noindent
"
begin math define pyk of mendelson proposition three two c as text "mendelson proposition three two c" end text end define end math
then math define tex of mendelson proposition three two c as text "M\ Proposition\ 3.2(c)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition 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 "
\\
%%%%% Proof of Proposition 3.2(c) %%%%%
\noindent
"
begin math define proof of mendelson proposition 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 mendelson proposition 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 mendelson tautology b 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 "
\\
Thus having proved "
begin bracket mendelson proposition three two c end bracket
end " we now proceed with "
begin bracket mendelson proposition three two d end bracket
end ".
%\subsection{Mendelson Proposition 3.2(d)}
\subsection{"
begin math mendelson proposition three two d end math
end "}
In order to prove "
begin bracket mendelson proposition three two d end bracket
end " following the proof in~\cite{mendelson}, p. 157, we will be
using two tautologies. A closer examination of the proofs reveals that
the two tautologies are an instance of "
begin bracket mendelson tautology a end bracket
end " and one of "
begin bracket mendelson tautology a end bracket
end ". Furthermore, we will be needing "
begin bracket mendelson proposition three two b end bracket
end " in our proof as well. Hence, we can commence
with the proof right away.
\\
%%%%%%%%%% 3.2(d) %%%%%%%%%%% OK
\noindent
"
begin math define pyk of mendelson proposition three two d as text "mendelson proposition three two d" end text end define end math
then math define tex of mendelson proposition three two d as text "M\ Proposition\ 3.2(d)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition three two d as system prime s infer all metavar var r end metavar indeed all metavar var t 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 "
\\
\noindent
"
begin math define proof of mendelson proposition three two d as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var r end metavar indeed all metavar var t end metavar indeed all metavar var s end metavar indeed mendelson proposition 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 mendelson tautology a 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 mendelson proposition 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 mendelson tautology b 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 mendelson tautology a 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 "
\\
Thus having proved "
begin bracket mendelson proposition three two d end bracket
end " we now proceed with "
begin bracket mendelson proposition three two f end bracket
end " in the proof of which we use the result just
obtained.
%\subsection{Mendelson Proposition 3.2(f)}
\subsection{"
begin math mendelson proposition three two f end math
end "}
The proof of "
begin bracket mendelson proposition three two f end bracket
end "
is split up into two parts as is seen from \cite{mendelson}, pp. 157f.
%\subsubsection{Mendelson Proposition 3.2(f) (i)}
\subsubsection{"
begin math mendelson proposition three two f i end math
end "}
After having introduced the proposition and placed it in the theory in
which we are working, we first show the identity of "
begin bracket peano zero end bracket
end ". This is the base case of a well-known proof by
induction. After have proved the base case, we shall thus proceed and
prove the induction step by the use of our two tautologies. Finally, we
prove "
begin bracket mendelson proposition three two f end bracket
end " by the
use of our two intermediary results.
\\
%%%%%%%%%% 3.2(f) (i) %%%%%%%%%%%
\noindent
"
begin math define pyk of mendelson proposition three two f i as text "mendelson proposition three two f i" end text end define end math
then math define tex of mendelson proposition three two f i as text "M\ Proposition\ 3.2(f)\ (i)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition three two f i as system prime s infer peano zero peano is peano zero peano plus peano zero end define end math
end "
\\
\noindent
"
begin math define proof of mendelson proposition three two f i 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 mendelson proposition 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 "
\\
We have now showed the base case in an induction. The next step is to
continue the induction.
%\subsubsection{Mendelson Proposition 3.2(f) (ii)}
\subsubsection{"
begin math mendelson proposition three two f ii end math
end "}
In Mendelson's proof of "
begin bracket mendelson proposition three two f ii end bracket
end " we note that the Deduction Theorem is used,
cf.~\cite{mendelson}, p. 158. We shall not use this theorem in our proof
but instead use the previously proved tautologies.
\\
%%%%%%%%%% 3.2(f) (ii) %%%%%%%%%%%
\noindent
"
begin math define pyk of mendelson proposition three two f ii as text "mendelson proposition three two f ii" end text end define end math
then math define tex of mendelson proposition three two f ii as text "M\ Proposition\ 3.2(f)\ (ii)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition three two f ii as system prime s infer peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ end define end math
end "
\\
\noindent
"
begin math define proof of mendelson proposition three two f ii as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s six conclude peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut axiom prime s two conclude var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut mendelson proposition three two d conclude var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut mendelson tautology b modus ponens var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ modus ponens var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ conclude var x peano var peano is peano zero peano plus var x peano var peano imply peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut mendelson tautology a modus ponens var x peano var peano is peano zero peano plus var x peano var peano imply peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ conclude peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut rule prime mp modus ponens peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ modus ponens peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ conclude var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut rule prime gen modus ponens var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ conclude peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ end quote state proof state cache var c end expand end define end math
end "
\\
We now have the necessary foundation to prove "
begin bracket mendelson proposition three two f end bracket
end ".
%\subsubsection{Mendelson Proposition 3.2(f)}
\subsubsection{"
begin math mendelson proposition three two f end math
end "}
As is seen from \cite{mendelson}, p. 158, induction is used in the proof
of "
begin bracket mendelson proposition three two f end bracket
end ". Due to
our ambition of keeping things as simple as possible, we have not
implemented an induction theorem. Hence, the proof will deviate from the
one given by Mendelson.
\\
%%%%%%%%%% 3.2(f) %%%%%%%%%%%
\noindent
"
begin math define pyk of mendelson proposition three two f as text "mendelson proposition three two f" end text end define end math
then math define tex of mendelson proposition three two f as text "M\ Proposition\ 3.2(f)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition three two f as system prime s infer peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var end define end math
end "
\\
%%%%% Proof of 3.2(f) %%%%%
\noindent
"
begin math define proof of mendelson proposition three two f as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s nine conclude peano zero peano is peano zero peano plus peano zero peano imply peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var cut mendelson proposition three two f i conclude peano zero peano is peano zero peano plus peano zero cut rule prime mp modus ponens peano zero peano is peano zero peano plus peano zero peano imply peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var modus ponens peano zero peano is peano zero peano plus peano zero conclude peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var cut mendelson proposition three two f ii conclude peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut rule prime mp modus ponens peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ peano imply peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var modus ponens peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ conclude peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var end quote state proof state cache var c end expand end define end math
end "
\\
We now proceed to proving "
begin bracket mendelson proposition three two g end bracket
end ", which is used in our final proof.
%\subsection{Mendelson Proposition 3.2(g)}
\subsection{"
begin math mendelson proposition three two g end math
end "}
%%%%%%%%%% 3.2(g) %%%%%%%%%%%
The proof of "
begin bracket mendelson proposition three two g end bracket
end "
is very much like our previous proof. Also, in this case do we need a
base case and an induction step.
%\subsubsection{Mendelson Proposition 3.2(g) (i)}
\subsubsection{"
begin math mendelson proposition three two g i end math
end "}
After having introduced the proposition and placed it in the theory in
which we are working, we first show the identity of "
begin bracket peano zero end bracket
end ".
\\
%%%%%%%%%% 3.2(g) (i) %%%%%%%%%%%
\noindent
"
begin math define pyk of mendelson proposition three two g i as text "mendelson proposition three two g i" end text end define end math
then math define tex of mendelson proposition three two g i as text "M\ Proposition\ 3.2(g)\ (i)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition three two g i as system prime s infer peano all var x peano var indeed var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ end define end math
end "
\\
%%%%% Proof of 3.2(g) (i) %%%%%
\noindent
"
begin math define proof of mendelson proposition three two g i as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var x peano var peano succ peano plus peano zero peano is var x peano var peano succ cut axiom prime s five conclude var x peano var peano plus peano zero peano is var x peano var cut axiom prime s two conclude var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano plus peano zero peano succ peano is var x peano var peano succ cut rule prime mp modus ponens var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano plus peano zero peano succ peano is var x peano var peano succ modus ponens var x peano var peano plus peano zero peano is var x peano var conclude var x peano var peano plus peano zero peano succ peano is var x peano var peano succ cut mendelson proposition three two d conclude var x peano var peano succ peano plus peano zero peano is var x peano var peano succ peano imply var x peano var peano plus peano zero peano succ peano is var x peano var peano succ peano imply var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ cut rule prime mp modus ponens var x peano var peano succ peano plus peano zero peano is var x peano var peano succ peano imply var x peano var peano plus peano zero peano succ peano is var x peano var peano succ peano imply var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ modus ponens var x peano var peano succ peano plus peano zero peano is var x peano var peano succ conclude var x peano var peano plus peano zero peano succ peano is var x peano var peano succ peano imply var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ cut rule prime mp modus ponens var x peano var peano plus peano zero peano succ peano is var x peano var peano succ peano imply var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ modus ponens var x peano var peano plus peano zero peano succ peano is var x peano var peano succ conclude var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ cut rule prime gen modus ponens var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ conclude peano all var x peano var indeed var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ end quote state proof state cache var c end expand end define end math
end "
\\
\subsubsection{"
begin math mendelson proposition three two g ii end math
end "}
%Mendelson Proposition 3.2(g) (ii)}
We now proceed with the induction step.
%%%%%%%%%% 3.2(g) (ii) %%%%%%%%%%%
\noindent
"
begin math define pyk of mendelson proposition three two g ii as text "mendelson proposition three two g ii" end text end define end math
then math define tex of mendelson proposition three two g ii as text "M\ Proposition\ 3.2(g)\ (ii)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition three two g ii as system prime s infer peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ end define end math
end "
\\
%%%%% Proof of 3.2(g) (ii) %%%%%
\noindent
"
begin math define proof of mendelson proposition three two g ii as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s six conclude var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano succ peano plus var y peano var peano succ cut axiom prime s two conclude var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut mendelson proposition three two c conclude var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano succ peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut mendelson tautology a modus ponens var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano succ peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ conclude var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano succ peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut mendelson tautology b modus ponens var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ modus ponens var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano succ peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ conclude var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano succ peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut mendelson tautology a modus ponens var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano succ peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ conclude var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano succ peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut rule prime mp modus ponens var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano succ peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ modus ponens var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano succ peano plus var y peano var peano succ conclude var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut axiom prime s six conclude var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ cut axiom prime s two conclude var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut mendelson proposition three two d conclude var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano plus var y peano var peano succ peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut mendelson tautology b modus ponens var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ modus ponens var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano plus var y peano var peano succ peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ conclude var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut mendelson tautology a modus ponens var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ conclude var x peano var peano plus var y peano var peano succ peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut rule prime mp modus ponens var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano succ peano is var x peano var peano plus var y peano var peano succ peano succ modus ponens var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ conclude var x peano var peano plus var y peano var peano succ peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut rule prime mp modus ponens var x peano var peano plus var y peano var peano succ peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ modus ponens var x peano var peano plus var y peano var peano succ peano succ peano is var x peano var peano plus var y peano var peano succ peano succ conclude var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut rule prime gen modus ponens var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ conclude peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ end quote state proof state cache var c end expand end define end math
end "
\\
%%%%%%%%%% 3.2(g) %%%%%%%%%%%
%\subsubsection{Mendelson Proposition 3.2(g)}
\subsubsection{"
begin math mendelson proposition three two g end math
end "}
We now have the necessary means to prove "
begin bracket mendelson proposition three two g end bracket
end ".
\\
\noindent
"
begin math define pyk of mendelson proposition three two g as text "mendelson proposition three two g" end text end define end math
then math define tex of mendelson proposition three two g as text "M\ Proposition\ 3.2(g)" end text end define end math
end "
\noindent
"
begin math define statement of mendelson proposition three two g as system prime s infer peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ end define end math
end "
\\
%%%%% Proof of 3.2(g) %%%%%
\noindent
"
begin math define proof of mendelson proposition three two g as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s nine conclude peano all var x peano var indeed var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ peano imply peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ cut mendelson proposition three two g i conclude peano all var x peano var indeed var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ cut rule prime mp modus ponens peano all var x peano var indeed var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ peano imply peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ modus ponens peano all var x peano var indeed var x peano var peano succ peano plus peano zero peano is var x peano var peano plus peano zero peano succ conclude peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ cut mendelson proposition three two g ii conclude peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ cut rule prime mp modus ponens peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ peano imply peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ modus ponens peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano succ conclude peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ end quote state proof state cache var c end expand end define end math
end "
\\
We have thus proved "
begin bracket mendelson proposition three two g end bracket
end ".
%%%%%%%%%%% 3.2(h) %%%%%%%%%%
%\subsection{Mendelson Proposition 3.2(h)}
\subsection{"
begin math mendelson proposition three two h end math
end "}
We now have the necessary means to show our objective, namely "
begin math mendelson proposition three two h end math
end ". As was the case for "
begin math mendelson proposition three two f end math
end " and "
begin math mendelson proposition three two g end math
end " also this proposition will be shown
by induction, that is, with a base case and an inductive step but
without an induction theorem.
%%%%%%%%%% 3.2(h) (i) %%%%%%%%%%% OK
\subsubsection{"
begin math mendelson proposition three two h i end math
end "}
The proof of "
begin bracket mendelson proposition three two f end bracket
end "
makes use of the @ operator, which is defined on the
\href{\lgwBaseUrl}{base} page, Section 6.3.9. It works as a quantifier
eliminator, that is, a sort of reverse of generalization. First, we
prove the base case. \\
\noindent
"
begin math define pyk of mendelson proposition three two h i as text "mendelson proposition three two h i" end text end define end math
then math define tex of mendelson proposition three two h i as text "M\ Proposition\ 3.2(h)(i)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition three two h i as system prime s infer peano all var x peano var indeed var x peano var peano plus peano zero peano is peano zero peano plus var x peano var end define end math
end "
\\
%%%%% Proof of 3.2(h) (i) %%%%%
\noindent
"
begin math define proof of mendelson proposition three two h i as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var x peano var peano plus peano zero peano is var x peano var cut mendelson proposition three two f conclude peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var cut axiom prime a four at var x peano var conclude peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano is peano zero peano plus var x peano var cut rule prime mp modus ponens peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano is peano zero peano plus var x peano var modus ponens peano all var x peano var indeed var x peano var peano is peano zero peano plus var x peano var conclude var x peano var peano is peano zero peano plus var x peano var cut mendelson proposition three two c conclude var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano plus peano zero peano is peano zero peano plus var x peano var cut rule prime mp modus ponens var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano plus peano zero peano is peano zero peano plus var x peano var modus ponens var x peano var peano plus peano zero peano is var x peano var conclude var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano plus peano zero peano is peano zero peano plus var x peano var cut rule prime mp modus ponens var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano plus peano zero peano is peano zero peano plus var x peano var modus ponens var x peano var peano is peano zero peano plus var x peano var conclude var x peano var peano plus peano zero peano is peano zero peano plus var x peano var cut rule prime gen modus ponens var x peano var peano plus peano zero peano is peano zero peano plus var x peano var conclude peano all var x peano var indeed var x peano var peano plus peano zero peano is peano zero peano plus var x peano var end quote state proof state cache var c end expand end define end math
end "
\\
Thus, we have proved the base case and now proceed to the induction
step. But before we can prove this we need a lemma, which must be proved
first.
%%%%%%%%%% 3.2(h)(g)(ii) %%%%%%%%%%
\subsubsection{"
begin math mendelson proposition three two h g ii end math
end "}
In the proof of "
begin bracket mendelson proposition three two h ii end bracket
end " line 3 we see that "
begin bracket mendelson proposition three two g end bracket
end " is used. Cf.~\cite{mendelson}, p. 158. In comparison to
the proof given here the $x$ and $y$ variables are swaped. We thus need
a lemma allowing this version of the proposition. This is because we
have used constants in stating and proving the proposition.
The lemma we need is as follows:
\\
\noindent
"
begin math define pyk of mendelson proposition three two h g ii as text "mendelson proposition three two h g ii" end text end define end math
then math define tex of mendelson proposition three two h g ii as text "M\ Proposition\ 3.2(h)_{(g)(ii)}" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition three two h g ii as system prime s infer peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ infer var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ end define end math
end "
\\
%%%%% Proof of 3.2(h)(g)(ii) %%%%%
"
begin math define proof of mendelson proposition three two h g ii as lambda var c dot lambda var x dot proof expand quote system prime s infer peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ infer axiom prime a four at var z peano var conclude peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var z peano var peano is var x peano var peano plus var z peano var peano succ cut rule prime mp modus ponens peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano succ peano plus var z peano var peano is var x peano var peano plus var z peano var peano succ modus ponens peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ conclude var x peano var peano succ peano plus var z peano var peano is var x peano var peano plus var z peano var peano succ cut rule prime gen modus ponens var x peano var peano succ peano plus var z peano var peano is var x peano var peano plus var z peano var peano succ conclude peano all var x peano var indeed var x peano var peano succ peano plus var z peano var peano is var x peano var peano plus var z peano var peano succ cut axiom prime a four at var y peano var conclude peano all var x peano var indeed var x peano var peano succ peano plus var z peano var peano is var x peano var peano plus var z peano var peano succ peano imply var y peano var peano succ peano plus var z peano var peano is var y peano var peano plus var z peano var peano succ cut rule prime mp modus ponens peano all var x peano var indeed var x peano var peano succ peano plus var z peano var peano is var x peano var peano plus var z peano var peano succ peano imply var y peano var peano succ peano plus var z peano var peano is var y peano var peano plus var z peano var peano succ modus ponens peano all var x peano var indeed var x peano var peano succ peano plus var z peano var peano is var x peano var peano plus var z peano var peano succ conclude var y peano var peano succ peano plus var z peano var peano is var y peano var peano plus var z peano var peano succ cut rule prime gen modus ponens var y peano var peano succ peano plus var z peano var peano is var y peano var peano plus var z peano var peano succ conclude peano all var z peano var indeed var y peano var peano succ peano plus var z peano var peano is var y peano var peano plus var z peano var peano succ cut axiom prime a four at var x peano var conclude peano all var z peano var indeed var y peano var peano succ peano plus var z peano var peano is var y peano var peano plus var z peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut rule prime mp modus ponens peano all var z peano var indeed var y peano var peano succ peano plus var z peano var peano is var y peano var peano plus var z peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ modus ponens peano all var z peano var indeed var y peano var peano succ peano plus var z peano var peano is var y peano var peano plus var z peano var peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ end quote state proof state cache var c end expand end define end math
end "
\\
We now have the necessary means to prove the induction step of "
begin math mendelson proposition three two h ii end math
end "
%%%%%%%%%% 3.2(h) (ii) %%%%%%%%%%% OK
\subsubsection{"
begin math mendelson proposition three two h ii end math
end "}
We then prove the induction step.
\\
%\newpage
\noindent
"
begin math define pyk of mendelson proposition three two h ii as text "mendelson proposition three two h ii" end text end define end math
then math define tex of mendelson proposition three two h ii as text "M\ Proposition\ 3.2(h)(ii)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition three two h ii as system prime s infer peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var end define end math
end "
\\
%%%%% Proof of 3.2(h) (ii) %%%%%
\noindent
"
begin math define proof of mendelson proposition three two h ii as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s six conclude var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ cut mendelson proposition three two g conclude peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ cut mendelson proposition three two h g ii modus ponens peano all var y peano var indeed var x peano var peano succ peano plus var y peano var peano is var x peano var peano plus var y peano var peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut axiom prime s two conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut mendelson proposition three two c conclude var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut mendelson tautology a modus ponens var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ conclude var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut mendelson tautology b modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ modus ponens var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut mendelson tautology a modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ conclude var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut rule prime mp modus ponens var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ peano imply var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ modus ponens var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut mendelson proposition three two d conclude var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var cut mendelson tautology b modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ modus ponens var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var cut mendelson tautology a modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var cut rule prime mp modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var cut rule prime gen modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var conclude peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var end quote state proof state cache var c end expand end define end math
end "
\\
We have thus proved the inductive step and can proceed to our final
objective.
%%%%%%%%%% 3.2(h) %%%%%%%%%%% OK
\subsubsection{"
begin math mendelson proposition three two h end math
end "}
And finally, we can now prove the objective of this report, namely the
commutative law of addition.
\\
\noindent
"
begin math define pyk of mendelson proposition three two h as text "mendelson proposition three two h" end text end define end math
then math define tex of mendelson proposition three two h as text "M\ Proposition\ 3.2(h)" end text end define end math
end "
\\
\noindent
"
begin math define statement of mendelson proposition three two h as system prime s infer peano all var x peano var indeed peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var end define end math
end "
\\
%%%%% Proof of 3.2(h) %%%%%
"
begin math define proof of mendelson proposition three two h as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s nine conclude peano all var x peano var indeed var x peano var peano plus peano zero peano is peano zero peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var cut mendelson proposition three two h i conclude peano all var x peano var indeed var x peano var peano plus peano zero peano is peano zero peano plus var x peano var cut rule prime mp modus ponens peano all var x peano var indeed var x peano var peano plus peano zero peano is peano zero peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var modus ponens peano all var x peano var indeed var x peano var peano plus peano zero peano is peano zero peano plus var x peano var conclude peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var cut mendelson proposition three two h ii conclude peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var cut rule prime mp modus ponens peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var modus ponens peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var conclude peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var cut rule prime gen modus ponens peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var conclude peano all var x peano var indeed peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var end quote state proof state cache var c end expand end define end math
end "
\\
We have thus proved "
begin math mendelson proposition three two h end math
end ", that is, the commutative law of addition.
%%%%%%%%%% Conclusion %%%%%%%%%%
\section{Conclusion}
In this report we have stated and proved a number of propositions from
\cite{mendelson}, p. 156. More precisely we have proved Proposition
3.2(a)-(h), except Proposition 3.2(e). The proofs have been carried out
we the ambition of keeping things as simple as possible. We have
succeded in doing so, proving all propositions by the help of the
theorems given in "
begin math define statement of system prime s as var x end define end math
end "
defined on the \href{\lgwPeanoUrl}{peano} page, two tautologies, and one
lemma needed in the proof of our final theorem. The final theorem stated
our original assignment, namely the commutativity of addition. We can
thus conclude that we have solved the assignment properly.
Furthermore, for the inexperienced user and logician we have given a
short and adequate introduction to the Logiweb system, axiomatic
theories, and peano arithmetic. The introduction should make the report
self-contained, though, we have given references to relevant literature
where needed.
\newpage
%%%%%%%%%% Appendix %%%%%%%%%%%%%%
\appendix
%%%%%%%%%% Chores %%%%%%%%%%%%%%
%\section{Chores}
%%%%%%%%%%%%%% Name of Page %%%%%%%%%%%%%%
%\subsection{The Name of the Page}
\section{The Name of the Page}
This defines the name of the page:
\display{
"
begin math define pyk of peano commutativity as text "peano commutativity" end text end define end math
end "}
%%%%%%%%%%%%%% Tex Definitions %%%%%%%%%%%%%%
%\subsection{\TeX\ Definitions}\label{section:TexDefinitions}
%\section{\TeX\ Definitions}\label{section:TexDefinitions}
%\begin{list}{}{
%\setlength{\leftmargin}{5em}
%\setlength{\itemindent}{-5em}}
%\immediate\closeout\outex
%\input{./page.otx}
%\end{list}
%%%%%%%%%%%%%% Priority Table %%%%%%%%%%%%%%
%\subsection{Priority Table}\label{section:PriorityTable}
\section{Priority Table}\label{section:PriorityTable}
%"
begin flush left math define priority of peano commutativity as preassociative priority peano commutativity equal priority base equal priority bracket x end bracket equal priority big bracket x end bracket equal priority math x end math equal priority flush left x end left equal priority var x equal priority var y equal priority var z equal priority proclaim x as x end proclaim equal priority define x of x as x end define equal priority pyk equal priority tex equal priority tex name equal priority priority equal priority x equal priority true equal priority if x then x else x end if equal priority introduce x of x as x end introduce equal priority value equal priority claim equal priority bottom equal priority function f of x end function equal priority identity x end identity equal priority false equal priority untagged zero equal priority untagged one equal priority untagged two equal priority untagged three equal priority untagged four equal priority untagged five equal priority untagged six equal priority untagged seven equal priority untagged eight equal priority untagged nine equal priority zero equal priority one equal priority two equal priority three equal priority four equal priority five equal priority six equal priority seven equal priority eight equal priority nine equal priority var a equal priority var b equal priority var c equal priority var d equal priority var e equal priority var f equal priority var g equal priority var h equal priority var i equal priority var j equal priority var k equal priority var l equal priority var m equal priority var n equal priority var o equal priority var p equal priority var q equal priority var r equal priority var s equal priority var t equal priority var u equal priority var v equal priority var w equal priority tagged parenthesis x end tagged equal priority tagged if x then x else x end if equal priority array x is x end array equal priority left equal priority center equal priority right equal priority empty equal priority substitute x set x to x end substitute equal priority map tag x end tag equal priority raw map untag x end untag equal priority map untag x end untag equal priority normalizing untag x end untag equal priority apply x to x end apply equal priority apply one x to x end apply equal priority identifier x end identifier equal priority identifier one x plus id x end identifier equal priority array plus x and x end plus equal priority array remove x array x level x end remove equal priority array put x value x array x level x end put equal priority array add x value x index x value x level x end add equal priority bit x of x end bit equal priority bit one x of x end bit equal priority example rack equal priority vector hook equal priority bibliography hook equal priority dictionary hook equal priority body hook equal priority codex hook equal priority expansion hook equal priority code hook equal priority cache hook equal priority diagnose hook equal priority pyk aspect equal priority tex aspect equal priority texname aspect equal priority value aspect equal priority message aspect equal priority macro aspect equal priority definition aspect equal priority unpack aspect equal priority claim aspect equal priority priority aspect equal priority lambda identifier equal priority apply identifier equal priority true identifier equal priority if identifier equal priority quote identifier equal priority proclaim identifier equal priority define identifier equal priority introduce identifier equal priority hide identifier equal priority pre identifier equal priority post identifier equal priority eval x stack x cache x end eval equal priority eval two x ref x id x stack x cache x end eval equal priority eval three x function x stack x cache x end eval equal priority eval four x arguments x stack x cache x end eval equal priority lookup x stack x default x end lookup equal priority abstract x term x stack x cache x end abstract equal priority quote x end quote equal priority expand x state x cache x end expand equal priority expand two x definition x state x cache x end expand equal priority expand list x state x cache x end expand equal priority macro equal priority macro state equal priority zip x with x end zip equal priority assoc one x address x index x end assoc equal priority protect x end protect equal priority self equal priority macro define x as x end define equal priority value define x as x end define equal priority intro define x as x end define equal priority pyk define x as x end define equal priority tex define x as x end define equal priority tex name define x as x end define equal priority priority table x end table equal priority macro define one equal priority macro define two x end define equal priority macro define three x end define equal priority macro define four x state x cache x definition x end define equal priority state expand x state x cache x end expand equal priority quote expand x term x stack x end expand equal priority quote expand two x term x stack x end expand equal priority quote expand three x term x stack x value x end expand equal priority quote expand star x term x stack x end expand equal priority parenthesis x end parenthesis equal priority aspect x subcodex x end aspect equal priority aspect x term x cache x end aspect equal priority tuple x end tuple equal priority tuple one x end tuple equal priority tuple two x end tuple equal priority let two x apply x end let equal priority let one x apply x end let equal priority claim define x as x end define equal priority checker equal priority check x cache x end check equal priority check two x cache x def x end check equal priority check three x cache x def x end check equal priority check list x cache x end check equal priority check list two x cache x value x end check equal priority test x end test equal priority false test x end test equal priority raw test x end test equal priority message equal priority message define x as x end define equal priority the statement aspect equal priority statement equal priority statement define x as x end define equal priority example axiom equal priority example scheme equal priority example rule equal priority absurdity equal priority contraexample equal priority example theory primed equal priority example lemma equal priority metavar x end metavar equal priority meta a equal priority meta b equal priority meta c equal priority meta d equal priority meta e equal priority meta f equal priority meta g equal priority meta h equal priority meta i equal priority meta j equal priority meta k equal priority meta l equal priority meta m equal priority meta n equal priority meta o equal priority meta p equal priority meta q equal priority meta r equal priority meta s equal priority meta t equal priority meta u equal priority meta v equal priority meta w equal priority meta x equal priority meta y equal priority meta z equal priority sub x set x to x end sub equal priority sub star x set x to x end sub equal priority the empty set equal priority example remainder equal priority make visible x end visible equal priority intro x index x pyk x tex x end intro equal priority intro x pyk x tex x end intro equal priority error x term x end error equal priority error two x term x end error equal priority proof x term x cache x end proof equal priority proof two x term x end proof equal priority sequent eval x term x end eval equal priority seqeval init x term x end eval equal priority seqeval modus x term x end eval equal priority seqeval modus one x term x sequent x end eval equal priority seqeval verify x term x end eval equal priority seqeval verify one x term x sequent x end eval equal priority sequent eval plus x term x end eval equal priority seqeval plus one x term x sequent x end eval equal priority seqeval minus x term x end eval equal priority seqeval minus one x term x sequent x end eval equal priority seqeval deref x term x end eval equal priority seqeval deref one x term x sequent x end eval equal priority seqeval deref two x term x sequent x def x end eval equal priority seqeval at x term x end eval equal priority seqeval at one x term x sequent x end eval equal priority seqeval infer x term x end eval equal priority seqeval infer one x term x premise x sequent x end eval equal priority seqeval endorse x term x end eval equal priority seqeval endorse one x term x side x sequent x end eval equal priority seqeval est x term x end eval equal priority seqeval est one x term x name x sequent x end eval equal priority seqeval est two x term x name x sequent x def x end eval equal priority seqeval all x term x end eval equal priority seqeval all one x term x variable x sequent x end eval equal priority seqeval cut x term x end eval equal priority seqeval cut one x term x forerunner x end eval equal priority seqeval cut two x term x forerunner x sequent x end eval equal priority computably true x end true equal priority claims x cache x ref x end claims equal priority claims two x cache x ref x end claims equal priority the proof aspect equal priority proof equal priority lemma x says x end lemma equal priority proof of x reads x end proof equal priority in theory x lemma x says x end lemma equal priority in theory x antilemma x says x end antilemma equal priority in theory x rule x says x end rule equal priority in theory x antirule x says x end antirule equal priority verifier equal priority verify one x end verify equal priority verify two x proofs x end verify equal priority verify three x ref x sequents x diagnose x end verify equal priority verify four x premises x end verify equal priority verify five x ref x array x sequents x end verify equal priority verify six x ref x list x sequents x end verify equal priority verify seven x ref x id x sequents x end verify equal priority cut x and x end cut equal priority head x end head equal priority tail x end tail equal priority rule one x theory x end rule equal priority rule x subcodex x end rule equal priority rule tactic equal priority plus x and x end plus equal priority theory x end theory equal priority theory two x cache x end theory equal priority theory three x name x end theory equal priority theory four x name x sum x end theory equal priority example axiom lemma primed equal priority example scheme lemma primed equal priority example rule lemma primed equal priority contraexample lemma primed equal priority example axiom lemma equal priority example scheme lemma equal priority example rule lemma equal priority contraexample lemma equal priority example theory equal priority ragged right equal priority ragged right expansion equal priority parameter term x stack x seed x end parameter equal priority parameter term star x stack x seed x end parameter equal priority instantiate x with x end instantiate equal priority instantiate star x with x end instantiate equal priority occur x in x substitution x end occur equal priority occur star x in x substitution x end occur equal priority unify x with x substitution x end unify equal priority unify star x with x substitution x end unify equal priority unify two x with x substitution x end unify equal priority ell a equal priority ell b equal priority ell c equal priority ell d equal priority ell e equal priority ell f equal priority ell g equal priority ell h equal priority ell i equal priority ell j equal priority ell k equal priority ell l equal priority ell m equal priority ell n equal priority ell o equal priority ell p equal priority ell q equal priority ell r equal priority ell s equal priority ell t equal priority ell u equal priority ell v equal priority ell w equal priority ell x equal priority ell y equal priority ell z equal priority ell big a equal priority ell big b equal priority ell big c equal priority ell big d equal priority ell big e equal priority ell big f equal priority ell big g equal priority ell big h equal priority ell big i equal priority ell big j equal priority ell big k equal priority ell big l equal priority ell big m equal priority ell big n equal priority ell big o equal priority ell big p equal priority ell big q equal priority ell big r equal priority ell big s equal priority ell big t equal priority ell big u equal priority ell big v equal priority ell big w equal priority ell big x equal priority ell big y equal priority ell big z equal priority ell dummy equal priority sequent reflexivity equal priority tactic reflexivity equal priority sequent commutativity equal priority tactic commutativity equal priority the tactic aspect equal priority tactic equal priority tactic define x as x end define equal priority proof expand x state x cache x end expand equal priority proof expand list x state x cache x end expand equal priority proof state equal priority conclude one x cache x end conclude equal priority conclude two x proves x cache x end conclude equal priority conclude three x proves x lemma x substitution x end conclude equal priority conclude four x lemma x end conclude equal priority peano equal priority peano zero equal priority peano one equal priority peano two equal priority peano a equal priority peano b equal priority peano c equal priority peano d equal priority peano e equal priority peano f equal priority peano g equal priority peano h equal priority peano i equal priority peano j equal priority peano k equal priority peano l equal priority peano m equal priority peano n equal priority peano o equal priority peano p equal priority peano q equal priority peano r equal priority peano s equal priority peano t equal priority peano u equal priority peano v equal priority peano w equal priority peano x equal priority peano y equal priority peano z equal priority peano nonfree x in x end nonfree equal priority peano nonfree star x in x end nonfree equal priority peano free x set x to x end free equal priority peano free star x set x to x end free equal priority peano sub x is x where x is x end sub equal priority peano sub star x is x where x is x end sub equal priority system s equal priority axiom a one equal priority axiom a two equal priority axiom a three equal priority axiom a four equal priority axiom a five equal priority axiom s one equal priority axiom s two equal priority axiom s three equal priority axiom s four equal priority axiom s five equal priority axiom s six equal priority axiom s seven equal priority axiom s eight equal priority axiom s nine equal priority rule mp equal priority rule gen equal priority lemma l three two a equal priority system prime s equal priority axiom prime a one equal priority axiom prime a two equal priority axiom prime a three equal priority axiom prime a four equal priority axiom prime a five equal priority axiom prime s one equal priority axiom prime s two equal priority axiom prime s three equal priority axiom prime s four equal priority axiom prime s five equal priority axiom prime s six equal priority axiom prime s seven equal priority axiom prime s eight equal priority axiom prime s nine equal priority rule prime mp equal priority rule prime gen equal priority lemma prime l three two a equal priority mendelson one seven equal priority hypothetical rule prime mp equal priority hypothesize equal priority hypothetical rule prime gen equal priority mendelson three two a equal priority hypothetical three two a equal priority hypothetical three two b equal priority hypothetical three one s one equal priority hypothetical three two c equal priority hypothetical three one s two equal priority hypothetical three one s five equal priority hypothetical three one s six equal priority mendelson three two f equal priority mendelson lemma one eight equal priority mendelson proposition three two a equal priority mendelson proposition three two b equal priority mendelson proposition three two c equal priority mendelson proposition three two d equal priority mendelson proposition three two f i equal priority mendelson proposition three two f ii equal priority mendelson proposition three two f equal priority mendelson proposition three two g i equal priority mendelson proposition three two g ii equal priority mendelson proposition three two g equal priority mendelson proposition three two h i equal priority mendelson proposition three two h g ii equal priority mendelson proposition three two h ii equal priority mendelson proposition three two h equal priority mendelson tautology a equal priority mendelson tautology b end priority greater than preassociative priority x sub x end sub equal priority x prime equal priority x assoc x end assoc equal priority x set x to x end set equal priority x set multi x to x end set equal priority x peano var end priority greater than preassociative priority unicode start of text x end unicode text equal priority unicode end of text equal priority text x end text equal priority text x plus x equal priority text x plus indent x equal priority
unicode newline x equal priority unicode space x equal priority unicode exclamation mark x equal priority unicode quotation mark x equal priority unicode number sign x equal priority unicode dollar sign x equal priority unicode percent x equal priority unicode ampersand x equal priority unicode apostrophe x equal priority unicode left parenthesis x equal priority unicode right parenthesis x equal priority unicode asterisk x equal priority unicode plus sign x equal priority unicode comma x equal priority unicode hyphen x equal priority unicode period x equal priority unicode slash x equal priority unicode zero x equal priority unicode one x equal priority unicode two x equal priority unicode three x equal priority unicode four x equal priority unicode five x equal priority unicode six x equal priority unicode seven x equal priority unicode eight x equal priority unicode nine x equal priority unicode colon x equal priority unicode semicolon x equal priority unicode less than x equal priority unicode equal sign x equal priority unicode greater than x equal priority unicode question mark x equal priority unicode commercial at x equal priority unicode capital a x equal priority unicode capital b x equal priority unicode capital c x equal priority unicode capital d x equal priority unicode capital e x equal priority unicode capital f x equal priority unicode capital g x equal priority unicode capital h x equal priority unicode capital i x equal priority unicode capital j x equal priority unicode capital k x equal priority unicode capital l x equal priority unicode capital m x equal priority unicode capital n x equal priority unicode capital o x equal priority unicode capital p x equal priority unicode capital q x equal priority unicode capital r x equal priority unicode capital s x equal priority unicode capital t x equal priority unicode capital u x equal priority unicode capital v x equal priority unicode capital w x equal priority unicode capital x x equal priority unicode capital y x equal priority unicode capital z x equal priority unicode left bracket x equal priority unicode backslash x equal priority unicode right bracket x equal priority unicode circumflex x equal priority unicode underscore x equal priority unicode grave accent x equal priority unicode small a x equal priority unicode small b x equal priority unicode small c x equal priority unicode small d x equal priority unicode small e x equal priority unicode small f x equal priority unicode small g x equal priority unicode small h x equal priority unicode small i x equal priority unicode small j x equal priority unicode small k x equal priority unicode small l x equal priority unicode small m x equal priority unicode small n x equal priority unicode small o x equal priority unicode small p x equal priority unicode small q x equal priority unicode small r x equal priority unicode small s x equal priority unicode small t x equal priority unicode small u x equal priority unicode small v x equal priority unicode small w x equal priority unicode small x x equal priority unicode small y x equal priority unicode small z x equal priority unicode left brace x equal priority unicode vertical line x equal priority unicode right brace x equal priority unicode tilde x equal priority preassociative x greater than x equal priority postassociative x greater than x equal priority priority x equal x equal priority priority x end priority equal priority newline x equal priority macro newline x end priority greater than preassociative priority x bit nil equal priority x bit one equal priority binary equal priority x color x end color equal priority x color star x end color end priority greater than preassociative priority x apply x equal priority x tagged apply x end priority greater than preassociative priority x raw head equal priority x raw tail equal priority x cardinal untag equal priority x head equal priority x tail equal priority x is singular equal priority x is cardinal equal priority x is data equal priority x is atomic equal priority x cardinal retract equal priority x tagged retract equal priority x boolean retract equal priority x ref equal priority x id equal priority x debug equal priority x root equal priority x zeroth equal priority x first equal priority x second equal priority x third equal priority x fourth equal priority x fifth equal priority x sixth equal priority x seventh equal priority x eighth equal priority x ninth equal priority x is error equal priority x is metavar equal priority x is metaclosed equal priority x is metaclosed star equal priority x peano succ end priority greater than preassociative priority x times x equal priority x times zero x equal priority x peano times x end priority greater than preassociative priority x plus x equal priority x plus zero x equal priority x plus one x equal priority x minus x equal priority x minus zero x equal priority x minus one x equal priority x peano plus x end priority greater than preassociative priority x term plus x end plus equal priority x term union x equal priority x term minus x end minus end priority greater than postassociative priority x raw pair x equal priority x eager pair x equal priority x tagged pair x equal priority x untagged double x equal priority x pair x equal priority x double x end priority greater than postassociative priority x comma x end priority greater than preassociative priority x boolean equal x equal priority x data equal x equal priority x cardinal equal x equal priority x peano equal x equal priority x tagged equal x equal priority x math equal x equal priority x reduce to x equal priority x term equal x equal priority x term list equal x equal priority x term root equal x equal priority x term in x equal priority x term subset x equal priority x term set equal x equal priority x sequent equal x equal priority x free in x equal priority x free in star x equal priority x free for x in x equal priority x free for star x in x equal priority x claim in x equal priority x less x equal priority x less zero x equal priority x less one x equal priority x peano is x equal priority x is peano var end priority greater than preassociative priority not x equal priority peano not x end priority greater than preassociative priority x and x equal priority x macro and x equal priority x simple and x equal priority x claim and x equal priority x peano and x end priority greater than preassociative priority x or x equal priority x parallel x equal priority x macro or x equal priority x peano or x end priority greater than preassociative priority peano all x indeed x equal priority peano exist x indeed x end priority greater than postassociative priority x macro imply x equal priority x peano imply x equal priority x peano iff x end priority greater than postassociative priority x guard x equal priority x tagged guard x end priority greater than preassociative priority x select x else x end select end priority greater than preassociative priority lambda x dot x equal priority tagging x equal priority open if x then x else x equal priority let x be x in x equal priority let x abbreviate x in x end priority greater than preassociative priority x init equal priority x modus equal priority x verify equal priority x curry plus equal priority x curry minus equal priority x dereference end priority greater than preassociative priority x at x equal priority x modus ponens x equal priority x modus probans x equal priority x conclude x end priority greater than postassociative priority x infer x equal priority x endorse x equal priority x id est x end priority greater than preassociative priority all x indeed x end priority greater than postassociative priority x rule plus x end priority greater than postassociative priority x cut x end priority greater than preassociative priority x proves x end priority greater than preassociative priority x proof of x reads x equal priority line x because x indeed x end line x equal priority because x indeed x qed equal priority line x premise x end line x equal priority line x side condition x end line x equal priority arbitrary x end line x equal priority locally define x as x end line x end priority greater than postassociative priority x
then x equal priority x
begin x
end x end priority greater than preassociative priority x tab x end priority greater than preassociative priority x row
x end priority greater than unicode end of text end define end math end left
end "
%%%%%%%%%%%%%% Bibliography %%%%%%%%%%%%%%
\section{Bibliography}
\bibliography{./page}
\end{document}
End of file
File page.bib
@book {mendelson,
author = {E. Mendelson},
title = {Introduction to Mathematical Logic},
publisher = {Wadsworth and Brooks},
year = {1987},
edition = {3.}}
@book {grue:base,
author = {Klaus Grue},
title = {A Logiweb base page},
publisher = {http://www.diku.dk/\verb+~+grue/logiweb/ 20050502/home/grue/base/latest/},
year = {2005}}
@book {grue:peano,
author = {Klaus Grue},
title = {Peano arithmetic},
publisher = {http://www.diku.dk/\verb+~+grue/logiweb/ 20050502/home/grue/peano-axioms/latest/},
year = {2005}}
@book {grue:check,
author = {Klaus Grue},
title = {Introduction to Logiweb},
publisher = {http://www.diku.dk/\verb+~+grue/logiweb/ 20050502/home/grue/check/GRD-2005-05-26-UTC-06-49-32-964854/},
year = {2005}}
End of file
File page.sty
% thebibliography environment from
% /usr/share/texmf/tex/latex/base/book.cls
% with \chapter removed
\renewenvironment{thebibliography}[1]
{\list{\@biblabel{\@arabic\c@enumiv}}%
{\settowidth\labelwidth{\@biblabel{#1}}%
\leftmargin\labelwidth
\advance\leftmargin\labelsep
\@openbib@code
\usecounter{enumiv}%
\let\p@enumiv\@empty
\renewcommand\theenumiv{\@arabic\c@enumiv}}%
\sloppy
\clubpenalty4000
\@clubpenalty \clubpenalty
\widowpenalty4000%
\sfcode`\.\@m}
{\def\@noitemerr
{\@latex@warning{Empty `thebibliography' environment}}%
\endlist}
End of file
latex page
bibtex page
latex page
latex page"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,