"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[english]{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 expansion
end "
\newpage
%%%%%%%%%% Introduction %%%%%%%%%%
\section{Introduction}
This report is turned in for credit for the course ``Logic'' at DIKU
summer 2005. In brief, 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
numbers the following holds:
\begin{equation}\label{eq:commu}
t + r = r + t,
\end{equation}
\noindent and we shall use Klaus Grue's Logiweb system to check our proof.
Cf.~\cite{grue:check}. However, we use "
begin bracket peano x end bracket
end " and
"
begin bracket peano y end bracket
end " as our variables.
During the course we have been introduced to mathematical logic using
the textbook \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 simply 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 any 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 well
displays the system ``at work''. In order to obtain a thorough knowledge
of the system one is advised to follow the course ``Logic'' or to read
the \href{\lgwBaseUrl}{base} page (cf.~\cite{grue:base}), but probably
the best choice would be to undertake the exercise of writing a page
proving some proposition of choice from~\cite{mendelson} using Logiweb.
After such an exercise any work in Logiweb and the hardship of doing it
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 worldwide can
distribute their own mathematical work and reuse the work of others.
Mathematics in Logiweb is published 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 be defined in one page. The proofs within a theory
will be proof checked upon submission to the Logiweb system (actually
they will be proof checked when compiling the page locally) 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 together they form a
directed acyclic graph from top (the base) to bottom (a Logiweb page).
Essentially, the Logiweb reference of a page is a 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}
\noindent \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
\url{http://www.diku.dk/~grue/logiweb/20050502/home/mrmr/peano-commutativity/latest/vector/page.lgw}}
\end{quote}
The two last ways to refer to a page is using the reference expressed in
so-called \emph{mixed endian hexadecimal}---which the kana reference is
based on---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 can be 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 forms 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 briefly 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 instance of a 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 beginners) the source code.
A Logiweb page is written in a mixture of {\LaTeX} and the language
\texttt{pyk} developed by Klaus Grue. \texttt{pyk} is the language
in which the mathematics 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 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 general for ``spoken
mathematics'', cf. the \href{\lgwBaseUrl}{base} page, Section 1.1. Thus,
a mathematical expression we are well-acquaintated with, such as:
\[ ( x + y ) ^ 2 = x ^ 2 + 2 x y + y ^ 2 \]
\noindent may correspond to 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, eventually one will be able to ``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 be 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 lowercase 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''. This
also appears in Appendix \ref{section:Page} of this page where the acutal
definition takes place.
\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
refers to once referenced pages. The Logiweb server will make sure no
cyclic references occur. We note that the \texttt{BIBLIOGRAPHY} section
of a Logiweb page is not the bibliography seen in Appendix
\ref{section:Bibliography}, which is the normal list of referenced
books, articles etc.
\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 the same priority. (In a sense the \emph{constructs} of a
Logiweb page make up the available \texttt{pyk} code in a page and/or
pages referring to the page declaring and defining the constructs.)
Thus, we get that:
\begin{quote}
\texttt{PREASSOCIATIVE * plus *, * minus *}
\end{quote}
\noindent indicates that, e.g., "
begin bracket var x plus var y end bracket
end " is to have the same priority as "
begin bracket var x minus var y end bracket
end ", whereas:
\begin{quote}
\texttt{PREASSOCIATIVE * times *} \\
\vdots \\
\texttt{PREASSOCIATIVE * plus *}
\end{quote}
\noindent indicates that, e.g., "
begin bracket var x times var y end bracket
end " is to 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 referring page with \texttt{base}
written after the associativity assignment. When using the names of
constructs from a page in the associativity section of another page one
is to place the priority of new constructs in proper hierarchical order.
Thus, in the associativity section of the present 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}
It might be confusing that \texttt{mendelson lemma one eight} and other
constructs declared and defined on a certain page does not have the name
of the page in front of the declaration in the associativity section,
but one gets used to this and quickly learn to distinguish.
The associativites can be found in the priority table of Appendix
~\ref{section:PriorityTable}.
\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
acquainted 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 structure for a Logiweb page as is seen in Figure
\ref{fig:Structure}
\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{The structure of a Logiweb page.}\label{fig:Structure}
}
\end{figure}
The above only gives a bland taste of the richness of the very complex
and impressive system that Logiweb is. But as stated earlier we believe
it should be enough to get the reader started. To set up a system one is
advised to read the \texttt{Pyk how-to} at:
\begin{quote}
{\scriptsize \url{http://diku.dk/undervisning/2005s/235/howto.html}}
\end{quote}
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 turns out not to be
enough when expressing more complex systems of logic. Though it took our
ancestors a couple of millennia to give us the formalistic tools to
express even 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 a communist'' and ``Jones is an
atheist'', and a few logical connectives, e.g. $\neg$ and $\Rightarrow$,
can be combined 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 when written in plural.
\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 set of $j$ wfs and each $\mathcal{B}$, one can
effectively decide whether the given $j$ wfs are in the relation $R_i$
to $\mathcal{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 $\mathcal{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 finite 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 prerequisites 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 abbreviated as $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}
The conceptual framework introduced in the previous subsection
is the one we shall work in when proving the law of 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 intro mendelson lemma one eight pyk "mendelson lemma one eight" tex "M\ Lemma\ 1.8" end intro
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 one reads 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 in 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 in theory system prime s lemma mendelson lemma one eight says all meta b indeed meta b peano imply meta b end lemma 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
\href{\lgwPeanoUrl}{peano} page. For now, we shall use these without
further introduction, which we defer until the next section: \\
\noindent
"
begin math system prime s proof of mendelson lemma one eight reads arbitrary meta b end line line ell a because axiom prime a two indeed parenthesis meta b peano imply parenthesis meta b peano imply meta b end parenthesis peano imply meta b end parenthesis peano imply parenthesis parenthesis meta b peano imply parenthesis meta b peano imply meta b end parenthesis end parenthesis peano imply parenthesis meta b peano imply meta b end parenthesis end parenthesis end line line ell b because axiom prime a one indeed meta b peano imply parenthesis parenthesis meta b peano imply meta b end parenthesis peano imply meta b end parenthesis end line line ell c because rule prime mp modus ponens ell a modus ponens ell b indeed parenthesis meta b peano imply parenthesis meta b peano imply meta b end parenthesis end parenthesis peano imply parenthesis meta b peano imply meta b end parenthesis end line line ell d because axiom prime a one indeed meta b peano imply parenthesis meta b peano imply meta b end parenthesis end line because rule prime mp modus ponens ell c modus ponens ell d indeed meta b peano imply meta b qed end math
end "
\\
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 are reproduced in the following subsections; they are
introduced and defined in \cite{grue:peano}. The appearance 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 arithmetic 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{"
begin bracket system prime s end bracket
end " Axioms}
In peano arithmetic---or in "
begin math theory system prime s end theory 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. We assume that the special symbols used are known to the reader.
\display{"
begin math in theory system prime s rule axiom prime a one says all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a two says all meta a indeed all meta b indeed all meta c indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a three says all meta a indeed all meta b indeed parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a four says all meta c indeed all meta a indeed all meta x indeed all meta b indeed peano sub quote meta a end quote is quote meta b end quote where quote meta x end quote is quote meta c end quote end sub endorse peano all meta x indeed meta b peano imply meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a five says all meta x indeed all meta a indeed all meta b indeed newline peano nonfree quote meta x end quote in quote meta a end quote end nonfree endorse peano all meta x indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply peano all meta x indeed meta b end rule end math
end "}
These definitions are copied from the \href{\lgwPeanoUrl}{peano} page,
Section 1.5.
%%%%% text... %%%%%
\subsubsection{"
begin bracket system prime s end bracket
end " Rules of Inference}
Besides the five axioms "
begin bracket system prime s end bracket
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 in theory system prime s rule rule prime mp says all meta a indeed all meta b indeed meta a peano imply meta b infer meta a infer meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule rule prime gen says all meta x indeed all meta a indeed meta a infer peano all meta x indeed meta a end rule end math
end "}
These definitions are copied from the \href{\lgwPeanoUrl}{peano} page,
Section 1.5.
%%%%% text... %%%%%
\subsubsection{"
begin bracket system prime s end bracket
end " Theorems}
Finally, within "
begin bracket system prime s end bracket
end " we
are allowed to use the following theorems. We shall not prove these:
%%%%% ...text %%%%%
\display{"
begin math in theory system prime s rule axiom prime s one says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta a peano is meta c peano imply meta b peano is meta c end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s two says all meta a indeed all meta b indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s three says all meta a indeed not peano zero peano is meta a peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s four says all meta a indeed all meta b indeed meta a peano succ peano is meta b peano succ peano imply meta a peano is meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s five says all meta a indeed meta a peano plus peano zero peano is meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s six says all meta a indeed all meta b indeed meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s seven says all meta a indeed meta a peano times peano zero peano is peano zero end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s eight says all meta a indeed all meta b indeed meta a peano times parenthesis meta b peano succ end parenthesis peano is parenthesis meta a peano times meta b end parenthesis peano plus meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s nine says all meta a indeed all meta b indeed all meta c indeed all meta x indeed macro newline peano sub meta b is meta a where meta x is peano zero end sub endorse peano sub meta c is meta a where meta x is meta x peano succ end sub endorse macro newline meta b peano imply peano all meta x indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta x indeed meta a end rule end math
end "}
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 final 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 a basic and expected
proposition---and quite logical!
\\
\noindent
"
begin intro mendelson proposition three two a pyk "mendelson proposition three two a" tex "M\ Proposition\ 3.2(a)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two a says all meta t indeed meta t peano is meta t end lemma end math
end "
\\
%%%%% Proof of 3.2(a) %%%%%
\noindent
"
begin math system prime s proof of mendelson proposition three two a reads arbitrary meta t end line line ell a because axiom prime s five indeed meta t peano plus peano zero peano is meta t end line line ell b because axiom prime s one indeed parenthesis meta t peano plus peano zero peano is meta t end parenthesis peano imply parenthesis meta t peano plus peano zero peano is meta t peano imply meta t peano is meta t end parenthesis end line line ell c because rule prime mp modus ponens ell b modus ponens ell a indeed meta t peano plus peano zero peano is meta t peano imply meta t peano is meta t end line because rule prime mp modus ponens ell c modus ponens ell a indeed meta t peano is meta t qed 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 intro mendelson tautology a pyk "mendelson tautology a" tex "M\ Tautology\ A" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson tautology a says all meta a indeed all meta b indeed all meta c indeed meta a peano imply parenthesis meta b peano imply meta c end parenthesis infer meta b peano imply parenthesis meta a peano imply meta c end parenthesis end lemma end math
end "
\\
%%%%% Proof of Tautology A %%%%%
\noindent
"
begin math system prime s proof of mendelson tautology a reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply parenthesis meta b peano imply meta c end parenthesis end line line ell b because axiom prime a two indeed parenthesis meta a peano imply parenthesis meta b peano imply meta c end parenthesis end parenthesis peano imply parenthesis parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end line line ell c because rule prime mp modus ponens ell b modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end line line ell d because axiom prime a one indeed parenthesis parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis peano imply parenthesis parenthesis meta b peano imply parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end parenthesis end line line ell e because rule prime mp modus ponens ell d modus ponens ell c indeed meta b peano imply parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end line line ell f because axiom prime a two indeed parenthesis meta b peano imply parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis peano imply parenthesis meta b peano imply parenthesis meta a peano imply meta b end parenthesis end parenthesis peano imply parenthesis meta b peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end line line ell g because rule prime mp modus ponens ell f modus ponens ell e indeed parenthesis meta b peano imply parenthesis meta a peano imply meta b end parenthesis end parenthesis peano imply parenthesis meta b peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end line line ell h because axiom prime a one indeed meta b peano imply parenthesis meta a peano imply meta b end parenthesis end line because rule prime mp modus ponens ell g modus ponens ell h indeed meta b peano imply parenthesis meta a peano imply meta c end parenthesis qed end math
end "
\\
We note that "
begin bracket mendelson proposition three two b end bracket
end "
could also be proved by means of Corollary 1.10(b),
cf.~\cite{mendelson}, p. 38. Mendelson proves this by the use of
Proposition 1.9 also known 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 intro mendelson proposition three two b pyk "mendelson proposition three two b" tex "M\ Proposition\ 3.2(b)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two b says all meta t indeed all meta r indeed meta t peano is meta r peano imply meta r peano is meta t end lemma end math
end "
\\
%%%%% Proof of Proposition 3.2(b) %%%%%
\noindent
"
begin math system prime s proof of mendelson proposition three two b reads arbitrary meta t end line arbitrary meta r end line line ell a because axiom prime s one indeed meta t peano is meta r peano imply parenthesis meta t peano is meta t peano imply meta r peano is meta t end parenthesis end line line ell b because mendelson tautology a modus ponens ell a indeed meta t peano is meta t peano imply parenthesis meta t peano is meta r peano imply meta r peano is meta t end parenthesis end line line ell c because mendelson proposition three two a indeed meta t peano is meta t end line because rule prime mp modus ponens ell b modus ponens ell c indeed meta t peano is meta r peano imply meta r peano is meta t qed end math
end "
\\
Thus having proved "
begin bracket mendelson proposition three two b end bracket
end " we proceed to [Proposition 3.2(c)] in the proof of which the
former is used. But before we do this we need yet \mbox{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 "
begin math mendelson proposition three two c end math
end " we see
that a tautology is used. We shall state and prove this tautology for
use in our next and later proofs.
\\
\noindent
"
begin intro mendelson tautology b pyk "mendelson tautology b" tex "M\ Tautology\ B" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson tautology b says all meta d indeed all meta e indeed all meta f indeed meta d peano imply meta e infer meta e peano imply meta f infer meta d peano imply meta f end lemma end math
end "
\\
%%%%% Proof of Tautology B %%%%%
\noindent
"
begin math system prime s proof of mendelson tautology b reads arbitrary meta d end line arbitrary meta e end line arbitrary meta f end line line ell a premise meta d peano imply meta e end line line ell b premise meta e peano imply meta f end line line ell c because axiom prime a one indeed parenthesis meta e peano imply meta f end parenthesis peano imply parenthesis meta d peano imply parenthesis meta e peano imply meta f end parenthesis end parenthesis end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed meta d peano imply parenthesis meta e peano imply meta f end parenthesis end line line ell e because axiom prime a two indeed parenthesis meta d peano imply parenthesis meta e peano imply meta f end parenthesis end parenthesis peano imply parenthesis parenthesis meta d peano imply meta e end parenthesis peano imply parenthesis meta d peano imply meta f end parenthesis end parenthesis end line line ell f because rule prime mp modus ponens ell e modus ponens ell d indeed parenthesis meta d peano imply meta e end parenthesis peano imply parenthesis meta d peano imply meta f end parenthesis end line because rule prime mp modus ponens ell f modus ponens ell a indeed meta d peano imply meta f qed 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 [Proposition 3.2(c)], which concerns transitivity.
\\
\noindent
"
begin intro mendelson proposition three two c pyk "mendelson proposition three two c" tex "M\ Proposition\ 3.2(c)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two c says all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r peano imply parenthesis meta r peano is meta s peano imply meta t peano is meta s end parenthesis end lemma end math
end "
\\
%%%%% Proof of Proposition 3.2(c) %%%%%
\noindent
"
begin math system prime s proof of mendelson proposition three two c reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a because axiom prime s one indeed meta r peano is meta t peano imply parenthesis meta r peano is meta s peano imply meta t peano is meta s end parenthesis end line line ell b because mendelson proposition three two b indeed meta t peano is meta r peano imply meta r peano is meta t end line because mendelson tautology b modus ponens ell b modus ponens ell a indeed meta t peano is meta r peano imply parenthesis meta r peano is meta s peano imply meta t peano is meta s end parenthesis qed end math
end "
\\
Thus having proved "
begin bracket mendelson proposition three two c end bracket
end " we now proceed with [Proposition 3.2(d)].
%\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 b 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 intro mendelson proposition three two d pyk "mendelson proposition three two d" tex "M\ Proposition\ 3.2(d)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two d says all meta r indeed all meta t indeed all meta s indeed meta r peano is meta t peano imply parenthesis meta s peano is meta t peano imply meta r peano is meta s end parenthesis end lemma end math
end "
\\
\noindent
"
begin math system prime s proof of mendelson proposition three two d reads arbitrary meta r end line arbitrary meta t end line arbitrary meta s end line line ell a because mendelson proposition three two c indeed meta r peano is meta t peano imply parenthesis meta t peano is meta s peano imply meta r peano is meta s end parenthesis end line line ell b because mendelson tautology a modus ponens ell a indeed meta t peano is meta s peano imply parenthesis meta r peano is meta t peano imply meta r peano is meta s end parenthesis end line line ell c because mendelson proposition three two b indeed meta s peano is meta t peano imply meta t peano is meta s end line line ell d because mendelson tautology b modus ponens ell c modus ponens ell b indeed meta s peano is meta t peano imply parenthesis meta r peano is meta t peano imply meta r peano is meta s end parenthesis end line because mendelson tautology a modus ponens ell d indeed meta r peano is meta t peano imply parenthesis meta s peano is meta t peano imply meta r peano is meta s end parenthesis qed end math
end "
\\
Thus having proved "
begin bracket mendelson proposition three two d end bracket
end " we now proceed with [Proposition 3.2(f)] 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 "}\label{section:3.2f}
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.
Furthermore, we now make use of regular variables and not metavariables
as was the case in the previous proofs. That is, we now show our theorem
to be true not for all terms but for all variables. This does not make a
difference, though.
%\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. This structure is used in the proofs
of the rest of the theorems including the final, namely, [Proposition
3.2(h)] stating the commutative law of addition.
\\
%%%%%%%%%% 3.2(f) (i) %%%%%%%%%%%
\noindent
"
begin intro mendelson proposition three two f i pyk "mendelson proposition three two f i" tex "M\ Proposition\ 3.2(f)\ (i)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two f i says peano zero peano is peano zero peano plus peano zero end lemma end math
end "
\\
\noindent
"
begin math system prime s proof of mendelson proposition three two f i reads line ell a because axiom prime s five indeed peano zero peano plus peano zero peano is peano zero end line line ell b because mendelson proposition three two b indeed peano zero peano plus peano zero peano is peano zero peano imply peano zero peano is peano zero peano plus peano zero end line because rule prime mp modus ponens ell b modus ponens ell a indeed peano zero peano is peano zero peano plus peano zero qed end math
end "
\\
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 intro mendelson proposition three two f ii pyk "mendelson proposition three two f ii" tex "M\ Proposition\ 3.2(f)\ (ii)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two f ii says peano all peano x indeed parenthesis peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end parenthesis end lemma end math
end "
\\
\noindent
"
begin math system prime s proof of mendelson proposition three two f ii reads line ell b because axiom prime s six indeed peano zero peano plus peano x peano succ peano is parenthesis peano zero peano plus peano x end parenthesis peano succ end line line ell c because axiom prime s two indeed peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is parenthesis peano zero peano plus peano x end parenthesis peano succ end line line ell d because mendelson proposition three two d indeed peano x peano succ peano is parenthesis peano zero peano plus peano x end parenthesis peano succ peano imply parenthesis peano zero peano plus peano x peano succ peano is parenthesis peano zero peano plus peano x end parenthesis peano succ peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end parenthesis end line line ell e because mendelson tautology b modus ponens ell c modus ponens ell d indeed peano x peano is peano zero peano plus peano x peano imply parenthesis peano zero peano plus peano x peano succ peano is parenthesis peano zero peano plus peano x end parenthesis peano succ peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end parenthesis end line line ell f because mendelson tautology a modus ponens ell e indeed peano zero peano plus peano x peano succ peano is parenthesis peano zero peano plus peano x end parenthesis peano succ peano imply parenthesis peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end parenthesis end line line ell g because rule prime mp modus ponens ell f modus ponens ell b indeed peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end line because rule prime gen modus ponens ell g indeed peano all peano x indeed parenthesis peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end parenthesis qed 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 "}\label{section:3.2f}
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 intro mendelson proposition three two f pyk "mendelson proposition three two f" tex "M\ Proposition\ 3.2(f)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two f says peano all peano x indeed parenthesis peano x peano is peano zero peano plus peano x end parenthesis end lemma end math
end "
\\
%%%%% Proof of 3.2(f) %%%%%
\noindent
"
begin math system prime s proof of mendelson proposition three two f reads line ell a because axiom prime s nine indeed parenthesis peano zero peano is peano zero peano plus peano zero end parenthesis peano imply peano all peano x indeed parenthesis peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end parenthesis peano imply peano all peano x indeed parenthesis peano x peano is peano zero peano plus peano x end parenthesis end line line ell b because mendelson proposition three two f i indeed peano zero peano is peano zero peano plus peano zero end line line ell c because rule prime mp modus ponens ell a modus ponens ell b indeed peano all peano x indeed parenthesis peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end parenthesis peano imply peano all peano x indeed parenthesis peano x peano is peano zero peano plus peano x end parenthesis end line line ell d because mendelson proposition three two f ii indeed peano all peano x indeed parenthesis peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end parenthesis end line because rule prime mp modus ponens ell c modus ponens ell d indeed peano all peano x indeed parenthesis peano x peano is peano zero peano plus peano x end parenthesis qed 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 similar to our previous proof. In this case, too, 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 base case.
\\
%%%%%%%%%% 3.2(g) (i) %%%%%%%%%%%
\noindent
"
begin intro mendelson proposition three two g i pyk "mendelson proposition three two g i" tex "M\ Proposition\ 3.2(g)\ (i)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two g i says peano all peano x indeed parenthesis peano x peano succ peano plus peano zero peano is parenthesis peano x peano plus peano zero end parenthesis peano succ end parenthesis end lemma end math
end "
\\
%%%%% Proof of 3.2(g) (i) %%%%%
\noindent
"
begin math system prime s proof of mendelson proposition three two g i reads line ell a because axiom prime s five indeed peano x peano succ peano plus peano zero peano is peano x peano succ end line line ell b because axiom prime s five indeed peano x peano plus peano zero peano is peano x end line line ell c because axiom prime s two indeed peano x peano plus peano zero peano is peano x peano imply parenthesis peano x peano plus peano zero end parenthesis peano succ peano is peano x peano succ end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed parenthesis peano x peano plus peano zero end parenthesis peano succ peano is peano x peano succ end line line ell e because mendelson proposition three two d indeed peano x peano succ peano plus peano zero peano is peano x peano succ peano imply parenthesis peano x peano plus peano zero end parenthesis peano succ peano is peano x peano succ peano imply peano x peano succ peano plus peano zero peano is parenthesis peano x peano plus peano zero end parenthesis peano succ end line line ell f because rule prime mp modus ponens ell e modus ponens ell a indeed parenthesis peano x peano plus peano zero end parenthesis peano succ peano is peano x peano succ peano imply peano x peano succ peano plus peano zero peano is parenthesis peano x peano plus peano zero end parenthesis peano succ end line line ell g because rule prime mp modus ponens ell f modus ponens ell d indeed peano x peano succ peano plus peano zero peano is parenthesis peano x peano plus peano zero end parenthesis peano succ end line because rule prime gen modus ponens ell g indeed peano all peano x indeed parenthesis peano x peano succ peano plus peano zero peano is parenthesis peano x peano plus peano zero end parenthesis peano succ end parenthesis qed 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 intro mendelson proposition three two g ii pyk "mendelson proposition three two g ii" tex "M\ Proposition\ 3.2(g)\ (ii)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two g ii says peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y peano succ end parenthesis peano succ end parenthesis end lemma end math
end "
\\
%%%%% Proof of 3.2(g) (ii) %%%%%
\noindent
"
begin math system prime s proof of mendelson proposition three two g ii reads line ell a because axiom prime s six indeed peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano succ peano plus peano y end parenthesis peano succ end line line ell b because axiom prime s two indeed peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply parenthesis peano x peano succ peano plus peano y end parenthesis peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ end line line ell c because mendelson proposition three two c indeed peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano succ peano plus peano y end parenthesis peano succ peano imply parenthesis peano x peano succ peano plus peano y end parenthesis peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ end line line ell d because mendelson tautology a modus ponens ell c indeed parenthesis peano x peano succ peano plus peano y end parenthesis peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano succ peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ end line line ell e because mendelson tautology b modus ponens ell b modus ponens ell d indeed peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano succ peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ end line line ell f because mendelson tautology a modus ponens ell e indeed peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano succ peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ end line line ell g because rule prime mp modus ponens ell f modus ponens ell a indeed peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ end line line ell h because axiom prime s six indeed peano x peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ end line line ell i because axiom prime s two indeed peano x peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply parenthesis peano x peano plus peano y peano succ end parenthesis peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ end line line ell j because mendelson proposition three two d indeed peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ peano imply parenthesis peano x peano plus peano y peano succ end parenthesis peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y peano succ end parenthesis peano succ end line line ell k because mendelson tautology b modus ponens ell g modus ponens ell j indeed peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply parenthesis peano x peano plus peano y peano succ end parenthesis peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y peano succ end parenthesis peano succ end line line ell l because mendelson tautology a modus ponens ell k indeed parenthesis peano x peano plus peano y peano succ end parenthesis peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ peano imply peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y peano succ end parenthesis peano succ end line line ell m because rule prime mp modus ponens ell i modus ponens ell h indeed parenthesis peano x peano plus peano y peano succ end parenthesis peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano succ end line line ell n because rule prime mp modus ponens ell l modus ponens ell m indeed peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y peano succ end parenthesis peano succ end line because rule prime gen modus ponens ell n indeed peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y peano succ end parenthesis peano succ end parenthesis qed 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 intro mendelson proposition three two g pyk "mendelson proposition three two g" tex "M\ Proposition\ 3.2(g)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two g says peano all peano y indeed peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ end lemma end math
end "
\\
%%%%% Proof of 3.2(g) %%%%%
\noindent
"
begin math system prime s proof of mendelson proposition three two g reads line ell a because axiom prime s nine indeed peano all peano x indeed parenthesis peano x peano succ peano plus peano zero peano is parenthesis peano x peano plus peano zero end parenthesis peano succ end parenthesis peano imply peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y peano succ end parenthesis peano succ end parenthesis peano imply peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ end parenthesis end line line ell b because mendelson proposition three two g i indeed peano all peano x indeed parenthesis peano x peano succ peano plus peano zero peano is parenthesis peano x peano plus peano zero end parenthesis peano succ end parenthesis end line line ell c because rule prime mp modus ponens ell a modus ponens ell b indeed peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y peano succ end parenthesis peano succ end parenthesis peano imply peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ end parenthesis end line line ell d because mendelson proposition three two g ii indeed peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano succ peano plus peano y peano succ peano is parenthesis peano x peano plus peano y peano succ end parenthesis peano succ end parenthesis end line because rule prime mp modus ponens ell c modus ponens ell d indeed peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ end parenthesis qed 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 [M
Proposition 3.2(h)]. As was the case for "
begin bracket mendelson proposition three two f end bracket
end " and "
begin bracket mendelson proposition three two g end bracket
end ", this proposition will also be shown
by induction, that is, with a base case and an inductive step but
without an induction theorem, cf. ~ref{section:3.2f}.
%%%%%%%%%% 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 h 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 intro mendelson proposition three two h i pyk "mendelson proposition three two h i" tex "M\ Proposition\ 3.2(h)(i)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two h i says peano all peano x indeed parenthesis peano x peano plus peano zero peano is peano zero peano plus peano x end parenthesis end lemma end math
end "
\\
%%%%% Proof of 3.2(h) (i) %%%%%
\noindent
"
begin math system prime s proof of mendelson proposition three two h i reads line ell a because axiom prime s five indeed peano x peano plus peano zero peano is peano x end line line ell b because mendelson proposition three two f indeed peano all peano x indeed parenthesis peano x peano is peano zero peano plus peano x end parenthesis end line line ell c because axiom prime a four at peano x indeed peano all peano x indeed parenthesis peano x peano is peano zero peano plus peano x end parenthesis peano imply peano x peano is peano zero peano plus peano x end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed peano x peano is peano zero peano plus peano x end line line ell e because mendelson proposition three two c indeed peano x peano plus peano zero peano is peano x peano imply parenthesis peano x peano is peano zero peano plus peano x peano imply peano x peano plus peano zero peano is peano zero peano plus peano x end parenthesis end line line ell f because rule prime mp modus ponens ell e modus ponens ell a indeed peano x peano is peano zero peano plus peano x peano imply peano x peano plus peano zero peano is peano zero peano plus peano x end line line ell g because rule prime mp modus ponens ell f modus ponens ell d indeed peano x peano plus peano zero peano is peano zero peano plus peano x end line because rule prime gen modus ponens ell g indeed peano all peano x indeed parenthesis peano x peano plus peano zero peano is peano zero peano plus peano x end parenthesis qed 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 2 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 swapped. 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 intro mendelson proposition three two h g ii pyk "mendelson proposition three two h g ii" tex "M\ Proposition\ 3.2(h)_{(g)(ii)}" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two h g ii says peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ end parenthesis infer peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end lemma end math
end "
\\
%%%%% Proof of 3.2(h)(g)(ii) %%%%%
"
begin math system prime s proof of mendelson proposition three two h g ii reads line ell a premise peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ end parenthesis end line line ell b because axiom prime a four at peano z indeed peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ end parenthesis peano imply peano x peano succ peano plus peano z peano is parenthesis peano x peano plus peano z end parenthesis peano succ end line line ell c because rule prime mp modus ponens ell b modus ponens ell a indeed peano x peano succ peano plus peano z peano is parenthesis peano x peano plus peano z end parenthesis peano succ end line line ell q because rule prime gen modus ponens ell c indeed peano all peano x indeed parenthesis peano x peano succ peano plus peano z peano is parenthesis peano x peano plus peano z end parenthesis peano succ end parenthesis end line line ell d because axiom prime a four at peano y indeed peano all peano x indeed parenthesis peano x peano succ peano plus peano z peano is parenthesis peano x peano plus peano z end parenthesis peano succ end parenthesis peano imply parenthesis peano y peano succ peano plus peano z peano is parenthesis peano y peano plus peano z end parenthesis peano succ end parenthesis end line line ell e because rule prime mp modus ponens ell d modus ponens ell q indeed peano y peano succ peano plus peano z peano is parenthesis peano y peano plus peano z end parenthesis peano succ end line line ell f because rule prime gen modus ponens ell e indeed peano all peano z indeed parenthesis peano y peano succ peano plus peano z peano is parenthesis peano y peano plus peano z end parenthesis peano succ end parenthesis end line line ell g because axiom prime a four at peano x indeed peano all peano z indeed parenthesis peano y peano succ peano plus peano z peano is parenthesis peano y peano plus peano z end parenthesis peano succ end parenthesis peano imply peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line because rule prime mp modus ponens ell g modus ponens ell f indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ qed end math
end "
\\
We now have the necessary means to prove the induction step of [M
Proposition 3.2(h)(ii)].
%%%%%%%%%% 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 intro mendelson proposition three two h ii pyk "mendelson proposition three two h ii" tex "M\ Proposition\ 3.2(h)(ii)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two h ii says peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end parenthesis end lemma end math
end "
\\
%%%%% Proof of 3.2(h) (ii) %%%%%
\noindent
"
begin math system prime s proof of mendelson proposition three two h ii reads line ell b because axiom prime s six indeed peano x peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ end line line ell c because mendelson proposition three two g indeed peano all peano y indeed parenthesis peano x peano succ peano plus peano y peano is parenthesis peano x peano plus peano y end parenthesis peano succ end parenthesis end line line ell d because mendelson proposition three two h g ii modus ponens ell c indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell i because axiom prime s two indeed peano x peano plus peano y peano is peano y peano plus peano x peano imply parenthesis peano x peano plus peano y end parenthesis peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell k because mendelson proposition three two c indeed peano x peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply parenthesis peano x peano plus peano y end parenthesis peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano x peano plus peano y peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell l because mendelson tautology a modus ponens ell k indeed parenthesis peano x peano plus peano y end parenthesis peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano x peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano plus peano y peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell m because mendelson tautology b modus ponens ell i modus ponens ell l indeed peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano plus peano y peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell n because mendelson tautology a modus ponens ell m indeed peano x peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ peano imply peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell o because rule prime mp modus ponens ell n modus ponens ell b indeed peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell p because mendelson proposition three two d indeed peano x peano plus peano y peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end line line ell q because mendelson tautology b modus ponens ell o modus ponens ell p indeed peano x peano plus peano y peano is peano y peano plus peano x peano imply peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end line line ell r because mendelson tautology a modus ponens ell q indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end line line ell s because rule prime mp modus ponens ell r modus ponens ell d indeed peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end line because rule prime gen modus ponens ell s indeed peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end parenthesis qed 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 intro mendelson proposition three two h pyk "mendelson proposition three two h" tex "M\ Proposition\ 3.2(h)" end intro
end "
\\
\noindent
"
begin math in theory system prime s lemma mendelson proposition three two h says peano all peano x indeed peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x end parenthesis end lemma end math
end "
\\
%%%%% Proof of 3.2(h) %%%%%
"
begin math system prime s proof of mendelson proposition three two h reads line ell a because axiom prime s nine indeed peano all peano x indeed parenthesis peano x peano plus peano zero peano is peano zero peano plus peano x end parenthesis peano imply parenthesis parenthesis peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end parenthesis end parenthesis peano imply peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x end parenthesis end parenthesis end line line ell b because mendelson proposition three two h i indeed peano all peano x indeed parenthesis peano x peano plus peano zero peano is peano zero peano plus peano x end parenthesis end line line ell c because rule prime mp modus ponens ell a modus ponens ell b indeed peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end parenthesis peano imply peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x end parenthesis end line line ell d because mendelson proposition three two h ii indeed peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end parenthesis end line line ell e because rule prime mp modus ponens ell c modus ponens ell d indeed peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x end parenthesis end line because rule prime gen modus ponens ell e indeed peano all peano x indeed peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x end parenthesis qed end math
end "
\\
We have thus proved "
begin math mendelson proposition three two h end math
end ", that is, \ref{eq:commu} stating the commutative law of addition. We
have done this using variables $x$ and $y$, but this does not make a
difference. Cf.~\ref{section:3.2f}.
%%%%%%%%%% 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
with 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 theory system prime s end theory 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 intended to
give a short 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}\label{section:Page}
This defines the name of the page:
\display{
"
begin math pyk define peano commutativity as "peano commutativity" 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 priority table 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 table end math end left
end "
%%%%%%%%%%%%%% Bibliography %%%%%%%%%%%%%%
\section{Bibliography}\label{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,