"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}
%\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}
\author{Anders B\o ggild-Povlsen (boggild@diku.dk) \& \\ Nicolai Esbensen(nies@diku.dk)}
\title{Kommutativitet for plusoperatoren}
\begin {document}
\maketitle
\tableofcontents
\newpage
%definitions
%end definitions
\section{Forord}
Denne rapport er bevistjekket og verificet korrekt, vha.
systemet \href{http://www.diku.dk/~grue/logiweb/20050502/logiweb/}{logiweb}.
Systemet muligg\o r verificering af dokumenter skrevet i sproget pyk, der
er en sammensmeltning mellem latex-kode og de konstruktioner der er defineret
i de inkluderede sider, og de konstruktioner der genkendes internt i pyk-overs\ae tteren.
Udover at verificere beviser publicerer logiweb siderne p\aa\ Internettet i div.
formater. Dette dokument er et s\aa ledes et produkt af et kompileret pyk-dokument.
Index-siden for dette dokument er at finde p\aa\ adressen:
\href{http://www.diku.dk/~grue/logiweb/20050502/home/nies/rapport/fixed/}
{http://www.diku.dk/~grue/logiweb/20050502/home/nies/rapport/fixed/}
De efterf\o lgende beviser bygger p\aa\ axiomer og inferensregler givet inden for
peanosystemet. Vi giver en kort historisk gennemgang af systemet i n\ae ste afsnit (\ref{peano axioms}).
M\aa let med projektet har v\ae ret at bevise kommutativitet for plus-operatoren (\ref{lemma three two h}),
vi kan i skrivende stund konkludere at det m\aa l er n\aa et.
\section{Peano-systemet}
\label{peano axioms}
I 1889 publicerede Peano en formalisering af de naturlige tal. Denne
formalisering bestod af 5 axiomer kendt som Peano's Postulater.
\begin{itemize}
\item[1] 0 er et naturligt tal\footnote{Oprindeligt 1 er et naturligt tal,
da 0 ikke blev betragtet som et naturligt tal}.
\item[2] Hvis $x$ er et naturligt tal, s\aa\ findes der et andet naturligt tal
$x'$ (efterf\o lgeren til x).
\item[3] $0 \neq x'$ for ethvert naturligt tal $x$.
\item[4] Hvis $x' = y'$ g\ae lder det at $x = y$
\item[5] Induktion: $Q$ er et udtryk der g\ae lder eller ikke g\ae lder. Hvis tallet $0$ har
$Q$'s egenskab og en given variabel $x$ og dens efterf\oe lger $x'$ har egenskaben, har alle
naturlige tal egenskaben. Alts\aa\ udtrykket g\ae lder for alle naturlige tal.
\end{itemize}
Form\aa let med vores rapport er at bevise kommutativitet for plusoperatoren
for de naturlige tal. Vi vil bevise dette ud fra en f\o rsteordens-teori ($S'$)\cite{peano} der
er en videreudvikling Peanos postulater. Denne teori har 9 axiomer ($S1' - S9'$) og har ikke \ae kvivalente
axiomer til alle Peano's Postulater. F.eks. er der ikke et axiom der siger at $0$
er et heltal, da dette fremg\aa r implicit axiomerne. De ekstra axiomer i $S'$
omfatter bl.a. en variation af transitivitet ($S1'$) og det omvendte af Peano's 4
postulat ($S2'$).
Derudover bygger $S'$ ogs\aa\ p\aa\ 5 axiomer ($A1' - A5'$) og 2 inferensregler ($MP,
Gen$)\footnote{hhv. Modus ponens og Generalisering} som g\ae lder for f\o rsteordens pr\ae dikat-kalkyler.
De enkelte regler og axiomer i den nye teori gennemg\aa s og opskrives i hhv. Mendelson \cite{mendelson}
og \href{http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/GRD-2005-06-22-UTC-07-23-31-271829/vector/page.lgw}{Peano-siden}.
\section{Introduktion}
\label{introduction}
I denne rapport vil vi som tidligere n\ae vnt fors\o ge at bevise
"
begin math mendelson lemma three two h end math
end ", ogs\aa\ kendt
som den kommutative lov. Til at hj\ae lpe os med dette har vi
axiomerne og inferensreglerne i systemet
\href{http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/GRD-2005-06-22-UTC-07-23-31-271829/vector/page.lgw}{"
begin math system prime s end math
end "},
stillet til r\aa dighed. I litteraturen {\cite{mendelson}}
foresl\aa es det at vi beviser visse teoremer vha.
axiomerne og inferensreglerne givet i "
begin math system prime s end math
end ",
og endelig bruge dem til at bevise "
begin math mendelson lemma three two h end math
end ".
I dette afsnit vil vi opskrive disse teoremer og kort beskrive deres betydning og brug.
Det kan t\ae nkes at vi undervejs kommer til at have brug for hj\ae lpes\ae tninger,
disse vil blive introduceret og bevist i afsnit (\ref{helpingsentences}).
Det f\o rste lemma beskriver egenskaben omkring et givent udtryk "
begin math meta t end math
end "
n\o dvendigvis
m\aa\ evalueres til at v\ae re lig den selv\footnote{Et krav for at et givent system er et system med lighed}.
Dette beskriver s\aa ledes den egenskab vi normalt forventer af
lighedsoperatoren\footnote{Skrives inden for det formulerede
peano-system "
begin math blank space peano is blank space end math
end " } i heltalsaritmetik.
Mere avancerede egenskaber ved lighedsopertoren bliver beskrevet i efterf\o lgende lemmaer.
"
begin math in theory system prime s lemma mendelson lemma three two a says all meta t indeed meta t peano is meta t end lemma end math
end "
\footnote{"
begin math pyk define mendelson lemma three two a as "mendelson lemma three two a" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two a as "LEMMA 3.2(a)" end define end math
end " }\\
\\
Andet teorem viser en anden egenskab for vores lighedsoperator; nemlig at det er kommutativt.
Er alle givne udtryk "
begin math meta t end math
end " lig "
begin math meta r end math
end ", m\aa\ det n\o dvendigvis
ogs\aa\ g\ae lde at "
begin math meta r end math
end " lig "
begin math meta t end math
end ".
"
begin math in theory system prime s lemma mendelson lemma 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 "
\footnote{"
begin math pyk define mendelson lemma three two b as "mendelson lemma three two b" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two b as "LEMMA 3.2(b)" end define end math
end " }\\
\\
Tredje teorem viser at transitivitet for lighedsoperatoren.
"
begin math in theory system prime s lemma mendelson lemma three two c says all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end lemma end math
end "
\footnote{"
begin math pyk define mendelson lemma three two c as "mendelson lemma three two c" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two c as "LEMMA 3.2(c)" end define end math
end " }\\
\\
Fjerde lemma beskriver samme egenskab som lemma tre, men udnytter samtidigt at lighedstegnet er kommutativt.
Dette lemma synes ikke umiddelbart at vise s\ae rligt sk\ae ls\ae ttende egenskaber, men kan vise sig s\ae rdeles
nyttig i forbindelse med brug af vores inferensregler.
"
begin math in theory system prime s lemma mendelson lemma three two d says all meta t indeed all meta r indeed all meta s indeed meta r peano is meta t peano imply meta s peano is meta t peano imply meta r peano is meta s end lemma end math
end "
\footnote{"
begin math pyk define mendelson lemma three two d as "mendelson lemma three two d" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two d as "LEMMA 3.2(d)" end define end math
end "}\\
\\
Femte lemma beskriver egenskaben ved heltallet 0, nemlig at addition med 0 ikke
\ae ndrer et udtryks v\ae rdi.
"
begin math in theory system prime s lemma mendelson lemma three two f says peano t peano is peano zero peano plus peano t end lemma end math
end "
\footnote{"
begin math pyk define mendelson lemma three two f as "mendelson lemma three two f" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two f as "LEMMA 3.2(f)" end define end math
end " }\\
\\
N\ae stsidste lemma viser en egenskab ved succesor-operatoren\footnote{Har den egenskab at der l\ae gges et til udtrykket
operatoren anvendes p\aa\ eksempelvis: $41' = 42$}. Egenskaben der
vises er at successor-operatoren er distributiv ved addition. Intuitivt giver dette god mening da plus-operatoren
er kommutativ\footnote{Bem\ae rk at dette ikke er bevist endnu}, og r\ae kkef\o lgen for evaluering derfor er ligegyldig.
"
begin math in theory system prime s lemma mendelson lemma three two g says peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end lemma end math
end "
\footnote{"
begin math pyk define mendelson lemma three two g as "mendelson lemma three two g" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two g as "LEMMA 3.2(g)" end define end math
end " }\\
\\
Vores endelig lemma, kronen p\aa\ v\ae rket, viser at plus-operatoren er kommutativ, alts\aa\ at resultatet er uafh\ae ngigt af
hvilken side operanderne st\aa r p\aa .
"
begin math in theory system prime s lemma mendelson lemma three two h says peano t peano plus peano r peano is peano r peano plus peano t end lemma end math
end "
\tex{ "
begin math tex define mendelson lemma three two h as "LEMMA 3.2(h)" end define end math
end " }
\footnote{"
begin math pyk define mendelson lemma three two h as "mendelson lemma three two h" end define end math
end "}
\section{Hj\ae lpes\ae tninger}
\label{helpingsentences}
I dette afsnit defineres og bevises de benyttede hj\ae lpes\ae tninger, der ligger ud over de
allerede definerede s\ae tninger i afsnit \ref{introduction}.
\subsection{Introduktion af metavariabel}
I l\o bet af projektet opstod der et behov for at introducere en ny metavariabel til at
medf\o re et andet givent udtryk. Dette vil g\ae lde uafh\ae ngigt af den introducerede variabels
sandhedsv\ae rdi, da det er en foruds\ae tning at den oprindelige s\ae tning g\ae lder
footnote{Se evt. sandhedstabellen for medf\o rer i \cite{mendelson} afsnit 1.1.}
Herunder f\o lger definitionen og beviset for lemmaet.
"
begin math in theory system prime s lemma int mvar says all meta a indeed all meta b indeed meta a infer meta b peano imply meta a end lemma end math
end "
\footnote{"
begin math pyk define int mvar as "int mvar" end define end math
end "}
\tex{ "
begin math tex define int mvar as "IMV" end define end math
end " }\\
\\
"
begin math system prime s proof of int mvar reads arbitrary meta a end line arbitrary meta b end line line ell a premise meta a end line line ell b because axiom prime a one indeed meta a peano imply meta b peano imply meta a end line because rule prime mp modus ponens ell b modus ponens ell a indeed meta b peano imply meta a qed end math
end "
\subsection{Kommutativitet ved medf\o rer}
Det viser sig at medf\o reroperatoren er associativ i f\o rste led for tre eller flere metavariable,
s\aa fremt hele det oprindelige udtryk evaluerer til sand. Dette er netop hvad nedenst\aa ende udtryk
siger. Dette faktum vil ogs\aa\ kunne vises ved tautologi at de to udtryk er logisk \ae kvivalente, denne
mulighed har dog ikke som bevisform, og vil derfor bevise p\aa standen vha. de givne axiomer og inferensregler.
"
begin math in theory system prime s lemma commutative imply says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta c peano imply meta b infer meta c peano imply meta a peano imply meta b end lemma end math
end "
\footnote{"
begin math pyk define commutative imply as "commutative imply" end define end math
end "}
\tex{ "
begin math tex define commutative imply as "CImp" end define end math
end " }\\
\\
"
begin math system prime s proof of commutative imply reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta c peano imply meta b end line line ell b because axiom prime a two indeed parenthesis meta a peano imply meta c peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b 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 c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis end line line ell d because int mvar modus ponens ell c indeed meta c peano imply parenthesis meta a peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis end line line ell e because axiom prime a two indeed parenthesis meta c peano imply parenthesis meta a peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis end parenthesis peano imply parenthesis meta c peano imply meta a peano imply meta c end parenthesis peano imply parenthesis meta c peano imply meta a peano imply meta b end parenthesis end line line ell f because rule prime mp modus ponens ell e modus ponens ell d indeed parenthesis meta c peano imply meta a peano imply meta c end parenthesis peano imply parenthesis meta c peano imply meta a peano imply meta b end parenthesis end line line ell g because axiom prime a one indeed meta c peano imply meta a peano imply meta c end line because rule prime mp modus ponens ell f modus ponens ell g indeed meta c peano imply meta a peano imply meta b qed end math
end "
\subsection{Transitivitet for medf\o rer}
Det er ofte en fordel at kunne vise at hvis et givent udtryk medf\o rer et andet, hvor dette
endvidere medf\o rer et tredje, m\aa\ der som konsekvens heraf g\ae lde at det f\o rste medf\o rer
det tredje. Dette er umiddelbart nemmere at opskrive end forklare, herunder
"
begin math meta a comma meta b comma meta c end math
end " (hhv. f\o rste, anden og tredje s\ae tning) :
"
begin math in theory system prime s lemma transitive imply says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b infer meta b peano imply meta c infer meta a peano imply meta c end lemma end math
end "
\footnote{"
begin math pyk define transitive imply as "transitive imply" end define end math
end "}
\tex{ "
begin math tex define transitive imply as "TImp" end define end math
end " }
Nedenst\aa ende bevis er givet i l\o sningssiderne i Mendelson \cite{mendelson}.
"
begin math system prime s proof of transitive imply reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell b premise meta a peano imply meta b end line line ell a premise meta b peano imply meta c end line line ell c because axiom prime a two 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 parenthesis meta a peano imply meta c end parenthesis end line line ell d because axiom prime a one indeed parenthesis meta b peano imply meta c end parenthesis peano imply meta a peano imply parenthesis meta b peano imply meta c end parenthesis end line line ell e because rule prime mp modus ponens ell d modus ponens ell a indeed meta a peano imply meta b peano imply meta c end line line ell f because rule prime mp modus ponens ell c modus ponens ell e indeed parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end line because rule prime mp modus ponens ell f modus ponens ell b indeed meta a peano imply meta c qed end math
end "
\newpage
\section{Bevis af lemmaer}
\label{proofs}
I dette afsnit beviser vi de beskrevne lemmaer i afsnit \ref{introduction}. Vi vil for
hvert bevis genopskrive det lemma der \o nskes bevist s\aa\ arbejdet mod konklusionen er klarere i sammenh\ae ngen.\\
\\
Beviserne bygger i st\o rre eller mindre grad p\aa\ de gennemg\aa ede beviser i Mendelson. Mange steder benyttes
tautologier samt deduktions teoremet, disse ting kan ikke direkte benyttes indenfor logiwebsystemet, hvorfor
vi beviser os ud af de enkelte linjer vha. de givne axiomer og inferensregler givet i
\href{http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/GRD-2005-06-22-UTC-07-23-31-271829/vector/page.lgw}{peano-systemet}. Det har
ogs\aa\ v\ae ret n\o dvedigt at ekspandere forskellige linjer og intruducere hj\ae lpes\ae tninger (\ref{helpingsentences})
enkelte steder.
\subsection{Bevis for "
begin math mendelson lemma three two a end math
end "}
\label{lemma three two a}
"
begin math in theory system prime s lemma mendelson lemma three two a says all meta t indeed meta t peano is meta t end lemma end math
end "
"
begin math system prime s proof of mendelson lemma 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 meta t peano plus peano zero peano is meta t peano imply meta t peano plus peano zero peano is meta t peano imply meta t peano is meta t 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 "
\subsection{Bevis for "
begin math mendelson lemma three two b end math
end "}
\label{lemma three two b}
"
begin math in theory system prime s lemma mendelson lemma three two b says all meta t indeed all meta r indeed meta t peano is meta r peano imply meta r peano is meta t end lemma end math
end "
"
begin math system prime s proof of mendelson lemma 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 meta t peano is meta t peano imply meta r peano is meta t end line line ell b because commutative imply modus ponens ell a indeed meta t peano is meta t peano imply meta t peano is meta r peano imply meta r peano is meta t end line line ell c because mendelson lemma 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 "
\subsection{Bevis for "
begin math mendelson lemma three two c end math
end "}
\label{lemma three two c}
"
begin math in theory system prime s lemma mendelson lemma three two c says all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end lemma end math
end "
"
begin math system prime s proof of mendelson lemma 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 meta r peano is meta s peano imply meta t peano is meta s end line line ell b because mendelson lemma three two b indeed meta t peano is meta r peano imply meta r peano is meta t end line because transitive imply modus ponens ell b modus ponens ell a indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s qed end math
end "
\subsection{Bevis for "
begin math mendelson lemma three two d end math
end "}
\label{lemma three two d}
"
begin math in theory system prime s lemma mendelson lemma three two d says all meta t indeed all meta r indeed all meta s indeed meta r peano is meta t peano imply meta s peano is meta t peano imply meta r peano is meta s end lemma end math
end "
"
begin math system prime s proof of mendelson lemma three two d reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a because mendelson lemma three two c indeed meta r peano is meta t peano imply meta t peano is meta s peano imply meta r peano is meta s end line line ell b because commutative imply modus ponens ell a indeed meta t peano is meta s peano imply meta r peano is meta t peano imply meta r peano is meta s end line line ell c because mendelson lemma three two b indeed meta s peano is meta t peano imply meta t peano is meta s end line line ell d because transitive imply modus ponens ell c modus ponens ell b indeed meta s peano is meta t peano imply meta r peano is meta t peano imply meta r peano is meta s end line because commutative imply modus ponens ell d indeed meta r peano is meta t peano imply meta s peano is meta t peano imply meta r peano is meta s qed end math
end "
\newpage
\subsection{Kort omkring induktionsbeviserne}
I de efterf\o lgende beviser benyttes induktion, for at bevise de enkelte lemmaer.
Vi g\o r dette ved seperat at bevise nultilf\ae ldet\footnote{De enkelte
delbeviser introduceres i de enkelte underafsnit} og induktionskridtet, for til sidst
at inducere over de to udtryk og herved n\aa\ vores konklusion. Dette er s\aa ledes samme
strategi der benyttes i Mendelson \cite{mendelson}. Bem\ae rk at vi i benytter peanovariable,
der udelukkende beskriver heltal, i mods\ae tning til de tidligere beviser, hvor vi
gennemf\o rte beviserne for arbitr\ae re udtryk. Dette er en n\o dvendighed, for at kunne
benytte peano-induktionsreglen ("
begin math axiom prime s nine end math
end ").
\subsection{Bevis for "
begin math mendelson lemma three two f end math
end "}
\label{lemma three two f}
\subsubsection{Bevis for basistilf\ae lde i "
begin math mendelson lemma three two f end math
end "}
"
begin math in theory system prime s lemma mendelson lemma three two f base says peano zero peano is peano zero peano plus peano zero end lemma end math
end "
\footnote{"
begin math pyk define mendelson lemma three two f base as "mendelson lemma three two f base" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two f base as "LEMMA 3.2(f) base" end define end math
end " }
"
begin math system prime s proof of mendelson lemma three two f base reads line ell a because axiom prime s five indeed peano zero peano plus peano zero peano is peano zero end line line ell b because mendelson lemma three two b indeed peano zero peano plus peano zero peano is peano zero peano imply peano zero peano is peano zero peano plus peano zero end line because rule prime mp modus ponens ell b modus ponens ell a indeed peano zero peano is peano zero peano plus peano zero qed end math
end "
\subsubsection{Bevis for induktionsskridt i "
begin math mendelson lemma three two f end math
end "}
"
begin math in theory system prime s lemma mendelson lemma three two f induction says peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end lemma end math
end "
\footnote{"
begin math pyk define mendelson lemma three two f induction as "mendelson lemma three two f induction" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two f induction as "LEMMA 3.2(f) induction" end define end math
end " }
"
begin math system prime s proof of mendelson lemma three two f induction reads line ell a because axiom prime s six indeed peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell b because axiom prime s two indeed peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell c because mendelson lemma three two d indeed peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end line line ell d because transitive imply modus ponens ell b modus ponens ell c indeed peano t peano is peano zero peano plus peano t peano imply peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end line line ell e because commutative imply modus ponens ell d indeed peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end line because rule prime mp modus ponens ell e modus ponens ell a indeed peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ qed end math
end "
\newpage
\subsubsection{Samling af delbeviser}
"
begin math in theory system prime s lemma mendelson lemma three two f says peano t peano is peano zero peano plus peano t end lemma end math
end "
"
begin math system prime s proof of mendelson lemma three two f reads line ell a because axiom prime s nine indeed peano zero peano is peano zero peano plus peano zero peano imply peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis peano imply peano all peano t indeed peano t peano is peano zero peano plus peano t end line line ell q because mendelson lemma three two f base indeed peano zero peano is peano zero peano plus peano zero end line line ell b because rule prime mp modus ponens ell a modus ponens ell q indeed peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis peano imply peano all peano t indeed peano t peano is peano zero peano plus peano t end line line ell r because mendelson lemma three two f induction indeed peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end line line ell c because rule prime gen modus ponens ell r indeed peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end line line ell d because rule prime mp modus ponens ell b modus ponens ell c indeed peano all peano t indeed peano t peano is peano zero peano plus peano t end line line ell e because axiom prime a four at peano t indeed peano all peano t indeed peano t peano is peano zero peano plus peano t peano imply peano t peano is peano zero peano plus peano t end line because rule prime mp modus ponens ell e modus ponens ell d indeed peano t peano is peano zero peano plus peano t qed end math
end "
\subsection{Bevis for "
begin math mendelson lemma three two g end math
end "}
Bem\ae rk at vi i dette afsnit har v\ae ret n\o dt til at ombytte variabelnavnene, i forhold til
i Mendelson \cite{mendelson}. Dette skyldes at vi fik en fejl, n\aa r vi instatierede lemmaet
i "
begin math mendelson lemma three two h end math
end ", denne ombytning har dog ingen indflydelse
p\aa\ den egenskab lemmaet beskriver.
\subsubsection{Bevis for basistilf\ae lde for "
begin math mendelson lemma three two g end math
end "}
"
begin math in theory system prime s lemma mendelson lemma three two g base says peano r peano succ peano plus peano zero peano is parenthesis peano r peano plus peano zero end parenthesis peano succ end lemma end math
end "
\footnote{"
begin math pyk define mendelson lemma three two g base as "mendelson lemma three two g base" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two g base as "LEMMA 3.2(g) base" end define end math
end " }
"
begin math system prime s proof of mendelson lemma three two g base reads line ell a because axiom prime s five indeed peano r peano succ peano plus peano zero peano is peano r peano succ end line line ell b because axiom prime s five indeed peano r peano plus peano zero peano is peano r end line line ell c because axiom prime s two indeed peano r peano plus peano zero peano is peano r peano imply parenthesis peano r peano plus peano zero end parenthesis peano succ peano is peano r peano succ end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed parenthesis peano r peano plus peano zero end parenthesis peano succ peano is peano r peano succ end line line ell e because mendelson lemma three two d indeed peano r peano succ peano plus peano zero peano is peano r peano succ peano imply parenthesis peano r peano plus peano zero end parenthesis peano succ peano is peano r peano succ peano imply peano r peano succ peano plus peano zero peano is parenthesis peano r 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 r peano plus peano zero end parenthesis peano succ peano is peano r peano succ peano imply peano r peano succ peano plus peano zero peano is parenthesis peano r peano plus peano zero end parenthesis peano succ end line because rule prime mp modus ponens ell f modus ponens ell d indeed peano r peano succ peano plus peano zero peano is parenthesis peano r peano plus peano zero end parenthesis peano succ qed end math
end "
\newpage
\subsubsection{Bevis for induktionsskridt for "
begin math mendelson lemma three two g end math
end "}
"
begin math in theory system prime s lemma mendelson lemma three two g induction says peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end lemma end math
end "
\footnote{"
begin math pyk define mendelson lemma three two g induction as "mendelson lemma three two g induction" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two g induction as "LEMMA 3.2(g) induction" end define end math
end " }
"
begin math system prime s proof of mendelson lemma three two g induction reads line ell a because axiom prime s six indeed peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano succ peano plus peano t end parenthesis peano succ end line line ell b because axiom prime s two indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply parenthesis peano r peano succ peano plus peano t end parenthesis peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ end line line ell c because mendelson lemma three two c indeed peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano succ peano plus peano t end parenthesis peano succ peano imply parenthesis peano r peano succ peano plus peano t end parenthesis peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ end line line ell d because rule prime mp modus ponens ell c modus ponens ell a indeed parenthesis peano r peano succ peano plus peano t end parenthesis peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ end line line ell e because transitive imply modus ponens ell b modus ponens ell d indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ end line line ell f because mendelson lemma three two d indeed peano r peano succ peano plus peano t peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ peano imply parenthesis peano r peano plus peano t peano succ end parenthesis peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end line line ell g because transitive imply modus ponens ell e modus ponens ell f indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply parenthesis peano r peano plus peano t peano succ end parenthesis peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end line line ell h because commutative imply modus ponens ell g indeed parenthesis peano r peano plus peano t peano succ end parenthesis peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end line line ell i because axiom prime s six indeed peano r peano plus peano t peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell j because axiom prime s two indeed peano r peano plus peano t peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply parenthesis peano r peano plus peano t peano succ end parenthesis peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ end line line ell k because rule prime mp modus ponens ell j modus ponens ell i indeed parenthesis peano r peano plus peano t peano succ end parenthesis peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ end line because rule prime mp modus ponens ell h modus ponens ell k indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ qed end math
end "
\newpage
\subsubsection{Samling af delbeviser}
"
begin math in theory system prime s lemma mendelson lemma three two g says peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end lemma end math
end "
"
begin math system prime s proof of mendelson lemma three two g reads line ell a because axiom prime s nine indeed peano r peano succ peano plus peano zero peano is parenthesis peano r peano plus peano zero end parenthesis peano succ peano imply peano all peano t indeed parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end parenthesis peano imply peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell b because mendelson lemma three two g base indeed peano r peano succ peano plus peano zero peano is parenthesis peano r peano plus peano zero end parenthesis peano succ end line line ell c because rule prime mp modus ponens ell a modus ponens ell b indeed peano all peano t indeed parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end parenthesis peano imply peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell d because mendelson lemma three two g induction indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end line line ell e because rule prime gen modus ponens ell d indeed peano all peano t indeed parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end parenthesis end line line ell f because rule prime mp modus ponens ell c modus ponens ell e indeed peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell g because axiom prime a four at peano t indeed peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line because rule prime mp modus ponens ell g modus ponens ell f indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ qed end math
end "
\subsection{Bevis for "
begin math mendelson lemma three two h end math
end "}
\label{lemma three two h}
\subsubsection{Bevis for basistilf\ae lde for "
begin math mendelson lemma three two h end math
end "}
"
begin math in theory system prime s lemma mendelson lemma three two h base says peano t peano plus peano zero peano is peano zero peano plus peano t end lemma end math
end "
\footnote{"
begin math pyk define mendelson lemma three two h base as "mendelson lemma three two h base" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two h base as "LEMMA 3.2(h) base" end define end math
end " }
"
begin math system prime s proof of mendelson lemma three two h base reads line ell a because axiom prime s five indeed peano t peano plus peano zero peano is peano t end line line ell b because mendelson lemma three two f indeed peano t peano is peano zero peano plus peano t end line line ell c because mendelson lemma three two c indeed peano t peano plus peano zero peano is peano t peano imply peano t peano is peano zero peano plus peano t peano imply peano t peano plus peano zero peano is peano zero peano plus peano t end line line ell d because rule prime mp modus ponens ell c modus ponens ell a indeed peano t peano is peano zero peano plus peano t peano imply peano t peano plus peano zero peano is peano zero peano plus peano t end line because rule prime mp modus ponens ell d modus ponens ell b indeed peano t peano plus peano zero peano is peano zero peano plus peano t qed end math
end "
\newpage
\subsubsection{Bevis for induktionsskridt for "
begin math mendelson lemma three two h end math
end "}
"
begin math in theory system prime s lemma mendelson lemma three two h induction says peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end lemma end math
end "
\footnote{"
begin math pyk define mendelson lemma three two h induction as "mendelson lemma three two h induction" end define end math
end "}
\tex{ "
begin math tex define mendelson lemma three two h induction as "LEMMA 3.2(h) induction" end define end math
end " }
"
begin math system prime s proof of mendelson lemma three two h induction reads line ell a because axiom prime s six indeed peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell b because mendelson lemma three two g indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell c because axiom prime s two indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell d because mendelson lemma three two c indeed peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell e because rule prime mp modus ponens ell d modus ponens ell a indeed parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell f because transitive imply modus ponens ell c modus ponens ell e indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell g because mendelson lemma three two d indeed peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end line line ell h because transitive imply modus ponens ell f modus ponens ell g indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end line line ell i because commutative imply modus ponens ell h indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end line because rule prime mp modus ponens ell i modus ponens ell b indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t qed end math
end "
\subsubsection{Samling af delbeviser}
"
begin math system prime s proof of mendelson lemma three two h reads line ell a because axiom prime s nine indeed peano t peano plus peano zero peano is peano zero peano plus peano t peano imply peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis peano imply peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end line line ell b because mendelson lemma three two h base indeed peano t peano plus peano zero peano is peano zero peano plus peano t end line line ell c because rule prime mp modus ponens ell a modus ponens ell b indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis peano imply peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end line line ell d because mendelson lemma three two h induction indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end line line ell e because rule prime gen modus ponens ell d indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis end line line ell f because rule prime mp modus ponens ell c modus ponens ell e indeed peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end line line ell g because axiom prime a four at peano r indeed peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano is peano r peano plus peano t end line because rule prime mp modus ponens ell g modus ponens ell f indeed peano t peano plus peano r peano is peano r peano plus peano t qed end math
end "
\section{Litteratur}
\begin{thebibliography}{99}
\bibitem{peano} K. Grue. Peano Axioms. \\
\href{http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/GRD-2005-06-22-UTC-07-23-31-271829/vector/page.lgw}
{http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/GRD-2005-06-22-UTC-07-23-31-271829/vector/page.lgw}
\bibitem{Base} K. Grue. Base Page.\\
\href{http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/GRD-2005-06-22-UTC-06-58-05-413682/vector/page.lgw}
{http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/GRD-2005-06-22-UTC-06-58-05-413682/vector/page.lgw}
\bibitem{mendelson} Elliott Mendelson. Introduction to Mathematical Logic - CRC press 2001.
\end{thebibliography}
\newpage
\section{\TeX\ definitioner}
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\immediate\closeout\outex
\input{./page.otx}
\end{list}
\section{Sidens navn}
"
begin math pyk define rapport as "rapport" end define end math
end "
"
begin math pyk define blank space as "blank space" end define end math
end "
\tex{ "
begin math tex define blank space as "" end define end math
end " }
\end{document}
End of file
latex page
latex page"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,