"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 metavar var t end metavar 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 define statement of mendelson lemma three two a as system prime s infer all metavar var t end metavar indeed metavar var t end metavar peano is metavar var t end metavar end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two a as text "mendelson lemma three two a" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two a as text "LEMMA 3.2(a)" end text 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 metavar var t end metavar end math
end " lig "
begin math metavar var r end metavar end math
end ", m\aa\ det n\o dvendigvis
ogs\aa\ g\ae lde at "
begin math metavar var r end metavar end math
end " lig "
begin math metavar var t end metavar end math
end ".
"
begin math define statement of mendelson lemma three two b as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two b as text "mendelson lemma three two b" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two b as text "LEMMA 3.2(b)" end text end define end math
end " }\\
\\
Tredje teorem viser at transitivitet for lighedsoperatoren.
"
begin math define statement of mendelson lemma three two c as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two c as text "mendelson lemma three two c" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two c as text "LEMMA 3.2(c)" end text 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 define statement of mendelson lemma three two d as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var r end metavar peano is metavar var t end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two d as text "mendelson lemma three two d" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two d as text "LEMMA 3.2(d)" end text 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 define statement of mendelson lemma three two f as system prime s infer var t peano var peano is peano zero peano plus var t peano var end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two f as text "mendelson lemma three two f" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two f as text "LEMMA 3.2(f)" end text 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 define statement of mendelson lemma three two g as system prime s infer var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two g as text "mendelson lemma three two g" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two g as text "LEMMA 3.2(g)" end text 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 define statement of mendelson lemma three two h as system prime s infer var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var end define end math
end "
\tex{ "
begin math define tex of mendelson lemma three two h as text "LEMMA 3.2(h)" end text end define end math
end " }
\footnote{"
begin math define pyk of mendelson lemma three two h as text "mendelson lemma three two h" end text 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 define statement of int mvar as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer metavar var b end metavar peano imply metavar var a end metavar end define end math
end "
\footnote{"
begin math define pyk of int mvar as text "int mvar" end text end define end math
end "}
\tex{ "
begin math define tex of int mvar as text "IMV" end text end define end math
end " }\\
\\
"
begin math define proof of int mvar as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer axiom prime a one conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar modus ponens metavar var a end metavar conclude metavar var b end metavar peano imply metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "
\subsection{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 define statement of commutative imply as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar infer metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end define end math
end "
\footnote{"
begin math define pyk of commutative imply as text "commutative imply" end text end define end math
end "}
\tex{ "
begin math define tex of commutative imply as text "CImp" end text end define end math
end " }\\
\\
"
begin math define proof of commutative imply as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar infer axiom prime a two conclude metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar modus ponens metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar conclude metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut int mvar modus ponens metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut axiom prime a two conclude metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar modus ponens metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut axiom prime a one conclude metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar modus ponens metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end quote state proof state cache var c end expand end define end math
end "
\subsection{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 metavar var a end metavar comma metavar var b end metavar comma metavar var c end metavar end math
end " (hhv. f\o rste, anden og tredje s\ae tning) :
"
begin math define statement of transitive imply as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar peano imply metavar var c end metavar end define end math
end "
\footnote{"
begin math define pyk of transitive imply as text "transitive imply" end text end define end math
end "}
\tex{ "
begin math define tex of transitive imply as text "TImp" end text end define end math
end " }
Nedenst\aa ende bevis er givet i l\o sningssiderne i Mendelson \cite{mendelson}.
"
begin math define proof of transitive imply as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var b end metavar peano imply metavar var c end metavar infer axiom prime a two conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut axiom prime a one conclude metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar conclude metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\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 define statement of mendelson lemma three two a as system prime s infer all metavar var t end metavar indeed metavar var t end metavar peano is metavar var t end metavar end define end math
end "
"
begin math define proof of mendelson lemma three two a as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed axiom prime s five conclude metavar var t end metavar peano plus peano zero peano is metavar var t end metavar cut axiom prime s one conclude metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var t end metavar cut rule prime mp modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var t end metavar modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar conclude metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var t end metavar cut rule prime mp modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var t end metavar modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar conclude metavar var t end metavar peano is metavar var t end metavar end quote state proof state cache var c end expand end define end math
end "
\subsection{Bevis for "
begin math mendelson lemma three two b end math
end "}
\label{lemma three two b}
"
begin math define statement of mendelson lemma three two b as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end define end math
end "
"
begin math define proof of mendelson lemma three two b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed axiom prime s one conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut commutative imply modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar conclude metavar var t end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut mendelson lemma three two a conclude metavar var t end metavar peano is metavar var t end metavar cut rule prime mp modus ponens metavar var t end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar modus ponens metavar var t end metavar peano is metavar var t end metavar conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end quote state proof state cache var c end expand end define end math
end "
\subsection{Bevis for "
begin math mendelson lemma three two c end math
end "}
\label{lemma three two c}
"
begin math define statement of mendelson lemma three two c as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end define end math
end "
"
begin math define proof of mendelson lemma three two c as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed axiom prime s one conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut mendelson lemma three two b conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut transitive imply modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar modus ponens metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define end math
end "
\subsection{Bevis for "
begin math mendelson lemma three two d end math
end "}
\label{lemma three two d}
"
begin math define statement of mendelson lemma three two d as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var r end metavar peano is metavar var t end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end define end math
end "
"
begin math define proof of mendelson lemma three two d as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed mendelson lemma three two c conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut commutative imply modus ponens metavar var r end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut mendelson lemma three two b conclude metavar var s end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut transitive imply modus ponens metavar var s end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar modus ponens metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut commutative imply modus ponens metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define end math
end "
\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 define statement of mendelson lemma three two f base as system prime s infer peano zero peano is peano zero peano plus peano zero end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two f base as text "mendelson lemma three two f base" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two f base as text "LEMMA 3.2(f) base" end text end define end math
end " }
"
begin math define proof of mendelson lemma three two f base as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude peano zero peano plus peano zero peano is peano zero cut mendelson lemma three two b conclude peano zero peano plus peano zero peano is peano zero peano imply peano zero peano is peano zero peano plus peano zero cut rule prime mp modus ponens peano zero peano plus peano zero peano is peano zero peano imply peano zero peano is peano zero peano plus peano zero modus ponens peano zero peano plus peano zero peano is peano zero conclude peano zero peano is peano zero peano plus peano zero end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis for induktionsskridt i "
begin math mendelson lemma three two f end math
end "}
"
begin math define statement of mendelson lemma three two f induction as system prime s infer var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two f induction as text "mendelson lemma three two f induction" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two f induction as text "LEMMA 3.2(f) induction" end text end define end math
end " }
"
begin math define proof of mendelson lemma three two f induction as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s six conclude peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut axiom prime s two conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut mendelson lemma three two d conclude var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut transitive imply modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ modus ponens var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut commutative imply modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut rule prime mp modus ponens peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ modus ponens peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ end quote state proof state cache var c end expand end define end math
end "
\newpage
\subsubsection{Samling af delbeviser}
"
begin math define statement of mendelson lemma three two f as system prime s infer var t peano var peano is peano zero peano plus var t peano var end define end math
end "
"
begin math define proof of mendelson lemma three two f as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s nine conclude peano zero peano is peano zero peano plus peano zero peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var cut mendelson lemma three two f base conclude peano zero peano is peano zero peano plus peano zero cut rule prime mp modus ponens peano zero peano is peano zero peano plus peano zero peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var modus ponens peano zero peano is peano zero peano plus peano zero conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var cut mendelson lemma three two f induction conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut rule prime gen modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut rule prime mp modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var cut axiom prime a four at var t peano var conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var cut rule prime mp modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var conclude var t peano var peano is peano zero peano plus var t peano var end quote state proof state cache var c end expand end define 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 define statement of mendelson lemma three two g base as system prime s infer var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two g base as text "mendelson lemma three two g base" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two g base as text "LEMMA 3.2(g) base" end text end define end math
end " }
"
begin math define proof of mendelson lemma three two g base as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var r peano var peano succ peano plus peano zero peano is var r peano var peano succ cut axiom prime s five conclude var r peano var peano plus peano zero peano is var r peano var cut axiom prime s two conclude var r peano var peano plus peano zero peano is var r peano var peano imply var r peano var peano plus peano zero peano succ peano is var r peano var peano succ cut rule prime mp modus ponens var r peano var peano plus peano zero peano is var r peano var peano imply var r peano var peano plus peano zero peano succ peano is var r peano var peano succ modus ponens var r peano var peano plus peano zero peano is var r peano var conclude var r peano var peano plus peano zero peano succ peano is var r peano var peano succ cut mendelson lemma three two d conclude var r peano var peano succ peano plus peano zero peano is var r peano var peano succ peano imply var r peano var peano plus peano zero peano succ peano is var r peano var peano succ peano imply var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ cut rule prime mp modus ponens var r peano var peano succ peano plus peano zero peano is var r peano var peano succ peano imply var r peano var peano plus peano zero peano succ peano is var r peano var peano succ peano imply var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ modus ponens var r peano var peano succ peano plus peano zero peano is var r peano var peano succ conclude var r peano var peano plus peano zero peano succ peano is var r peano var peano succ peano imply var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ cut rule prime mp modus ponens var r peano var peano plus peano zero peano succ peano is var r peano var peano succ peano imply var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ modus ponens var r peano var peano plus peano zero peano succ peano is var r peano var peano succ conclude var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ end quote state proof state cache var c end expand end define end math
end "
\newpage
\subsubsection{Bevis for induktionsskridt for "
begin math mendelson lemma three two g end math
end "}
"
begin math define statement of mendelson lemma three two g induction as system prime s infer var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two g induction as text "mendelson lemma three two g induction" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two g induction as text "LEMMA 3.2(g) induction" end text end define end math
end " }
"
begin math define proof of mendelson lemma three two g induction as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s six conclude var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano succ cut axiom prime s two conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut mendelson lemma three two c conclude var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut rule prime mp modus ponens var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ modus ponens var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano succ conclude var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut transitive imply modus ponens var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ modus ponens var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut mendelson lemma three two d conclude var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut transitive imply modus ponens var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ modus ponens var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut commutative imply modus ponens var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ conclude var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut axiom prime s six conclude var r peano var peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut axiom prime s two conclude var r peano var peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut rule prime mp modus ponens var r peano var peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ modus ponens var r peano var peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ conclude var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut rule prime mp modus ponens var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ modus ponens var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ end quote state proof state cache var c end expand end define end math
end "
\newpage
\subsubsection{Samling af delbeviser}
"
begin math define statement of mendelson lemma three two g as system prime s infer var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ end define end math
end "
"
begin math define proof of mendelson lemma three two g as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s nine conclude var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ peano imply peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ cut mendelson lemma three two g base conclude var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ cut rule prime mp modus ponens var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ peano imply peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ modus ponens var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ conclude peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ cut mendelson lemma three two g induction conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut rule prime gen modus ponens var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ conclude peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut rule prime mp modus ponens peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ modus ponens peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ conclude peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ cut axiom prime a four at var t peano var conclude peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ cut rule prime mp modus ponens peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ modus ponens peano all var t peano var indeed var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ end quote state proof state cache var c end expand end define end math
end "
\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 define statement of mendelson lemma three two h base as system prime s infer var t peano var peano plus peano zero peano is peano zero peano plus var t peano var end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two h base as text "mendelson lemma three two h base" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two h base as text "LEMMA 3.2(h) base" end text end define end math
end " }
"
begin math define proof of mendelson lemma three two h base as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var t peano var peano plus peano zero peano is var t peano var cut mendelson lemma three two f conclude var t peano var peano is peano zero peano plus var t peano var cut mendelson lemma three two c conclude var t peano var peano plus peano zero peano is var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano plus peano zero peano is peano zero peano plus var t peano var cut rule prime mp modus ponens var t peano var peano plus peano zero peano is var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano plus peano zero peano is peano zero peano plus var t peano var modus ponens var t peano var peano plus peano zero peano is var t peano var conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano plus peano zero peano is peano zero peano plus var t peano var cut rule prime mp modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano plus peano zero peano is peano zero peano plus var t peano var modus ponens var t peano var peano is peano zero peano plus var t peano var conclude var t peano var peano plus peano zero peano is peano zero peano plus var t peano var end quote state proof state cache var c end expand end define end math
end "
\newpage
\subsubsection{Bevis for induktionsskridt for "
begin math mendelson lemma three two h end math
end "}
"
begin math define statement of mendelson lemma three two h induction as system prime s infer var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var end define end math
end "
\footnote{"
begin math define pyk of mendelson lemma three two h induction as text "mendelson lemma three two h induction" end text end define end math
end "}
\tex{ "
begin math define tex of mendelson lemma three two h induction as text "LEMMA 3.2(h) induction" end text end define end math
end " }
"
begin math define proof of mendelson lemma three two h induction as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s six conclude var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ cut mendelson lemma three two g conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ cut axiom prime s two conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut mendelson lemma three two c conclude var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut rule prime mp modus ponens var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ modus ponens var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ conclude var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut transitive imply modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ modus ponens var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut mendelson lemma three two d conclude var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut transitive imply modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ modus ponens var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut commutative imply modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut rule prime mp modus ponens var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var modus ponens var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Samling af delbeviser}
"
begin math define proof of mendelson lemma three two h as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s nine conclude var t peano var peano plus peano zero peano is peano zero peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var cut mendelson lemma three two h base conclude var t peano var peano plus peano zero peano is peano zero peano plus var t peano var cut rule prime mp modus ponens var t peano var peano plus peano zero peano is peano zero peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var modus ponens var t peano var peano plus peano zero peano is peano zero peano plus var t peano var conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var cut mendelson lemma three two h induction conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut rule prime gen modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut rule prime mp modus ponens peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var modus ponens peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var cut axiom prime a four at var r peano var conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var cut rule prime mp modus ponens peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var modus ponens peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var end quote state proof state cache var c end expand end define end math
end "
\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 define pyk of rapport as text "rapport" end text end define end math
end "
"
begin math define pyk of blank space as text "blank space" end text end define end math
end "
\tex{ "
begin math define tex of blank space as text "" end text end define end math
end " }
\end{document}
End of file
latex page
latex page"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,