"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,titlepage]{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}
\usepackage{lscape}
\usepackage{multicol}
\usepackage{float}
\usepackage[latin1]{inputenc}
\usepackage[dvips]{graphicx}
\usepackage{verbatim}
\usepackage[danish]{babel}
\usepackage{graphpap}
\newcommand{\baseurl}{www.diku.dk/~grue/logiweb/20050502/home/grue/base/GRD-2005-06-03-UTC-15-49-33-495567}
\newcommand{\peanourl}{www.diku.dk/~grue/logiweb/20050502/home/grue/peano-axioms/GRD-2005-06-03-UTC-15-58-02-061312}
\begin{document}
\title{ \Huge{Et bevis i Peano aritmetik}}
\author{Frederik Eriksen \texttt{(eriksen@diku.dk)} }
\date{29.\ juni 2005}
\floatplacement{figure}{h!}
\floatplacement{table}{h!}
\bibliographystyle{plain}
\hyphenation{Plus-Commutativity si-de-be-ting-el-se}
\maketitle
\newpage
\tableofcontents
\listoffigures
\listoftables
\newpage
\section{Indledning}
Her er en matematisk s\ae{}tning: Ligheden
%
%\begin{center}
\begin{eqnarray}
\mathit{n} + \mathit{m} & = & \mathit{m} + \mathit{n} \label{eq:com}
\end{eqnarray}
%\end{center}
%
g\ae{}lder for alle naturlige tal $\mathit{n}$ og $\mathit{m}$. (Ved et ``naturligt tal'' forst\aa{}r jeg et ikke-negativt heltal).
Denne rapport indeholder et formelt bevis for s\ae{}tning (\ref{eq:com}). Beviset gennemf\o{}res inden for rammerne af et formelt system kaldet ``Peano aritmetik''. Rapporten er udarbejdet ved hj\ae{}lp af Logiweb, som er et system til verifikation og publikation af tekster, der indeholder formel matematik.
Logiweb har vericeret, at rapportens bevis for s\ae{}tning (\ref{eq:com}) er korrekt --- s\aa{} jeg kan tillade mig at p\aa{}st\aa{}, at rapporten ikke indeholder nogen formelle fejl. Jeg har ogs\aa{} brugt Logiweb til at publicere rapporten p\aa{} internettet; adressen er:
\noindent
\resizebox{\textwidth}{!}{\url{http://www.diku.dk/~grue/logiweb/20050502/home/eriksen/peano-commutativity}.}
Rapportens bevis for (\ref{eq:com}) findes allerede i litteraturen --- se \cite{kn:mendel}, s\ae{}tning 3.2(h). Det er alts\aa{} mere rimeligt at betragte rapporten som en formel \o{}velse i at bruge Logiweb, end som et selvst\ae{}ndigt stykke matematisk arbejde; men formelle \o{}velser har jo ogs\aa{} deres berettigelse.
Rapporten er struktueret som f\o{}lger: Afsnit \ref{sec:logiweb} handler om Logiweb. Det er ikke en detaljeret beskrivelse af systemet, men giver forh\aa{}bentlig oplysninger nok til, at man kan forst\aa{} rapportens formelle indhold uden yderligere viden om Logiweb.
Afsnit \ref{sec:peano} beskriver syntaksen for Peano aritmetik samt det aksiomsystem, der bliver brugt i rapporten.
Afsnit \ref{sec:hjaelpesaetninger} pr\ae{}senterer de 28 hj\ae{}lpes\ae{}tninger, som jeg vil bruge til at bevise ligning (\ref{eq:com}). For overskuelighedens skyld har jeg inddelt hj\ae{}lpes\ae{}tningerne i 3 undergrupper: Lemmaer, afledte lemmaer og makroer. Makroerne bliver bevist i afsnit \ref{sec:bevismakroer}; og de resterende hj\ae{}lpes\ae{}tninger bliver bevist i afsnit \ref{sec:bevislemmaer}.
\section{Lidt om Logiweb} \label{sec:logiweb}
Som n\ae{}vnt i indledningen er denne rapport skrevet ved hj\ae{}lp af Logiweb. Dette betyder dels,
at rapportens formelle indhold er defineret ud fra nogle andre Logiweb-dokumenter,
og dels at rapporten har nogle stilistiske s\ae{}rtr\ae{}k. Disse to facetter ved Logiweb vil jeg kort forklare i afsnit \ref{sec:formelkon} og \ref{sec:saerlig}. For en detaljeret beskrivelse af hele Logiweb systemet vil jeg henvise til \cite{kn:base}; her kan man bla.\ l\ae{}se om den bevischecker, der har verificeret rapportens beviser.
\subsection{Formelle konstruktioner} \label{sec:formelkon}
Det formelle indhold af et Logiweb-dokument er sammensat af en r\ae{}kke formelle konstruktioner. En formel konstruktion kan repr\ae{}sentere alt, hvad der har med formel matematik at g\o{}re: Variable, funktioner, lemmaer, beviser, osv. Der er to kilder til konstruktionerne i et Logiweb-dokument: Dels kan man indf\o{}re sine egne konstruktioner, og dels kan man importere konstruktioner fra andre Logiiweb-dokumenter. I denne rapport er alle konstruktioner importerede fra de to Logiweb-dokumenter \cite{kn:base} og \cite{kn:peano} --- med undtagelse af de konstruktioner, der repr\ae{}senterer rapportens 28 hj\ae{}lpes\ae{}tninger; dem definerer jeg selv.
%de lemmaer, som bliver bevist i rapporten; dem definerer jeg selv.
\subsection{S\ae{}rlige definitioner} \label{sec:saerlig}
Den formelle del af et Logiweb-dokument skrives i et formateringssprog ved navn ``pyk''. Hver formel konstruktion, man arbejder med i dokumentet, har tilknyttet en s\aa{}kaldt ``pyk definition''. Dette er en angivelse af, hvad man skal skrive, hvis man i et andet Logiweb-dokument \o{}nsker at benytte den p\aa{}g\ae{}ldende konstruktion. Hvis man indf\o{}rer en ny konstruktion i sit Logiweb-dokument, er det et krav, at man g\o{}r den tilsvarende pyk definition tilg\ae{}ngelig i dokumentet. Dette krav vil jeg im\o{}dekomme ved at n\ae{}vne pyk definitionen i en fodnote, hver gang jeg pr\ae{}senterer en ny hj\ae{}lpes\ae{}tning.
Logiweb genererer det f\ae{}rdige dokument ved hj\ae{}lp af det kendte formateringssprog \LaTeX. Derfor har hver formel konstruktion ogs\aa{} tilknyttet en s\aa{}kaldt ``\TeX{} definition'', som angiver, hvordan konstruktionen skal skrives i \LaTeX. Ligesom pyk definitioner skal ogs\aa{} \TeX{} definitioner v\ae{}re tilg\ae{}ngelige i dokumentet. \TeX{} definitionerne for denne rapports lemmaer er vedlagt i bilag \ref{sec:texdefinitioner}.
Endelig skal det n\ae{}vnes, at Logiweb opfatter selve navnet p\aa{} et Logiweb-dokument som en formel konstruktion. Derfor skal ethvert Logiweb-dokument indeholde mindst \'{e}n pyk definition --- nemlig pyk definitionen af dokumentets eget navn. Denne definition har jeg vedlagt i bilag \ref{sec:navn}.
\section{Peano aritmetik} \label{sec:peano}
Peano aritmetik er et formelt sprog, der bruges til at repr\ae{}sentere de naturlige tal. Jeg vil bruge n\o{}jagtig den samme version af Peano aritmetik som d\'{e}n, der pr\ae{}senteres i \cite{kn:peano}. Dette g\ae{}lder b\aa{}de mht.\ syntaksen (som jeg gennemg\aa{}r i \mbox{afsnit \ref{sec:syntaks}}), og mht.\ det anvendte aksiomsystem (som jeg gennemg\aa{}r i \mbox{afsnit \ref{sec:aksiomer}}).
\subsection{Syntaks} \label{sec:syntaks}
Peano aritmetik er opbygget af termer og formler; jeg gennemg\aa{}r hver af disse begreber i de f\o{}lgende to underafsnit.
\subsubsection{Termer} \label{sec:termer}
Syntaksen for en term "
begin math meta t end math
end " kan beskrives ved den f\o{}lgende BNF-grammatik:
%
\begin{eqnarray}
{\cal T} & ::= & \dot{0} \; | \; {{\cal T}}' \; | \; {\cal T} \mathop{\dot{+}} {\cal T} \; | \;
{\cal T} \mathop{\dot{\cdot}} {\cal T} \; | \; \texttt{Pvar} \label{eq:term}
\end{eqnarray}
%
Efterf\o{}lgeren $\mathit{m}$ til et naturligt tal $\mathit{n}$ er det mindste naturlige tal, der er st\o{}rre end $\mathit{n}$. Efterf\o{}lgeroperatoren er den funktion, der f\o{}rer $\mathit{n}$ over i $\mathit{m}$. Ideen med den syntaktiske konstruktion ${}'$ er, at den skal repr\ae{}sentere efterf\o{}lgeroperatoren. P\aa{} denne m\aa{}de kan vi repr\ae{}sentere alle naturlige tal med de to konstruktioner "
begin math peano zero end math
end " og ${}'$ --- $1$ kan repr\ae{}senteres som "
begin math peano zero peano succ end math
end ", $2$ som "
begin math parenthesis peano zero peano succ end parenthesis peano succ end math
end ",
%
\footnote{Egentlig b\o{}r "
begin math parenthesis peano zero peano succ end parenthesis peano succ end math
end " skrives $\dot{0}''$. Imidlertid er der en lille fejl ved \TeX{} definitionen af konstruktionen ${}'$ i \cite{kn:peano}. Fejlen betyder, at \LaTeX{} ikke accepterer to anvendelser af ${}'$ i tr\ae{}k --- derfor den ekstra parentes.}
%
osv.
Ideen med konstruktionerne $\mathop{\dot{+}}$ og $\mathop{\dot{\cdot}}$ er, at de skal repr\ae{}sentere regningsarterne addition og multiplikation. Da denne rapport kun omhandler addition, kommer vi ikke til at se mere til tegnet $\mathop{\dot{\cdot}}$.
Den sidste konstruktion i (\ref{eq:term}) er \texttt{Pvar}, som er en forkortelse for ``Peano variabel'' . En Peano variabel er en variabel, der varierer over konstante termer (hvor en konstant term er en term, der ikke indeholder Peano variable). Artiklen \cite{kn:peano} bruger sm\aa{} bogstaver med en prik over til at ben\ae{}vne Peano variable --- alts\aa{} f.eks.\ "
begin math peano a end math
end " og "
begin math peano b end math
end ". Jeg vil g\o{}re det samme, idet jeg dog kun vil bruge bogstaverne "
begin math peano t end math
end ", "
begin math peano r end math
end " og "
begin math peano s end math
end ".
\subsubsection{Formler}
Syntaksen for en formel "
begin math meta f end math
end " kan beskrives ved den f\o{}lgende BNF-grammatik:
%
\begin{eqnarray*}
{\cal F} & ::= & {\cal T} \stackrel{p}{=} {\cal T} \; | \; \dot{\neg}{\cal F} \; | \; {\cal F} \mathrel{\dot{\Rightarrow}} {\cal F} \; | \;
\dot{\forall}\texttt{Pvar}:{\cal F} %\label{eq:formel}
\end{eqnarray*}
%
Med en formel kan vi alts\aa{} p\aa{}st\aa{}, at to termer er lig hinanden. Herudover kan vi negere formler, s\ae{}tte formler sammen med implikationstegnet $\mathrel{\dot{\Rightarrow}}$ samt s\ae{}tte alkvantoren $\dot{\forall}$
foran formler. Bem\ae{}rk at $\mathrel{\dot{\Rightarrow}}$ er h\o{}jreassociativ; et udtryk som f.eks.\ "
begin math peano r peano imply peano s peano imply peano t end math
end " skal l\ae{}ses som "
begin math peano r peano imply parenthesis peano s peano imply peano t end parenthesis end math
end ".
\subsection{Aksiomatisk system} \label{sec:aksiomer}
Beviserne i denne rapport baserer sig p\aa{} det aksiomatiske system "
begin math system prime s end math
end " fra \cite{kn:peano}. Dette system best\aa{}r af 14 aksiomskemaer (kaldet "
begin math axiom prime a one end math
end "--- "
begin math axiom prime a five end math
end " og "
begin math axiom prime s one end math
end "---"
begin math axiom prime s nine end math
end ") og 2 slutningsregler (kaldet "
begin math rule prime mp end math
end " og "
begin math rule prime gen end math
end "). For overblikkets skyld genoptrykker jeg dem her:
\display{"
begin math in theory system prime s rule axiom prime a one says all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a two says all meta a indeed all meta b indeed all meta c indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a three says parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a four says all meta c indeed all meta a indeed all meta x indeed all meta b indeed peano sub quote meta a end quote is quote meta b end quote where quote meta x end quote is quote meta c end quote end sub endorse peano all meta x indeed meta b peano imply meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a five says all meta x indeed all meta a indeed all meta b indeed peano nonfree meta x in meta a end nonfree endorse peano all meta x indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply peano all meta x indeed meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule rule prime mp says all meta a indeed all meta b indeed meta a peano imply meta b infer meta a infer meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule rule prime gen says all meta x indeed all meta a indeed meta a infer peano all meta x indeed meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s one says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta a peano is meta c peano imply meta b peano is meta c end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s two says all meta a indeed all meta b indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s three says all meta a indeed not peano zero peano is meta a peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s four says all meta a indeed all meta b indeed meta a peano succ peano is meta b peano succ peano imply meta a peano is meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s five says all meta a indeed meta a peano plus peano zero peano is meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s six says all meta a indeed all meta b indeed meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s seven says all meta a indeed meta a peano times peano zero peano is peano zero end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s eight says all meta a indeed all meta b indeed meta a peano times parenthesis meta b peano succ end parenthesis peano is parenthesis meta a peano times meta b end parenthesis peano plus meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s nine says all meta a indeed all meta b indeed all meta c indeed all meta x indeed macro newline peano sub meta b is meta a where meta x is peano zero end sub endorse peano sub meta c is meta a where meta x is meta x peano succ end sub endorse macro newline meta b peano imply peano all meta x indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta x indeed meta a end rule end math
end "}
For at lette forst\aa{}elsen af "
begin math system s prime end math
end " vil jeg slutte dette afsnit med en generel beskrivelse af de to komponenter, som "
begin math system s prime end math
end " best\aa{}r af: Aksiomskemaer og slutningsregler.
Et aksiom er en formel, som vi kan tage for givet. Et aksiomskema repr\ae{}senterer en m\ae{}ngde af aksiomer. F.eks.\ f\o{}lger det af aksiom "
begin math axiom prime a one end math
end ", at formler som "
begin math peano r peano imply peano t peano imply peano r end math
end " og "
begin math peano s peano imply peano zero peano is peano zero peano succ peano imply peano s end math
end " er aksiomer. Variablene "
begin math meta a end math
end " og "
begin math meta b end math
end " i "
begin math axiom prime a one end math
end " kaldes for meta-variable. Meta-variable er ikke en del af Peano aritmetik; de bruges i stedet, n\aa{}r vi taler om Peano aritmetik --- hvilket vi jo g\o{}r i vores aksiomsystem. (Der er en tilsvarende forskel mellem den alkvantor $\dot{\forall}$, som vi bruger i Peano aritmetik, og den alkvantor $\forall$, som vi bruger i "
begin math system s prime end math
end "). Meta-variable kan variere over Peano variable, vilk\aa{}rlige termer eller formler. I "
begin math system s prime end math
end " bruges ``"
begin math meta x end math
end "'' om den f\o{}rste slags meta-variable, mens ``"
begin math meta a end math
end "'', ``"
begin math meta b end math
end "'' og ``"
begin math meta c end math
end "'' bruges om de to andre slags meta-variable.
Ud over aksiomskemaerne indeholder "
begin math system prime s end math
end " som n\ae{}vnt to slutningsregler. En slutningsregel er en regel for, hvordan vi kan vise formler ud fra andre formler, som allerede er bevist. F.eks.\ siger "
begin math rule prime mp end math
end ", at vi kan vise formlen "
begin math meta b end math
end ", hvis vi i forvejen har vist de to formler "
begin math meta a peano imply meta b end math
end " og "
begin math meta a end math
end ". Slutningsreglerne definerer s\aa{}ledes en beviselighedsrelation $\vdash$ mellem formler.
Tilsammen definerer aksiomskemaerne og slutningsreglerne en m\ae{}ngde af beviselige formler: En beviselig formel er enten et aksiom, eller ogs\aa{} kan den bevises ud fra aksiomerne ved hj\ae{}lp af slutningsreglerne. Jeg vil bruge ordet ``systems\ae{}tning'' som en f\ae{}llesbetegnelse for aksiomskemaer og slutningsregler.
En systems\ae{}tning kan indeholde en eller flere sidebetingelser; dette g\ae{}lder for tre af aksiomskemaerne i system "
begin math system prime s end math
end " ("
begin math axiom prime a four end math
end ", "
begin math axiom prime a five end math
end " og "
begin math axiom prime s nine end math
end "). En sidebetingelse i en systems\ae{}tning definerer et krav til den korrekte anvendelse af systems\ae{}tningen. I "
begin math axiom prime s nine end math
end " er det f.eks.\ klart, at implikationen "
begin bracket meta b peano imply peano all meta x indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta x indeed meta a end bracket
end " ikke har generel gyldighed: "
begin math meta b end math
end " skal v\ae{}re et basistilf\ae{}lde, og formlen "
begin math meta a peano imply meta c end math
end " skal repr\ae{}sentere det induktive skridt. Disse ekstra krav er formuleret i de to sidebetingelser i "
begin math axiom prime s nine end math
end ". Rent syntaktisk bruger vi tegnet ``$\models$'' til at adskille en sidebetingelse fra den \o{}vrige del af systems\ae{}tningen.
\section{Lemmaer, afledte lemmaer og makroer} \label{sec:hjaelpesaetninger}
Som n\ae{}vnt i indledningen har jeg opdelt beviset for (\ref{eq:com}) i 28 hj\ae{}lpes\ae{}tninger. For overskuelighedens skyld har jeg inddelt disse hj\ae{}lpes\ae{}tninger i tre grupper: Lemmaer, afledte lemmaer og makroer. Distinktionen mellem disse grupper er ikke knivskarp, men den g\o{}r det lettere at forklare bevisets struktur. I dette afsnit
vil jeg gennemg\aa{} hver gruppe og pr\ae{}sentere de hj\ae{}lpes\ae{}tninger, som grupperne indeholder.
%*** Variabelnavns-itemize ***
I min definition af de forskellige hj\ae{}lpes\ae{}tninger vil jeg bruge de f\o{}lgende konventioner for variabelnavne:
%
\begin{itemize}
\item Meta-variable, der varierer over formler, betegnes med ``"
begin math meta a end math
end "'', ``"
begin math meta b end math
end "'', ``"
begin math meta c end math
end "'', ``"
begin math meta d end math
end "'', ``"
begin math meta e end math
end "'' og ``"
begin math meta f end math
end "''.
\item Meta-variable, der varierer over vilk\aa{}rlige termer, betegnes med ``"
begin math meta t end math
end "'', ``"
begin math meta r end math
end "'', ``"
begin math meta s end math
end "'' og ``"
begin math meta u end math
end "''.
\item Meta-variable, der varierer over Peano variable, betegnes med ``"
begin math meta z end math
end "''.
\item Peano variable betegnes med ``"
begin math peano t end math
end "'', ``"
begin math peano r end math
end "'' og ``"
begin math peano s end math
end "''(som allerede n\ae{}vnt i afsnit \ref{sec:termer}).
\end{itemize}
%
\subsection{Lemmaer} \label{sec:lemmaer}
Under kategorien ``lemmaer'' vil jeg for det f\o{}rste rubricere hoveds\ae{}tningen (\ref{eq:com}), formuleret i Peano aritmetik:
\display{
"
begin math in theory system prime s lemma plus commutativity says peano t peano plus peano r peano is peano r peano plus peano t end lemma end math
end "
%
\footnote{"
begin math pyk define plus commutativity as "plus commutativity" end define end math
end ". Dette er en ``pyk definition'', som omtalt i afsnit \ref{sec:saerlig}.}
%
}
Som det kan ses, benytter "
begin math plus commutativity end math
end " sig ikke af meta-variable (som f.eks.\
"
begin math meta t end math
end " og "
begin math meta r end math
end "), men derimod af Peano variablene "
begin math peano t end math
end " og "
begin math peano r end math
end ". Der er en teknisk forklaring herp\aa{}: "
begin math plus commutativity end math
end " skal vises ved induktion, og derfor kommer aksiomskemaet "
begin math axiom prime s nine end math
end " uundg\aa{}eligt til at indg\aa{} i beviset. Som n\ae{}vnt i afsnit \ref{sec:aksiomer} benytter "
begin math axiom prime s nine end math
end " sig af sidebetingelser; og Logiwebs bevischecker kan (endnu) ikke evaluere sidebetingelser, der indeholder meta-variable.
I afsnit 3.1 i l\ae{}rebogen \cite{kn:mendel} beviser Mendelson "
begin math plus commutativity end math
end " under navnet ``s\ae{}tning 3.2(h)''. For at n\aa{} frem til s\ae{}tning 3.2(h) viser Mendelson f\o{}rst de f\o{}lgende seks lemmaer:
%
\footnote{Det skal lige n\ae{}vnes, at Mendelson bruger meta-variable i sin formulering af "
begin math mendelson three two f end math
end " og "
begin math mendelson three two g end math
end ". Fordi disse lemmaer skal vises ved induktion, bruger jeg Peano variable i stedet for.}
%
\display{
"
begin math in theory system prime s lemma equal reflexivity says all meta t indeed meta t peano is meta t end lemma end math
end "
%
\footnote{"
begin math pyk define equal reflexivity as "equal reflexivity" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma equal symmetry 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 equal symmetry as "equal symmetry" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma equal transitivity 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 equal transitivity as "equal transitivity" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma mendelson three two d says all meta t indeed all meta u indeed all meta s indeed meta t peano is meta u peano imply meta s peano is meta u peano imply meta t peano is meta s end lemma end math
end "
%
\footnote{"
begin math pyk define mendelson three two d as "mendelson three two d" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma mendelson 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 three two f as "mendelson three two f" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma mendelson three two g says peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end lemma end math
end "
%
\footnote{"
begin math pyk define mendelson three two g as "mendelson three two g" end define end math
end "}
%
}
Lemmaerne "
begin math equal reflexivity end math
end ", "
begin math equal symmetry end math
end " og
"
begin math equal transitivity end math
end " udsiger tilsammen, at $\stackrel{p}{=}$ er en \ae{}kvivalensrelation --- alts\aa{} en relation, som er refleksiv, symmetrisk og transitiv. Indholdet af de tre lemmaer
"
begin math mendelson three two d end math
end ", "
begin math mendelson three two f end math
end " og "
begin math mendelson three two g end math
end " kan ikke sammenfattes lige s\aa{} koncist, s\aa{} jeg har givet dem de samme navne, som de har i \cite{kn:mendel}.
Ligesom "
begin math plus commutativity end math
end " skal "
begin math mendelson three two f end math
end " og "
begin math mendelson three two g end math
end " bevises ved induktion. For at begr\ae{}nse l\ae{}ngden af de enkelte beviser har jeg valgt at definere basistilf\ae{}ldene og de induktive skridt som selvst\ae{}ndige lemmaer. P\aa{} denne m\aa{}de f\aa{}r vi yderligere seks lemmaer:
\display{
"
begin math in theory system prime s lemma mendelson 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 three two f base as "mendelson three two f base" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma mendelson 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 three two f induction as "mendelson three two f induction" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma mendelson three two g base says peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end lemma end math
end "
%
\footnote{"
begin math pyk define mendelson three two g base as "mendelson three two g base" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma mendelson three two g induction says peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end lemma end math
end "
%
\footnote{"
begin math pyk define mendelson three two g induction as "mendelson three two g induction" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma plus commutativity 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 plus commutativity base as "plus commutativity base" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma plus commutativity 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 plus commutativity induction as "plus commutativity induction" end define end math
end "}
%
}
Bem\ae{}rk at induktionen i "
begin math mendelson three two g end math
end " og "
begin math plus commutativity end math
end " forl\o{}ber efter variablen "
begin math peano r end math
end " (og ikke efter "
begin math peano t end math
end ").
Flere lemmaer er der ikke i denne rapport; en opt\ae{}lling viser, at der i alt er 13 lemmaer.
\subsection{Afledte lemmaer}
Som navnet antyder, er de afledte lemmaer afledt fra de lemmaer, som jeg pr\ae{}senterede i afsnit \ref{sec:lemmaer}.
%
\footnote{Jeg vil bruge ordet ``moderlemma'' om et lemma, ud fra hvilket man kan aflede andre lemmaer.}
%
Jeg vil i alt definere 6 afledte lemmaer. De kan opdeles i tre undergrupper: Regellemmaer, betingede regellemmaer og navneafledte lemmaer.
\subsubsection{Regellemmaer} \label{sec:regellemmaer}
Som vi senere vil se i afsnit \ref{sec:condmpbevis}, kan vi altid bevise
"
begin math meta a infer meta b end math
end ",
\noindent hvis vi i forvejen har et bevis for:
"
begin math meta a peano imply meta b end math
end ".
\noindent Ved et ``regellemma'' forst\aa{}r jeg et lemma af formen "
begin math meta a infer meta b end math
end ", som er afledt fra et lemma af formen "
begin math meta a peano imply meta b end math
end ". N\aa{}r et lemma skal anvendes i beviser, er det som regel lettere at arbejde med regellemmaet end med det tilsvarende moderlemma.
Det g\ae{}lder ogs\aa{} for de tre lemmaer "
begin math equal symmetry end math
end ", "
begin math equal transitivity end math
end " og "
begin math mendelson three two d end math
end " fra afsnit \ref{sec:lemmaer}. Derfor vil jeg bevise de tilsvarende tre regellemmaer:
\display{
"
begin math in theory system prime s lemma mendelson three two d rule says macro newline all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r infer meta s peano is meta r infer meta t peano is meta s end lemma end math
end "
%
\footnote{"
begin math pyk define mendelson three two d rule as "mendelson three two d rule" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma equal transitivity rule says macro newline all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r infer meta r peano is meta s infer meta t peano is meta s end lemma end math
end "
%
\footnote{"
begin math pyk define equal transitivity rule as "equal transitivity rule" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma equal symmetry rule says all meta t indeed all meta r indeed meta t peano is meta r infer meta r peano is meta t end lemma end math
end "
%
\footnote{"
begin math pyk define equal symmetry rule as "equal symmetry rule" end define end math
end "}
%
}
\begin{sloppypar}
Jeg kunne ogs\aa{} have bevist regellemmaer svarende til "
begin math mendelson three two f induction end math
end ", "
begin math mendelson three two g induction end math
end " og "
begin math plus commutativity induction end math
end ". Imidlertid har jeg valgt kun at bevise de tre regellemmaer, som kan bruges i beviset for "
begin math plus commutativity end math
end ". Regellemmaer har ikke megen v\ae{}rdi i sig selv; de er et middel til at g\o{}re beviser kortere og mere overskuelige.
\end{sloppypar}
\subsubsection{Betingede regellemmaer}
Et yderligere raffinement er at g\aa{} fra regellemmaets form:
"
begin math meta a infer meta b end math
end "
\noindent til den betingede form:
"
begin math meta c peano imply meta a infer meta c peano imply meta b end math
end "
\noindent Ved et ``betinget regellemma'' forst\aa{}r jeg et afledt lemma, der har denne form. Jeg vil bevise de f\o{}lgende to betingede regellemmaer:\\
\display{
"
begin math in theory system prime s lemma equal transitivity conditioned rule says macro newline all meta a indeed all meta t indeed all meta r indeed all meta s indeed meta a peano imply meta t peano is meta r infer meta a peano imply meta r peano is meta s infer meta a peano imply meta t peano is meta s end lemma end math
end "
%
\footnote{"
begin math pyk define equal transitivity conditioned rule as "equal transitivity conditioned rule" end define end math
end "}
%
}
\display{
"
begin math in theory system prime s lemma mendelson three two d conditioned rule says macro newline all meta a indeed all meta t indeed all meta r indeed all meta s indeed meta a peano imply meta t peano is meta r infer meta a peano imply meta s peano is meta r infer meta a peano imply meta t peano is meta s end lemma end math
end "
%
\footnote{"
begin math pyk define mendelson three two d conditioned rule as "mendelson three two d conditioned rule" end define end math
end "}
%
}
Jeg beviser netop disse to betingede regellemmaer, fordi de kan bruges i beviset for "
begin math plus commutativity end math
end ". Ligesom i afsnit \ref{sec:regellemmaer} g\ae{}lder det, at der ikke er nogen selvst\ae{}ndig grund til at bevise betingede regellemmaer.
\subsubsection{Navneafledte lemmaer}
Den sidste kategori af afledte lemmaer indeholder kun et enkelt lemma. Det er defineret som f\o{}lger:
\display{
"
begin math in theory system prime s lemma mendelson three two g rt switch 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 three two g rt switch as "mendelson three two g rt switch" end define end math
end "}
%
}
Som man kan se, er dette lemma helt identisk med lemma "
begin math mendelson three two g end math
end " fra afsnit \ref{sec:lemmaer} --- bortset fra at der er byttet om p\aa{} de to Peano variable "
begin math peano r end math
end " og "
begin math peano t end math
end ". Derfor kalder jeg "
begin math mendelson three two g rt switch end math
end " for et ``navneafledt lemma''. Det viser sig, at det er denne form af "
begin math mendelson three two g end math
end ", som vi f\aa{}r brug for, n\aa{}r vi skal vise "
begin math plus commutativity end math
end ". Dette er et eksempel p\aa{} ulempen ved at arbejde med Peano variable frem for meta-variable: Vi kan ikke abstrahere fra variablenes navne. Man kunne naturligvis l\o{}se problemet ved at bevise den brugbare form til at begynde med. Jeg har valgt l\o{}sningen med "
begin math mendelson three two g rt switch end math
end " for at se, hvor meget ekstra arbejde det kr\ae{}ver at \ae{}ndre variabelnavnene i et tilf\ae{}lde som dette.
\subsection{Makroer} \label{sec:makroer}
Ved en makro forst\aa{}r jeg en generel hj\ae{}lpes\ae{}tning, der kan bruges i beviset for mange forskellige slags s\ae{}tninger. I denne rapport er der i alt 9 makroer. Jeg har alene defineret og bevist disse makroer for at bruge dem i beviset for "
begin math plus commutativity end math
end "; alligevel er de fleste af makroerne generelle nok til, at man ogs\aa{} kan bruge dem i andre sammenh\ae{}nge.
I det f\o{}lgende vil jeg for hver enkelt makro pr\ae{}sentere den formelle definition og forklare makroens indhold.
% form\aa{}let med makroen.
%hvordan man intuitivt kan forst\aa{} makroens indhold.
\display{
"
begin math in theory system prime s lemma weakening 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 weakening as "weakening" end define end math
end ". Bem\ae{}rk at Logiweb kalder alle hj\ae{}lpes\ae{}tninger for for ``lemmaer'' --- ogs\aa{} dem, som jeg kalder for ``makroer''.}
%
}
Denne makro tillader os at g\o{}re formler betingede. Hvis vi har vist, at formel "
begin math meta a end math
end " g\ae{}lder ubetinget, s\aa{} m\aa{} vi ogs\aa{} gerne antage, at "
begin math meta a end math
end " g\ae{}lder under \mbox{betingelsen "
begin math meta b end math
end "}.
\display{
"
begin math in theory system prime s lemma double mp prime says all meta c indeed all meta d indeed all meta e indeed meta c peano imply meta d peano imply meta e infer meta c infer meta d infer meta e end lemma end math
end "
%
\footnote{"
begin math pyk define double mp prime as "double mp prime" end define end math
end "}
%
}
Makroen "
begin math double mp prime end math
end " kan spare os for en enkelt bevislinie i de tilf\ae{}lde, hvor man ellers ville bruge slutningsreglen "
begin math rule prime mp end math
end " to gange i tr\ae{}k.
\display{
"
begin math in theory system prime s lemma conditioned mp prime says macro newline all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta a peano imply meta b infer meta a peano imply meta c end lemma end math
end "
%
\footnote{"
begin math pyk define conditioned mp prime as "conditioned mp prime" end define end math
end "}
%
}
Indholdet af slutningsreglen "
begin math rule prime mp end math
end " er som bekendt, at man kan slutte "
begin math meta c end math
end " ud fra "
begin math meta b peano imply meta c end math
end " og "
begin math meta b end math
end ". Man kan t\ae{}nke p\aa{} makroen "
begin math conditioned mp prime end math
end " som en betinget udgave af "
begin math rule prime mp end math
end ": Den siger, at vi har lov til at bruge "
begin math rule prime mp end math
end " under en vilk\aa{}rlig betingelse "
begin math meta a end math
end ", hvis vi tilf\o{}jer "
begin math meta a end math
end " til begge pr\ae{}misser og til konklusionen.
\display{
"
begin math in theory system prime s lemma double conditioned mp prime says macro newline all meta a indeed all meta d indeed all meta e indeed all meta f indeed meta a peano imply meta d peano imply meta e peano imply meta f infer meta a peano imply meta d infer meta a peano imply meta e infer meta a peano imply meta f end lemma end math
end "
%
\footnote{"
begin math pyk define double conditioned mp prime as "double conditioned mp prime" end define end math
end "}
%
}
Af og til kan man f\aa{} brug for at benytte makroen "
begin math conditioned mp prime end math
end " to gange i tr\ae{}k. Her kan "
begin math double conditioned mp prime end math
end " spare en bevislinie. Denne makro forholder sig alts\aa{} til "
begin math conditioned mp prime end math
end " p\aa{} n\o{}jagtigt samme m\aa{}de, som "
begin math double mp prime end math
end " forholder sig til "
begin math rule prime mp end math
end ".
\display{
"
begin math in theory system prime s lemma imply transitivity says all meta d indeed all meta e indeed all meta f indeed meta d peano imply meta e infer meta e peano imply meta f infer meta d peano imply meta f end lemma end math
end "
%
\footnote{"
begin math pyk define imply transitivity as "imply transitivity" end define end math
end "}
%
}
Som navnet antyder, udsiger "
begin math imply transitivity end math
end ", at relationen $\mathrel{\dot{\Rightarrow}}$ er transitiv; ud fra "
begin math meta d peano imply meta e end math
end " og "
begin math meta e peano imply meta f end math
end " kan vi slutte "
begin math meta d peano imply meta f end math
end ".
\display{
"
begin math in theory system prime s lemma permute antecedents says macro newline all meta d indeed all meta e indeed all meta f indeed meta d peano imply meta e peano imply meta f infer meta e peano imply meta d peano imply meta f end lemma end math
end "
%
\footnote{"
begin math pyk define permute antecedents as "permute antecedents" end define end math
end "}
%
}
I en term som "
begin math meta d peano imply meta e peano imply meta f end math
end " kaldes "
begin math meta d end math
end " og "
begin math meta e end math
end " for antecedenterne, mens "
begin math meta f end math
end " kaldes for konsekvensen. Indholdet af "
begin math permute antecedents end math
end " er, at antecedenternes r\ae{}kkef\o{}lge er ligegyldig; vi kan omskrive "
begin math meta d peano imply meta e peano imply meta f end math
end " til "
begin math meta e peano imply meta d peano imply meta f end math
end ".
\display{
"
begin math in theory system prime s lemma add one says all meta t indeed all meta r indeed meta t peano is meta r infer meta t peano succ peano is meta r peano succ end lemma end math
end "
%
\footnote{"
begin math pyk define add one as "add one" end define end math
end "}
%
}
Denne makro er afledt fra aksiomskemaet "
begin math axiom prime s two end math
end ": Hvis "
begin math axiom prime s two end math
end " havde v\ae{}ret et lemma, ville jeg have rubriceret "
begin math add one end math
end " som et regellemma (med "
begin math axiom prime s two end math
end " som moderlemma).
\newpage
\display{
"
begin math in theory system prime s lemma substitution macro says macro newline all meta z indeed all meta c indeed all meta a indeed all meta d indeed peano sub quote meta a end quote is quote meta d end quote where quote meta z end quote is quote meta c end quote end sub endorse meta d infer meta a end lemma end math
end "
%
\footnote{"
begin math pyk define substitution macro as "substitution macro" end define end math
end "}
%
}
Denne makro siger, at vi kan slutte "
begin math meta a end math
end " ud fra "
begin math meta d end math
end ", hvis vi kan frembringe "
begin math meta a end math
end " ud fra "
begin math meta d end math
end " ved hj\ae{}lp af en substitution. F.eks.\ kan vi slutte "
begin math peano zero peano is peano zero end math
end " ud fra "
begin math peano t peano is peano t end math
end ", fordi vi kan f\aa{} "
begin math peano zero peano is peano zero end math
end " frem ved at erstatte "
begin math peano t end math
end " med "
begin math peano zero end math
end " i "
begin math peano t peano is peano t end math
end ".
\display{"
begin math in theory system prime s lemma induction macro says all meta a indeed all meta b indeed all meta c indeed all meta z indeed macro newline peano sub quote meta a end quote is quote meta a end quote where quote meta z end quote is quote meta z end quote end sub endorse peano sub meta b is meta a where meta z is peano zero end sub endorse peano sub meta c is meta a where meta z is meta z peano succ end sub endorse macro newline meta b infer meta a peano imply meta c infer meta a end lemma end math
end "
%
\footnote{"
begin math pyk define induction macro as "induction macro" end define end math
end "}
%
}
I et induktionsbevis ligger det meste af arbejdet som regel i at vise basistilf\ae{}ldet og det induktive skridt. N\aa{}r dette er gjort, mangler man bare at henvise til princippet om matematisk induktion. Dette arbejde er indkapslet i "
begin math induction macro end math
end ". Med denne makro kan man f\ae{}rdigg\o{}re et induktionsbevis med en enkelt linie, n\aa{}r man f\o{}rst har vist basistilf\ae{}ldet "
begin math meta b end math
end " og det induktive skridt "
begin math meta a peano imply meta c end math
end ".
Bem\ae{}rk i\o{}vrigt den lidt pudsige sidebetingelse "
begin math peano sub quote meta a end quote is quote meta a end quote where quote meta z end quote is quote meta z end quote end sub end math
end ", der siger, at "
begin math meta a end math
end " er lig med "
begin math meta a end math
end ", hvis vi erstatter enhver fri forekomst af Peano variablen "
begin math meta z end math
end " i "
begin math meta a end math
end " med sig selv. Det er klart, at dette er opfyldt for enhver formel "
begin math meta a end math
end " og enhver Peano variabel "
begin math meta z end math
end ", s\aa{} ved f\o{}rste \o{}jekast virker det som en overfl\o{}dig sidebetingelse.
Det er imidlertid n\o{}dvendigt eksplicit at fort\ae{}lle Logiweb, at betingelsen er opfyldt, hvis beviset for "
begin math induction macro end math
end " skal g\aa{} igennem. Dette skyldes, at Logiweb ikke kan evaluere udtryk, der indeholder meta-variable (som allerede omtalt i afsnit \ref{sec:aksiomer}). Ved at formulere meta-udsagnet \mbox{"
begin math peano sub quote meta a end quote is quote meta a end quote where quote meta z end quote is quote meta z end quote end sub end math
end "} som en sidebetingelse, kan vi bruge det direkte i beviset, uden at Logiweb evaluerer det.
%
\footnote{Det omtalte bevis st\aa{}r i afsnit \ref{sec:inductionbevis}.}
%
N\aa{}r vi skal til at anvende "
begin math induction macro end math
end " i andre beviser, vil betingelsen altid v\ae{}re opfyldt; s\aa{} den ekstra sidebetingelse udg\o{}r kun et \ae{}stetisk problem.
\newpage
\section{Beviser for makroerne} \label{sec:bevismakroer}
I dette afsnit vil jeg bevise de 9 makroer, som blev pr\ae{}senteret i afsnit \ref{sec:makroer}. Jeg beviser makroerne i den samme r\ae{}kkef\o{}lge, som blev brugt i dette afsnit.
Tre af makroerne er s\aa{} generelle, at de kan bruges i beviserne for de andre makroer. I tabel 1 kan man se, hvilke makroer der bruges i beviserne for hvilke andre makroer.
% makro-makro tabel
%\begin{tiny}
\begin{center}
\begin{table} \label{tab:makromakro}
\fbox{
\begin{tabular}{l|ccccccccc}
& \rotatebox{90}{"
begin math weakening end math
end "} & \rotatebox{90}{"
begin math double mp prime end math
end "} &
\rotatebox{90}{"
begin math conditioned mp prime end math
end "} &
\rotatebox{90}{"
begin math double conditioned mp prime end math
end "} &
\rotatebox{90}{"
begin math imply transitivity end math
end "} &
\rotatebox{90}{"
begin math permute antecedents end math
end "} &
\rotatebox{90}{"
begin math add one end math
end "} & \rotatebox{90}{"
begin math substitution macro end math
end "} & \rotatebox{90}{"
begin math induction macro end math
end "}
\\ \hline
"
begin math weakening end math
end " & &&&& $\bullet$ & $\bullet$ &&& \\ \hline
"
begin math double mp prime end math
end " & & & $\bullet$ &&&&&& $\bullet$ \\ \hline
"
begin math conditioned mp prime end math
end " & &&& $\bullet$ & $\bullet$ & $\bullet$ &&&
\end{tabular}
}
\caption[Makroer der beviser makroer]{Makroer der beviser makroer. En ``$\bullet$'' i r\ae{}kke $\mathit{X}$, s\o{}jle $\mathit{Y}$ betyder, at makro $\mathit{X}$ bliver brugt i beviset for makro $\mathit{Y}$.}
\end{table}
\end{center}
%\end{tiny}
\subsection{Bevis for "
begin math weakening end math
end " }
Her er beviset for "
begin math weakening end math
end ":
\display{
"
begin math in theory system prime s lemma weakening says all meta a indeed all meta b indeed meta a infer meta b peano imply meta a end lemma end math
end "
}
"
begin math system prime s proof of weakening reads arbitrary meta a end line arbitrary meta b end line line ell b premise meta a end line line ell c 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 c modus ponens ell b indeed meta b peano imply meta a qed end math
end "
\verb| | \\ \noindent Da dette er rapportens f\o{}rste bevis, vil jeg bringe nogle ekstra kommentarer. Oven over beviset har jeg gentaget definitionen af det, der skal bevises; dette er kun for overblikkets skyld --- det er ikke en formel n\o{}dvendighed. Selve beviset for "
begin math weakening end math
end " best\aa{}r af fem linier, nummereret fra 1 til 5. En bevislinie kan have to former. Den f\o{}rste form er:
%
\begin{eqnarray*}
\texttt{Argumentation} & \gg & \texttt{Konklusion} %\label{eq:linie}
\end{eqnarray*}
%
hvor \texttt{Konklusion} er det som linien beviser, mens teksten i \texttt{Argumentation} udg\o{}r en begrundelse for, at \texttt{Konklusion} g\ae{}lder. F.eks.\ siger linie 4, at meta-formlen "
begin math meta a peano imply meta b peano imply meta a end math
end " g\ae{}lder, fordi den kan udledes fra aksiomskemaet "
begin math axiom prime a one end math
end " ved substitution. I linie 5 skal argumentationen l\ae{}ses p\aa{} den m\aa{}de, at konklusionerne fra linie 4 og 3 bliver brugt som pr\ae{}misser til slutningsreglen "
begin math rule prime mp end math
end ". Den generelle betydning af konstruktionen ``"
begin math var x modus ponens var y end math
end "'' er, at konklusionen fra "
begin math var y end math
end " bliver brugt som pr\ae{}mis i forhold til "
begin math var x end math
end ".
Den anden form, en bevislinie kan have, er:
%
\begin{eqnarray*}
\texttt{N\o{}gleord} & \gg & \texttt{Konklusion} %\label{eq:linie2}
\end{eqnarray*}
%
hvor \texttt{N\o{}gleord} er et af de tre ord ``Arbitrary'', ``Premise'' eller ``Side-condition''. Betydningen af ordene ``Premise'' og ``Side-condition'' er \aa{}benlys: De angiver, at liniens konklusion indg\aa{}r som en pr\ae{}mis (hhv.\ sidebetingelse) i den hj\ae{}lpes\ae{}tning, der skal bevises. F.eks.\ siger bevisets linie 3, at "
begin math weakening end math
end " bruger meta-formlen "
begin math meta a end math
end "
som pr\ae{}mis. N\aa{}r ordet ``Arbitrary'' bruges, best\aa{}r konklusionen af en meta-variabel (f.eks. "
begin math meta a end math
end " i linie 1 og "
begin math meta b end math
end " i line 2). Meningen med ``Arbitrary'' er af teknisk karakter: Ideen er at udtrykke, at vi ikke antager noget om den p\aa{}g\ae{}ldende meta-variabel, og at vi derfor har ret til at binde meta-variablen med en alkvantor i den hj\ae{}lpes\ae{}tning, der skal bevises. I det forh\aa{}ndenv\ae{}rende bevis fungerer de to linier med ``Arbitrary'' alts\aa{} som berettigelse for, at "
begin math weakening end math
end " er kvantificeret med ``$\forall {\cal A}\colon \forall {\cal B}\colon $''.
Alt dette har drejet sig om den formelle syntaks for et Logiweb bevis. Der er egentlig ikke s\aa{} meget at sige om selve beviset for "
begin math weakening end math
end "; det er en ganske enkel anvendelse af "
begin math axiom prime a one end math
end " og "
begin math rule prime mp end math
end ".
%\newpage
%*********** double mp prime **************
\subsection{Bevis for "
begin math double mp prime end math
end "}
\display{
"
begin math in theory system prime s lemma double mp prime says all meta c indeed all meta d indeed all meta e indeed meta c peano imply meta d peano imply meta e infer meta c infer meta d infer meta e end lemma end math
end "
}
"
begin math system prime s proof of double mp prime reads arbitrary meta c end line arbitrary meta d end line arbitrary meta e end line line ell a premise meta c peano imply meta d peano imply meta e end line line ell b premise meta c end line line ell c premise meta d end line line ell d because rule prime mp modus ponens ell a modus ponens ell b indeed meta d peano imply meta e end line because rule prime mp modus ponens ell d modus ponens ell c indeed meta e qed end math
end "
\verb| | \\ \noindent Som n\ae{}vnt i afsnit \ref{sec:makroer} er ideen med "
begin math double mp prime end math
end " at indkapsle to anvendelser af "
begin math rule prime mp end math
end " i en enkelt bevislinie. Det er derfor ganske naturligt, at kernen i beviset for "
begin math double mp prime end math
end " netop best\aa{}r af to anvendelser af "
begin math rule prime mp end math
end ".
\newpage
%*********** conditioned mp prime **************
\subsection{Bevis for "
begin math conditioned mp prime end math
end " } \label{sec:condmpbevis}
\display{
"
begin math in theory system prime s lemma conditioned mp prime says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta a peano imply meta b infer meta a peano imply meta c end lemma end math
end "
}
"
begin math system prime s proof of conditioned mp prime 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 b peano imply meta c end line line ell b premise meta a peano imply meta b 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 meta a peano imply meta c end line because double mp prime modus ponens ell c modus ponens ell a modus ponens ell b indeed meta a peano imply meta c qed end math
end "
\verb| | \\ \noindent I afsnit \ref{sec:makroer} n\ae{}vnte jeg, at "
begin math conditioned mp prime end math
end " kunne opfattes som en betinget udgave af "
begin math rule prime mp end math
end ". Vi kan ogs\aa{} opfatte "
begin math conditioned mp prime end math
end " som et regellemma i forhold til aksiomskemaet "
begin math axiom prime a two end math
end ": "
begin math axiom prime a two end math
end " har formen "
begin math meta a peano imply meta b peano imply meta c end math
end ", mens "
begin math conditioned mp prime end math
end " har formen "
begin math meta a infer meta b infer meta c end math
end ". Dermed kan vi bruge en meget enkel teknik til at bevise "
begin math conditioned mp prime end math
end ": F\o{}rst opskriver vi pr\ae{}misserne og moderlemmaet, og s\aa{} bruger vi "
begin math rule prime mp end math
end " \'{e}n gang for hver pr\ae{}mis. (I dette tilf\ae{}lde er ``moderlemmaet'' et aksiomskema, men det g\o{}r ingen forskel). Jeg vil ogs\aa{} bruge denne teknik, n\aa{}r vi senere hen skal bevise de egentlige regellemmaer.
%\newpage
%*********** Double conditioned mp prime **************
\subsection{Bevis for "
begin math double conditioned mp prime end math
end " }
\display{
"
begin math in theory system prime s lemma double conditioned mp prime says macro newline all meta a indeed all meta d indeed all meta e indeed all meta f indeed meta a peano imply meta d peano imply meta e peano imply meta f infer meta a peano imply meta d infer meta a peano imply meta e infer meta a peano imply meta f end lemma end math
end "
}
"
begin math system prime s proof of double conditioned mp prime reads arbitrary meta a end line arbitrary meta d end line arbitrary meta e end line arbitrary meta f end line line ell a premise meta a peano imply meta d peano imply meta e peano imply meta f end line line ell b premise meta a peano imply meta d end line line ell c premise meta a peano imply meta e end line line ell d because conditioned mp prime modus ponens ell a modus ponens ell b indeed meta a peano imply meta e peano imply meta f end line because conditioned mp prime modus ponens ell d modus ponens ell c indeed meta a peano imply meta f qed end math
end "
\verb| | \\ \noindent Makroen "
begin math double conditioned mp prime end math
end " indkapsler to anvendelser af "
begin math conditioned mp prime end math
end ", s\aa{} beviset er enkelt: Vi anvender "
begin math conditioned mp prime end math
end " to gange.
\newpage
%*********** ImplyTransitivity **************
\subsection{Bevis for "
begin math imply transitivity end math
end "}
\display{
"
begin math in theory system prime s lemma imply transitivity says all meta d indeed all meta e indeed all meta f indeed meta d peano imply meta e infer meta e peano imply meta f infer meta d peano imply meta f end lemma end math
end "
}
"
begin math system prime s proof of imply transitivity reads arbitrary meta d end line arbitrary meta e end line arbitrary meta f end line line ell a premise meta d peano imply meta e end line line ell b premise meta e peano imply meta f end line line ell c because weakening modus ponens ell b indeed meta d peano imply meta e peano imply meta f end line because conditioned mp prime modus ponens ell c modus ponens ell a indeed meta d peano imply meta f qed end math
end "
%\newpage
\verb| | \\ \noindent Hidtil har beviserne v\ae{}ret s\aa{} enkle, at det har v\ae{}ret let at forklare deres struktur med et par s\ae{}tninger. Denne fremgangsm\aa{}de er ikke holdbar for de mere komplicerede beviser. I disse tilf\ae{}lde vil jeg i stedet illustrere bevisernes struktur med tr\ae{}er som dette:
%*** ImplyTransitivity tegning ***
%\resizebox{15cm}{!}{
\begin{picture}(200,150)%XY 150
%\graphpaper(0,0)(500,500)
\thicklines
\put(150,100){\framebox(30,20){\textbf{7}:$\cal{DF}$}}
\put(180,40){\framebox(30,20){\textbf{4}:$\cal{DE}$}}
\put(180,30){Premise}
\put(180,60){\vector(0,1){40}}
\put(100,40){\framebox(50,20){\textbf{5--6}:$\cal{DEF}$}}
\put(100,30){Premise-W}
\put(105,80){$\textrm{CondMP}'$}
\put(150,60){\vector( 0,1){40}}
%\put( 120,40){\framebox(30,20){\textbf{4}:$\cal{DE}$}}
%\put(120,30){Premise}
%\put(105,80){$\textrm{CondMP}'$}
%\put(180,60){\vector(0,1){40}}
%\put(180,40){\framebox(50,20){\textbf{5--6}:$\cal{DEF}$}}
%\put(180,30){Premise-W}
%\put(150,60){\vector( 0,1){40}}
\end{picture}
%}
\noindent I et ``bevistr\ae{}'' som dette repr\ae{}senterer hver knude en eller to af de centrale bevislinier. Bladene svarer til aksiomer eller pr\ae{}misser, mens bevisets konklusion st\aa{}r i roden. Kanterne er orienteret fra barneknude til for\ae{}ldreknude; betydningen af en kant er, at barneknuden bruges til at bevise for\ae{}ldreknuden. Hver kant er m\ae{}rket med den systems\ae{}tning eller hj\ae{}lpes\ae{}tning, der bruges i argumentationen for for\ae{}ldreknuden.
%
\footnote{Hvis to kanter f\o{}rer op til en knude, er kun den ene kant m\ae{}rket.}
%
Bevislinier, der bruger "
begin math weakening end math
end " i argumentationen, er ikke vist som selvst\ae{}ndige knuder; disse bevislinier er i stedet sl\aa{}et sammen med de linier, som "
begin math weakening end math
end " virker p\aa{}. Der er alts\aa{} nogle knuder, som svarer til to bevislinier; disse knuder er m\ae{}rket med endelsen ``-W'' (som st\aa{}r for ``"
begin math weakening end math
end "'').
\begin{sloppypar}
For at g\o{}re den ovenst\aa{}ende tegning p\ae{}n har jeg forkortet navnet \mbox{``"
begin math conditioned mp prime end math
end "''} og udeladt tegnet ``$\mathrel{\dot{\Rightarrow}}$'' fra de tre knuder. Den slags friheder vil jeg ogs\aa{} tage mig ved de kommende bevistr\ae{}er; og jeg vil kun g\o{}re opm\ae{}rksom p\aa{} den \ae{}ndrede notation, n\aa{}r jeg sk\o{}nner det n\o{}dvendigt.
\end{sloppypar}
\begin{sloppypar}
S\aa{} meget om bevistr\ae{}er. Jeg vil ikke kommentere selve beviset for "
begin math imply transitivity end math
end ", men lade bevistr\ae{}et tale for sig selv.
Jeg vil heller ikke kommentere nogen af de andre beviser, der er illustrerede med bevistr\ae{}er.
\end{sloppypar}
%\newpage
%*********** Permute Antecedents **************
\subsection{Bevis for "
begin math permute antecedents end math
end " }
\display{
"
begin math in theory system prime s lemma permute antecedents says all meta d indeed all meta e indeed all meta f indeed meta d peano imply meta e peano imply meta f infer meta e peano imply meta d peano imply meta f end lemma end math
end "
}
"
begin math system prime s proof of permute antecedents reads arbitrary meta d end line arbitrary meta e end line arbitrary meta f end line line ell a premise meta d peano imply meta e peano imply meta f end line line ell b because weakening modus ponens ell a indeed meta e peano imply meta d peano imply meta e peano imply meta f end line line ell c because axiom prime a two indeed parenthesis meta d peano imply meta e peano imply meta f end parenthesis peano imply parenthesis meta d peano imply meta e end parenthesis peano imply meta d peano imply meta f end line line ell d because weakening modus ponens ell c indeed meta e peano imply parenthesis meta d peano imply meta e peano imply meta f end parenthesis peano imply macro newline parenthesis meta d peano imply meta e end parenthesis peano imply meta d peano imply meta f end line line ell e because conditioned mp prime modus ponens ell d modus ponens ell b indeed meta e peano imply parenthesis meta d peano imply meta e end parenthesis peano imply meta d peano imply meta f end line line ell f because axiom prime a one indeed meta e peano imply meta d peano imply meta e end line because conditioned mp prime modus ponens ell e modus ponens ell f indeed meta e peano imply meta d peano imply meta f qed end math
end "
%\newpage
%*** PermuteAntecedents tegning ***
%\resizebox{15cm}{!}{
\begin{center}
\begin{picture}(0,0)(200,200)
%\graphpaper(0,0)(500,500)
\thicklines
\put(250,160){\framebox(50,20){\textbf{10}:$\cal{EDF}$}}
\put(180,100){\framebox(70,20){\textbf{8}:$\cal{E(DE)(DF)}$}}
\put(250,120){\vector(0,1){40}}
\put(205,140){$\textrm{CondMP}'$}
\put(60,40){\framebox(120,20){\textbf{6--7}:$\cal{E(DEF)(DE)(DF)}$}}
\put(60,30){$A2'$-W}
\put(180,60){\vector(0,1){40}}
\put(135,80){$\textrm{CondMP}'$}
\put(250,40){\framebox(60,20){\textbf{4--5}:$\cal{EDEF}$}}
\put(250,30){Premise-W}
\put(250,60){\vector(0,1){40}}
\put(300,100){\framebox(50,20){\textbf{9}:$\cal{EDE}$}}
\put(300,120){\vector( 0,1){40}}
\put(300,90){$A1'$}
\end{picture}
%}
\end{center}
\newpage
%*********** AddOne **************
\subsection{Bevis for "
begin math add one end math
end "}
\display{
"
begin math in theory system prime s lemma add one says all meta t indeed all meta r indeed meta t peano is meta r infer meta t peano succ peano is meta r peano succ end lemma end math
end "
}
"
begin math system prime s proof of add one reads arbitrary meta t end line arbitrary meta r end line line ell a premise meta t peano is meta r end line line ell b because axiom prime s two indeed meta t peano is meta r peano imply meta t peano succ peano is meta r peano succ end line because rule prime mp modus ponens ell b modus ponens ell a indeed meta t peano succ peano is meta r peano succ qed end math
end "
\verb| | \\ \noindent
Som n\ae{}vnt i afsnit \ref{sec:makroer} kan vi opfatte "
begin math add one end math
end " som et regellemma i forhold til aksiomskemaet "
begin math axiom prime s two end math
end ". Derfor kan vi vise "
begin math add one end math
end " med den samme enkle teknik, som vi s\aa{} f\o{}rste gang i beviset for "
begin math conditioned mp prime end math
end " (afsnit \ref{sec:condmpbevis}): Vi skriver pr\ae{}missen og moderlemmaet op, og vi anvender "
begin math rule prime mp end math
end " \'{e}n gang for hver pr\ae{}mis (i dette tilf\ae{}lde kun en enkelt gang).
%\newpage
%************* substitution macro (ZCAD) ****************
\subsection{Bevis for "
begin math substitution macro end math
end "} \label{sec:substitutionbevis}
\display{"
begin math in theory system prime s lemma substitution macro says macro newline all meta z indeed all meta c indeed all meta a indeed all meta d indeed peano sub quote meta a end quote is quote meta d end quote where quote meta z end quote is quote meta c end quote end sub endorse meta d infer meta a end lemma end math
end "
}
"
begin math system prime s proof of substitution macro reads arbitrary meta z end line arbitrary meta c end line arbitrary meta a end line arbitrary meta d end line line ell q side condition peano sub quote meta a end quote is quote meta d end quote where quote meta z end quote is quote meta c end quote end sub end line line ell a premise meta d end line line ell b because rule prime gen modus ponens ell a indeed peano all meta z indeed meta d end line line ell c because axiom prime a four modus probans ell q indeed peano all meta z indeed meta d peano imply meta a end line because rule prime mp modus ponens ell c modus ponens ell b indeed meta a qed end math
end "
\verb| | \\ \noindent Kernen i dette bevis er linie 8. Konklusionen "
begin bracket peano all meta z indeed meta d peano imply meta a end bracket
end " i denne linie udtrykker, at den generelle formel "
begin math meta d end math
end " medf\o{}rer den mindre generelle formel "
begin math meta a end math
end ". Da vi har antaget "
begin math meta d end math
end ", er det let at konkludere "
begin math meta a end math
end " i linie 9.
I argumentationen i linie 8 benytter vi "
begin math axiom prime a four end math
end ", der som n\ae{}vnt i afsnit \ref{sec:aksiomer} kr\ae{}ver, at en sidebetingelse skal v\ae{}re opfyldt. Derfor bruger vi konstruktionen \mbox{``"
begin math var x modus probans var y end math
end "''}, som markerer, at konklusionen fra "
begin math var y end math
end " kan bruges som sidebetingelse for "
begin math var x end math
end " .
\newpage
%*********** induction macro **************
\subsection{Bevis for "
begin math induction macro end math
end "} \label{sec:inductionbevis}
\display{"
begin math in theory system prime s lemma induction macro says all meta a indeed all meta b indeed all meta c indeed all meta z indeed macro newline peano sub quote meta a end quote is quote meta a end quote where quote meta z end quote is quote meta z end quote end sub endorse peano sub meta b is meta a where meta z is peano zero end sub endorse peano sub meta c is meta a where meta z is meta z peano succ end sub endorse macro newline meta b infer meta a peano imply meta c infer meta a end lemma end math
end "
}
"
begin math system prime s proof of induction macro reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line arbitrary meta z end line line ell q side condition peano sub quote meta a end quote is quote meta a end quote where quote meta z end quote is quote meta z end quote end sub end line line ell a side condition peano sub meta b is meta a where meta z is peano zero end sub end line line ell b side condition peano sub meta c is meta a where meta z is meta z peano succ end sub end line line ell c premise meta b end line line ell d premise meta a peano imply meta c end line line ell e because rule prime gen modus ponens ell d indeed peano all meta z indeed parenthesis meta a peano imply meta c end parenthesis end line line ell f because axiom prime s nine modus probans ell a modus probans ell b indeed meta b peano imply peano all meta z indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta z indeed meta a end line line ell g because double mp prime modus ponens ell f modus ponens ell c modus ponens ell e indeed peano all meta z indeed meta a end line line ell h because axiom prime a four modus probans ell q indeed peano all meta z indeed meta a peano imply meta a end line because rule prime mp modus ponens ell h modus ponens ell g indeed meta a qed end math
end "
\verb| | \\ \noindent
Beviset for "
begin math induction macro end math
end " er langt, men det er ikke s\aa{} kompliceret, at jeg vil illustrere det med et bevistr\ae{}. Kernen i beviset er de f\o{}lgende tre blokke:
%
\begin{itemize}
\item Linie 8, der fort\ae{}ller os, at vi har vist basistilf\ae{}ldet.
\item Linie 9--10, der fort\ae{}ller os, at ogs\aa{} det induktive skridt er vist.
\item Linie 11, der formulerer princippet om matematisk induktion.
\end{itemize}
%
I linie 12 binder vi disse blokke sammen med en "
begin math double mp prime end math
end ", hvilket giver os konklusionen "
begin math all meta z indeed meta a end math
end ". I de sidste to linier fjerner vi Peano alkvantoren herfra, hvorved vi n\aa{}r frem til m\aa{}let: "
begin math meta a end math
end ".
\newpage
\enlargethispage*{5cm}
\section{Beviser for lemmaerne} \label{sec:bevislemmaer}
Jeg beviser lemmaerne i den samme r\ae{}kkef\o{}lge, som bliver brugt i \cite{kn:mendel}. Figur 1 giver en oversigt over, hvordan lemmaerne bruges til at bevise hinanden.
\nopagebreak
%\setcounter{figure}{1} %virker ikke
%\setcounter{figure}{0} %virker delvist (reference:1, ellers: 2)
%\refstepcounter{figure}
\begin{figure}
%\resizebox{\textwidth}{!}{\includegraphics[0cm,0cm][20cm,30cm]{/net/urd/home/disk15/eriksen/.logiweb/peano-%commutativity/legeplads/strukturMinus1.eps}}
\label{fig:graf}
\scalebox{2}{
\resizebox{\textwidth}{!}{
\includegraphics[0cm,5cm][40cm,25cm]{/net/urd/home/disk15/eriksen/.logiweb/peano-commutativity/legeplads/strukturMinus1.eps}
}
}
\caption[Den overordnede struktur af beviset for "
begin math plus commutativity end math
end "]{Den overordnede struktur af beviset for "
begin math plus commutativity end math
end ". En pil fra lemma $\mathit{A}$ til lemma $\mathit{B}$ betyder, at $\mathit{A}$ bliver brugt i beviset for $\mathit{B}$. Den \o{}verste graf viser ikke de afledte lemmaer, og heller ikke basistilf\ae{}ldene og de induktive skridt i de 3 induktionsbeviser. Den nederste graf har disse detaljer med. For at g\o{}re tegningen p\ae{}n er nogle af lemmaernes navne forkortede. ``PC'' st\aa{}r for ``"
begin math plus commutativity end math
end "''; de \o{}vrige forkortelser skulle v\ae{}re umiddelbart forst\aa{}elige.}
\end{figure}
\newpage
De nedenst\aa{}ende tabeller illustrerer, hvordan makroerne bruges i beviserne for lemmaerne.
% makro-lemma tabel, nr. 1
\begin{table} \label{tab:makrolemma}
\begin{center}
\fbox{
\begin{tabular}{l|c|cc|ccc|ccc} % 1 + 9
& \rotatebox{90}{"
begin math equal reflexivity end math
end "} & \rotatebox{90}{"
begin math equal symmetry end math
end "} & \rotatebox{90}{"
begin math equal symmetry rule end math
end "} &
\rotatebox{90}{"
begin math equal transitivity end math
end "} & \rotatebox{90}{"
begin math equal transitivity rule end math
end "} & \rotatebox{90}{"
begin math equal transitivity conditioned rule end math
end "} &
\rotatebox{90}{"
begin math mendelson three two d end math
end "} & \rotatebox{90}{"
begin math mendelson three two d rule end math
end "} & \rotatebox{90}{"
begin math mendelson three two d conditioned rule end math
end "}
\\ \hline
"
begin math weakening end math
end " & &&&$\bullet$&&$\bullet$&&&$\bullet$ \\ \hline
"
begin math double mp prime end math
end " & $\bullet$&&&&$\bullet$&&&$\bullet$& \\ \hline
"
begin math conditioned mp prime end math
end " & &&&$\bullet$&&& && \\ \hline
"
begin math double conditioned mp prime end math
end " & &&&&&$\bullet$& &&$\bullet$ \\ \hline
"
begin math imply transitivity end math
end " & &&&&&& $\bullet$&& \\ \hline
"
begin math permute antecedents end math
end " & &$\bullet$&&&&& $\bullet$&& %\\ \hline
%"
begin math add one end math
end " & &&&&&& && \\ \hline
%"
begin math substitution macro end math
end " & &&&&&& && \\ \hline
%"
begin math induction macro end math
end " & &&&&&& &&
\end{tabular}
}
\end{center}
\begin{center}
% makro-lemma tabel, nr. 2
\fbox{
\begin{tabular}{l|c|c|c|c|c|cc|c|c|c} % 1 + 10
& \rotatebox{90}{"
begin math mendelson three two f base end math
end "} & \rotatebox{90}{"
begin math mendelson three two f induction end math
end "} & \rotatebox{90}{"
begin math mendelson three two f end math
end "} & \rotatebox{90}{"
begin math mendelson three two g base end math
end "} & \rotatebox{90}{"
begin math mendelson three two g induction end math
end "} & \rotatebox{90}{"
begin math mendelson three two g end math
end "} & \rotatebox{90}{"
begin math mendelson three two g rt switch end math
end "} & \rotatebox{90}{"
begin math plus commutativity base end math
end "} & \rotatebox{90}{"
begin math plus commutativity induction end math
end "} & \rotatebox{90}{"
begin math plus commutativity end math
end "}
\\ \hline
"
begin math weakening end math
end " & &$\bullet$&& &$\bullet$&&&&$\bullet$& \\ \hline
%"
begin math double mp prime end math
end " & &&& &&&&&& \\ \hline
%"
begin math conditioned mp prime end math
end " & &&& &&&&&& \\ \hline
%"
begin math double mp prime end math
end " & &&& &&&&&& \\ \hline
%"
begin math imply transitivity end math
end " & &&& &&&&&& \\ \hline
%"
begin math permute antecedents end math
end " & &&& &&&&&& \\ \hline
"
begin math add one end math
end " & &&& $\bullet$&$\bullet$&&&& \\ \hline
"
begin math substitution macro end math
end " & $\bullet$&&& &&&$\bullet$&&& \\ \hline
"
begin math induction macro end math
end " & &&$\bullet$& &&$\bullet$&&&&$\bullet$
\end{tabular}
}
\caption[Makroer der beviser lemmaer]{Makroer der beviser lemmaer. En ``$\bullet$'' i r\ae{}kke $\mathit{X}$, s\o{}jle $\mathit{Y}$ betyder, at makro $\mathit{X}$ bliver brugt i beviset for lemma $\mathit{Y}$. For at g\o{}re tegningen p\ae{n} er informationerne fordelt p\aa{} to tabeller.}
\end{center}
\end{table}
%\end{tiny}
\enlargethispage*{5cm}
\newpage
%*********** EqualReflexitivity **************
\subsection{Bevis for "
begin math equal reflexivity end math
end "}
\display{"
begin math in theory system prime s lemma equal reflexivity says all meta t indeed meta t peano is meta t end lemma end math
end "
}
"
begin math system prime s proof of equal reflexivity 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 because double mp prime modus ponens ell b modus ponens ell a modus ponens ell a indeed meta t peano is meta t qed end math
end "
\verb| | \\ \noindent
Beviset for "
begin math equal reflexivity end math
end " er s\aa{} simpelt, at jeg kun vil give en enkelt kommentar: Ideen med aksiomskemaet "
begin math axiom prime s five end math
end " er egentlig, at det skal v\ae{}re med til at definere betydningen af addition i Peano aritmetik; men som det kan ses af beviset, kan "
begin math axiom prime s five end math
end " ogs\aa{} bruges til at bevise lemmaer om $\stackrel{p}{=}$.
% *********** EqualSymmetry **************
\subsection{Bevis for "
begin math equal symmetry end math
end " og heraf afledt lemma}
\display{
"
begin math in theory system prime s lemma equal symmetry 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 equal symmetry 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 permute antecedents 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 equal reflexivity 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 "
%\newpage
\begin{picture}(200,200)
%\graphpaper(0,0)(500,500)
\thicklines
\put(150,160){\framebox(70,20){\textbf{6}:${\cal TR} \mathrel{\dot{\Rightarrow}} {\cal RT} $}}
\put(130,140){$\textrm{MP}'$}
\put(50,100){\framebox(100,20){\textbf{4}:${\cal TT} \mathrel{\dot{\Rightarrow}} {\cal TR} \mathrel{\dot{\Rightarrow}} {\cal RT}$}}
\put(150,120){\vector( 0,1){40}}
\put(40,80){PermuteAnts}
\put(50,40){\framebox(100,20){\textbf{3}:${\cal TR} \mathrel{\dot{\Rightarrow}} {\cal TT} \mathrel{\dot{\Rightarrow}} {\cal RT}$}}
\put(100,60){\vector(0,1){40}}
\put(50,30){$\textrm{S1}'$}
\put(220,100){\framebox(30,20){\textbf{5}:${\cal TT}$}}
\put(220,120){\vector(0,1){40}}
\put(220,90){EqualReflexivity}
\end{picture}
I det ovenst\aa{}ende bevistr\ae{} er alle forekomster af tegnet ``$\mathrel{\dot{\Rightarrow}}$'' taget med; til geng\ae{}ld er ``$\stackrel{p}{=}$'' underforst\aa{}et --- f.eks.\ skal ``${\cal TR}$'' l\ae{}ses som ``"
begin math meta t peano is meta r end math
end "''. Jeg vil bruge den samme notation i afsnit \ref{sec:equaltransbevis} og \ref{sec:dbevis}.
%\newpage
%*********** Equal Symmetry Rule **************
\display{"
begin math in theory system prime s lemma equal symmetry rule says all meta t indeed all meta r indeed meta t peano is meta r infer meta r peano is meta t end lemma end math
end "
}
"
begin math system prime s proof of equal symmetry rule reads arbitrary meta t end line arbitrary meta r end line line ell a premise meta t peano is meta r end line line ell b because equal symmetry indeed meta t peano is meta r peano imply meta r peano is meta t end line because rule prime mp modus ponens ell b modus ponens ell a indeed meta r peano is meta t qed end math
end "
\verb| | \\ \noindent
Beviset for dette regellemma bruger den samme teknik, som vi s\aa{} f\o{}rste gang i afsnit \ref{sec:condmpbevis}.
%*********** EqualTransitivity **************
\subsection{Bevis for "
begin math equal transitivity end math
end " og heraf afledte lemmaer}
\label{sec:equaltransbevis}
\display{"
begin math in theory system prime s lemma equal transitivity 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 equal transitivity 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 weakening modus ponens ell a indeed meta t peano is meta r peano imply macro newline 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 c because equal symmetry indeed meta t peano is meta r peano imply meta r peano is meta t end line because conditioned mp prime modus ponens ell b modus ponens ell c 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 "
%\newpage
\begin{picture}(200,150) % Equal Transitivity
%\graphpaper(0,0)(500,500)
\thicklines
\put(150,100){\framebox(100,20){\textbf{7}:${\cal TR} \mathrel{\dot{\Rightarrow}} {\cal RS} \mathrel{\dot{\Rightarrow}} {\cal TS}$}}
\put(105,80){$\textrm{CondMP}'$}
\put(10,40){\framebox(140,20){\textbf{4--5}:${\cal TR} \mathrel{\dot{\Rightarrow}} {\cal RT} \mathrel{\dot{\Rightarrow}} {\cal RS} \mathrel{\dot{\Rightarrow}} {\cal TS}$}}
\put(150,60){\vector( 0,1){40}}
\put(10,30){$\textrm{S1}'$-W}
\put(250,40){\framebox(70,20){\textbf{6}:${\cal TR} \mathrel{\dot{\Rightarrow}} {\cal RT}$}}
\put(250,60){\vector(0,1){40}}
\put(250,30){EqualSymmetry}
\end{picture}
\newpage
%*********** Equal Transitivity Rule **************
\display{"
begin math in theory system prime s lemma equal transitivity rule says all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r infer meta r peano is meta s infer meta t peano is meta s end lemma end math
end "}
"
begin math system prime s proof of equal transitivity rule reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a premise meta t peano is meta r end line line ell b premise meta r peano is meta s end line line ell c because equal transitivity indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end line because double mp prime modus ponens ell c modus ponens ell a modus ponens ell b indeed meta t peano is meta s qed end math
end "
\verb| | \\ \noindent
Beviset for dette regellemma bruger den samme teknik, som vi s\aa{} f\o{}rste gang i afsnit \ref{sec:condmpbevis}.
%*********** Equal Transitivity Conditioned Rule **************
\display{"
begin math in theory system prime s lemma equal transitivity conditioned rule says all meta a indeed all meta t indeed all meta r indeed all meta s indeed macro newline meta a peano imply meta t peano is meta r infer meta a peano imply meta r peano is meta s infer meta a peano imply meta t peano is meta s end lemma end math
end "
}
"
begin math system prime s proof of equal transitivity conditioned rule reads arbitrary meta a end line arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a premise meta a peano imply meta t peano is meta r end line line ell b premise meta a peano imply meta r peano is meta s end line line ell c because equal transitivity indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end line line ell q because weakening modus ponens ell c indeed meta a peano imply macro newline meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end line because double conditioned mp prime modus ponens ell q modus ponens ell a modus ponens ell b indeed meta a peano imply meta t peano is meta s qed end math
end "
\verb| | \\ \noindent
Vi viser et betinget regellemma som "
begin math equal transitivity conditioned rule end math
end " p\aa{} n\ae{}sten samme m\aa{}de, som vi viser et ubetinget regellemma. F\o{}rst skriver vi pr\ae{}misserne og moderlemmaet op. Derefter g\o{}r vi moderlemmaet betinget ved at bruge "
begin math weakening end math
end ". Til slut bruger vi "
begin math conditioned mp prime end math
end " \'{en} gang for hver pr\ae{}mis; dette giver os den \o{}nskede konklusion.
\newpage
%*********** Mendelson D (TUS) **************
\subsection{Bevis for "
begin math mendelson three two d end math
end " og heraf afledte lemmaer}
\label{sec:dbevis}
\display{
"
begin math in theory system prime s lemma mendelson 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 three two d reads arbitrary meta t end line arbitrary meta u end line arbitrary meta s end line line ell a because equal transitivity indeed meta t peano is meta u peano imply meta u peano is meta s peano imply meta t peano is meta s end line line ell b because permute antecedents modus ponens ell a indeed meta u peano is meta s peano imply meta t peano is meta u peano imply meta t peano is meta s end line line ell c because equal symmetry indeed meta s peano is meta u peano imply meta u peano is meta s end line line ell d because imply transitivity modus ponens ell c modus ponens ell b indeed meta s peano is meta u peano imply meta t peano is meta u peano imply meta t peano is meta s end line because permute antecedents modus ponens ell d indeed meta t peano is meta u peano imply meta s peano is meta u peano imply meta t peano is meta s qed end math
end "
%*** D tegning ***
%\newpage
\begin{picture}(200,250) % XY 200
%\graphpaper(0,0)(500,500)
\thicklines
\put(120,220){\framebox(100,20){\textbf{8}:${\cal TU} \mathrel{\dot{\Rightarrow}} {\cal SU} \mathrel{\dot{\Rightarrow}} {\cal TS}$}}
\put(110,200){PermuteAnts}
\put(120,160){\framebox(100,20){\textbf{7}:${\cal SU} \mathrel{\dot{\Rightarrow}} {\cal TU} \mathrel{\dot{\Rightarrow}} {\cal TS}$}}
\put(170,180){\vector( 0,1){40}}
\put(60,140){ImplyTransitivity}
\put(40,100){\framebox(100,20){\textbf{6}:${\cal SU} \mathrel{\dot{\Rightarrow}} {\cal US}$}}
\put(140,120){\vector( 0,1){40}}
\put(40,90){EqualSymmetry}
\put(200,100){\framebox(100,20){\textbf{5}:${\cal US} \mathrel{\dot{\Rightarrow}} {\cal TU} \mathrel{\dot{\Rightarrow}} {\cal TS}$} }
\put(200,120){\vector(0,1){40}}
\put(190,80){PermuteAnts}
\put(200,40){\framebox(100,20){\textbf{4}:${\cal TU} \mathrel{\dot{\Rightarrow}} {\cal US} \mathrel{\dot{\Rightarrow}} {\cal TS}$} }
\put(250,60){\vector(0,1){40}}
\put(200,30){EqualTransitivity}
\end{picture}
\newpage
%*********** Mendelson 32dRule **************
\display{"
begin math in theory system prime s lemma mendelson three two d rule says all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r infer meta s peano is meta r infer meta t peano is meta s end lemma end math
end "
}
"
begin math system prime s proof of mendelson three two d rule reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a premise meta t peano is meta r end line line ell b premise meta s peano is meta r end line line ell c because mendelson three two d indeed meta t peano is meta r peano imply meta s peano is meta r peano imply meta t peano is meta s end line because double mp prime modus ponens ell c modus ponens ell a modus ponens ell b indeed meta t peano is meta s qed end math
end "
\verb| | \\ \noindent
Beviset for dette regellemma bruger den samme teknik, som vi s\aa{} f\o{}rste gang i afsnit \ref{sec:condmpbevis}.
%\newpage
%*********** Mendelson 32dConditionedRule **************
\display{ "
begin math in theory system prime s lemma mendelson three two d conditioned rule says all meta a indeed all meta t indeed all meta r indeed all meta s indeed macro newline meta a peano imply meta t peano is meta r infer meta a peano imply meta s peano is meta r infer meta a peano imply meta t peano is meta s end lemma end math
end "
}
"
begin math system prime s proof of mendelson three two d conditioned rule reads arbitrary meta a end line arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a premise meta a peano imply meta t peano is meta r end line line ell b premise meta a peano imply meta s peano is meta r end line line ell c because mendelson three two d indeed meta t peano is meta r peano imply meta s peano is meta r peano imply meta t peano is meta s end line line ell q because weakening modus ponens ell c indeed meta a peano imply macro newline meta t peano is meta r peano imply meta s peano is meta r peano imply meta t peano is meta s end line because double conditioned mp prime modus ponens ell q modus ponens ell a modus ponens ell b indeed meta a peano imply meta t peano is meta s qed end math
end "
\verb| | \\ \noindent
Beviset for dette betingede regellemma bruger den samme teknik, som vi brugte til at vise "
begin math equal transitivity conditioned rule end math
end " i afsnit \ref{sec:equaltransbevis}.
%*********** Mendelson F base **************
\subsection{Bevis for "
begin math mendelson three two f end math
end "} \label{sec:fbevis}
\display{"
begin math in theory system prime s lemma mendelson three two f base says peano zero peano is peano zero peano plus peano zero end lemma end math
end "
}
"
begin math system prime s proof of mendelson three two f 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 c because equal symmetry rule modus ponens ell a indeed peano t peano is peano t peano plus peano zero end line because substitution macro at peano t at peano zero modus ponens ell c indeed peano zero peano is peano zero peano plus peano zero qed end math
end "
\verb| | \\ \noindent
Dette bevis illustrerer nytten af makroen "
begin math substitution macro end math
end ". Bem\ae{}rk i \o{}vrigt de to snabel-a'er i linie 3; deres form\aa{}l er at fort\ae{}lle Logiwebs bevischecker, at de to meta-variable "
begin math meta z end math
end " og "
begin math meta c end math
end " i "
begin math substitution macro end math
end " skal instantieres til hhv.\ \mbox{"
begin math peano t end math
end " og "
begin math peano zero end math
end ".} I skrivende stund kan Logiwebs bevischecker ikke selv n\aa{} frem til, hvordan "
begin math meta z end math
end " og "
begin math meta c end math
end " skal instantieres (fordi disse meta-variable kun optr\ae{}der i sidebetingelsen i "
begin math substitution macro end math
end ").
%*********** Mendelson F induktion (peano version) **************
\display{
"
begin math in theory system prime s lemma mendelson 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 "
}
"
begin math system prime s proof of mendelson three two f induction reads line ell a 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 b because axiom prime s six indeed peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell c because weakening modus ponens ell b 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 end line because mendelson three two d conditioned rule modus ponens ell a modus ponens ell c 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 "
\verb| | \\ \noindent
Jeg vil ikke illustrere dette bevis med et bevistr\ae{}; hele arbejdet g\o{}res med en anvendelse af "
begin math mendelson three two d conditioned rule end math
end " p\aa{} to aksiomer (hvoraf det ene er gjort betinget med "
begin math weakening end math
end ").
%*********** Mendelson F simpliciter **************
\display{
"
begin math in theory system prime s lemma mendelson 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 three two f reads line ell a because mendelson three two f base indeed peano zero peano is peano zero peano plus peano zero end line line ell b because mendelson 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 because induction macro modus ponens ell a modus ponens ell b indeed peano t peano is peano zero peano plus peano t qed end math
end "
\verb| | \\ \noindent
Som det kan ses, g\o{}r "
begin math induction macro end math
end " det meget enkelt at f\ae{}rdigg\o{}re et induktionsbevis.
\newpage
%*********** Mendelson G base **************
\subsection{Bevis for "
begin math mendelson three two g end math
end " og heraf afledt lemma}
\display{
"
begin math in theory system prime s lemma mendelson three two g base says peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end lemma end math
end "
}
"
begin math system prime s proof of mendelson three two g base reads line ell a because axiom prime s five indeed peano t peano succ peano plus peano zero peano is peano t peano succ end line line ell b because axiom prime s five indeed peano t peano plus peano zero peano is peano t end line line ell c because add one modus ponens ell b indeed parenthesis peano t peano plus peano zero end parenthesis peano succ peano is peano t peano succ end line because mendelson three two d rule modus ponens macro newline ell a modus ponens ell c indeed peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ qed end math
end "
%\newpage
%*** Gbase tegning ***
\begin{picture}(-120,0)(200,200) % XY (0,0)
%\graphpaper(0,0)(500,500)
\thicklines
\put(310,160){\framebox(90,20){\textbf{4}:$\mathit{t}' + 0 = (\mathit{t} + 0)'$}}
\put(280,140){Drule}
\put(240,100){\framebox(70,20){\textbf{1}:$\mathit{t}' + 0 = \mathit{t}'$}}
\put(310,120){\vector(0,1){40}}
\put(240,90){$\textrm{S5}'$}
\put(400,100){\framebox(70,20){\textbf{3}:$(\mathit{t} + 0)' = \mathit{t}'$}}
\put(400,120){\vector(0,1){40}}
\put(390,80){AddOne}
\put(400,40){\framebox(60,20){\textbf{2}:$\mathit{t} + 0 = \mathit{t}$}}
\put(430,60){\vector(0,1){40}}
\put(400,30){$\textrm{S5}'$}
\end{picture}
\newpage
%*********** Mendelson G induction **************
\display{
"
begin math in theory system prime s lemma mendelson three two g induction says macro newline peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end lemma end math
end "
}
"
begin math system prime s proof of mendelson three two g induction reads line ell a because axiom prime s two indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply macro newline parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end line line ell b because axiom prime s six indeed peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ end line line ell c because weakening modus ponens ell b indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply macro newline peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ end line line ell d because equal transitivity conditioned rule modus ponens ell c modus ponens ell a indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply macro newline peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end line line ell e 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 f because add one modus ponens ell e indeed parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end line line ell g because weakening modus ponens ell f indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply macro newline parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ end line because mendelson three two d conditioned rule modus ponens ell d modus ponens ell g indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply macro newline peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ qed end math
end "
%\newpage
%*** Gindu tegning ***
\scalebox{0.85}[1]{
\begin{picture}(40,50)(200,300) % XY
%\graphpaper(0,0)(600,500)
\thicklines
\put(310,280){\framebox(165,20){\textbf{8}:$\mathit{t}' + \mathit{r} \mathop{=} (\mathit{t} + \mathit{r})' \mathrel{\dot{\Rightarrow}} \mathit{t}' + \mathit{r}' \mathop{=} (\mathit{t} + \mathit{r}')'$}}
\put(255,260){DCondRule}
\put(210,220){\framebox(170,20){\textbf{4}:$\mathit{t}' + \mathit{r} \mathop{=} (\mathit{t} + \mathit{r})' \mathrel{\dot{\Rightarrow}} \mathit{t}' + \mathit{r}' \mathop{=} (\mathit{t} + \mathit{r})''$}}
% DOUBLESUCC
\put(310,240){\vector( 0,1){40}}
\put(215,200){EqualTransitivityCondRule}
\put(380,100){\framebox(180,20){\textbf{1}:$\mathit{t}' + \mathit{r} \mathop{=} (\mathit{t} + \mathit{r})' \mathrel{\dot{\Rightarrow}} (\mathit{t}' + \mathit{r})' \mathop{=} (\mathit{t} + \mathit{r})''$}}
\put(380,90){$\textrm{S2}'$}
\put(380,120){\vector( 0,1){100}}
\put(180,160){\framebox(180,20){\textbf{2--3}:$\mathit{t}' + \mathit{r} \mathop{=} (\mathit{t} + \mathit{r})' \mathrel{\dot{\Rightarrow}} \mathit{t}' + \mathit{r}' \mathop{=} (\mathit{t}' + \mathit{r})'$}}
% DOUBLESUCC
\put(180,150){$\textrm{S6}'$-W}
\put(340,180){\vector( 0,1){40}}
\put(400,220){\framebox(190,20){\textbf{6--7}:$\mathit{t}' + \mathit{r} \mathop{=} (\mathit{t} + \mathit{r})' \mathrel{\dot{\Rightarrow}} (\mathit{t} + \mathit{r}')' \mathop{=} (\mathit{t} + \mathit{r})'' $}}
% DOUBLESUCC
\put(475,240){\vector(0,1){40}}
\put(445,200){AddOne-W}
\put(450,160){\framebox(80,20){\textbf{5}:$\mathit{t} + \mathit{r}' \mathop{=} (\mathit{t} + \mathit{r})'$}}
\put(500,180){\vector(0,1){40}}
\put(450,150){$\textrm{S6}'$}
\end{picture}
}
\newpage
%*********** Mendelson G simpliciter **************
\display{
"
begin math in theory system prime s lemma mendelson three two g says peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end lemma end math
end "
}
"
begin math system prime s proof of mendelson three two g reads line ell a because mendelson three two g base indeed peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end line line ell b because mendelson three two g induction indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply macro newline peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end line because induction macro modus ponens ell a modus ponens ell b indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ qed end math
end "
\begin{sloppypar}
\verb| | \\ \noindent
Ligesom i afsnit \ref{sec:fbevis} har vi her f\ae{}rdiggjort induktionsbeviset ved hj\ae{}lp af "
begin math induction macro end math
end ".
\end{sloppypar}
%*********** Mendelson32gRTswitch **************
\display{
"
begin math in theory system prime s lemma mendelson three two g rt switch 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 three two g rt switch reads line ell a because mendelson three two g indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell b because substitution macro at peano t at peano s modus ponens ell a indeed peano s peano succ peano plus peano r peano is parenthesis peano s peano plus peano r end parenthesis peano succ end line line ell c because substitution macro at peano r at peano t modus ponens ell b indeed peano s peano succ peano plus peano t peano is parenthesis peano s peano plus peano t end parenthesis peano succ end line because substitution macro at peano s at peano r modus ponens ell c 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 "
\verb| | \\ \noindent
Som det kan ses, er det ganske enkelt at bytte om p\aa{} variabelnavnene i et lemma som "
begin math mendelson three two g end math
end ", n\aa{}r vi f\o{}rst har makroen "
begin math substitution macro end math
end " til r\aa{}dighed. Det eneste raffinement er, at vi m\aa{} introducere en hj\ae{}lpevariabel "
begin math peano s end math
end ": Hvis vi f.eks.\ havde konkluderet "
begin math peano r peano succ peano plus peano r peano is parenthesis peano r peano plus peano r end parenthesis peano succ end math
end " i linie 2, ville vi ikke l\ae{}ngere kunne udtrykke, at lemmaet g\ae{}lder for to forskellige variable.
%\newpage
%******** Plus commutativity base **************
\subsection{Bevis for "
begin math plus commutativity end math
end " }
\display{"
begin math in theory system prime s lemma plus commutativity base says peano t peano plus peano zero peano is peano zero peano plus peano t end lemma end math
end "
}
"
begin math system prime s proof of plus commutativity 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 three two f indeed peano t peano is peano zero peano plus peano t end line because equal transitivity rule modus ponens macro newline ell a modus ponens ell b indeed peano t peano plus peano zero peano is peano zero peano plus peano t qed end math
end "
\begin{sloppypar}
\verb| | \\ \noindent
Vi har udelukkende vist "
begin math mendelson three two f end math
end " for at kunne bruge det i dette bevis; men som det ses, har vi heller ikke brug for meget mere for at vise "
begin math plus commutativity base end math
end ".
\end{sloppypar}
\newpage
%********* Plus commutativity induktion ***********
\display{"
begin math in theory system prime s lemma plus commutativity 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 "
}
"
begin math system prime s proof of plus commutativity induction reads line ell a because axiom prime s two indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply macro newline 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 b because axiom prime s six indeed peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell c because weakening modus ponens ell b indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply macro newline 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 f because equal transitivity conditioned rule modus ponens ell c modus ponens ell a indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply macro newline 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 d because mendelson three two g rt switch 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 e because weakening modus ponens ell d indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply macro newline peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line because mendelson three two d conditioned rule modus ponens ell f 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 peano r peano succ peano plus peano t qed end math
end "
%\newpage
\scalebox{0.9}[1]{
\begin{picture}(120,50)(200,300)
%\graphpaper(0,0)(600,500)
\thicklines
\put(325,280){\framebox(140,20){\textbf{7}:$\mathit{t} + \mathit{r} \mathop{=} \mathit{r} + \mathit{t} \mathrel{\dot{\Rightarrow}} \mathit{t} + \mathit{r}' \mathop{=} \mathit{r}' + \mathit{t}$}}
\put(320,260){DCondRule}
\put(225,220){\framebox(150,20){\textbf{4}:$\mathit{t} + \mathit{r} \mathop{=} \mathit{r} + \mathit{t} \mathrel{\dot{\Rightarrow}} \mathit{t} + \mathit{r}' \mathop{=} (\mathit{r} + \mathit{t})'$}}
\put(375,240){\vector( 0,1){40}}
\put(250,200){EqualTransitivityCondRule}
\put(175,120){\framebox(155,20){\textbf{2-3}:$\mathit{t} + \mathit{r} \mathop{=} \mathit{r} + \mathit{t} \mathrel{\dot{\Rightarrow}} \mathit{t} + \mathit{r}' \mathop{=} (\mathit{t} + \mathit{r})'$}}
\put(245,140){\vector(0,1){80}}
\put(175,110){$\textrm{S6}'$-W}
\put(345,120){\framebox(155,20){\textbf{1}:$\mathit{t} + \mathit{r} \mathop{=} \mathit{r} + \mathit{t} \mathrel{\dot{\Rightarrow}} (\mathit{t} + \mathit{r})' \mathop{=} (\mathit{r} + \mathit{t})'$}}
\put(375,140){\vector(0,1){80}}
\put(345,110){$\textrm{S2}'$}
%\put(350,120){\framebox(155,20){\textbf{2-3}:$\mathit{t} + \mathit{r} \mathop{=} \mathit{r} + \mathit{t} %\mathrel{\dot{\Rightarrow}} \mathit{t} + \mathit{r}' \mathop{=} (\mathit{t} + \mathit{r})'$}}
%\put(380,140){\vector(0,1){80}}
%\put(350,110){$\textrm{S6}'$-W}
\put(405,220){\framebox(155,20){\textbf{5-6}:$\mathit{t} + \mathit{r} \mathop{=} \mathit{r} + \mathit{t} \mathrel{\dot{\Rightarrow}} \mathit{r}' + \mathit{t} \mathop{=} (\mathit{r} + \mathit{t})' $}}
\put(405,240){\vector(0,1){40}}
\put(405,210){Gswitch-W}
\end{picture}
}
\newpage
%*********** Plus Commutativity simpliciter **************
\display{"
begin math in theory system prime s lemma plus commutativity says peano t peano plus peano r peano is peano r peano plus peano t end lemma end math
end "
}
\begin{sloppypar}
"
begin math system prime s proof of plus commutativity reads line ell a because plus commutativity base indeed peano t peano plus peano zero peano is peano zero peano plus peano t end line line ell b because plus commutativity 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 because induction macro modus ponens ell a modus ponens ell b indeed peano t peano plus peano r peano is peano r peano plus peano t qed end math
end "
\end{sloppypar}
\verb| | \\ \noindent
Den sidste af de 28 hj\ae{}lpes\ae{}tninger vises alts\aa{} ved en simpel anvendelse af "
begin math induction macro end math
end ". Hermed er det lovede bevis for s\ae{}tning (\ref{eq:com}) f\ae{}rdiggjort.
%\newpage
\appendix
\section{Navnet p\aa{} dette dokument} \label{sec:navn}
Den f\o{}lgende definition fastl\ae{}gger dette dokuments Logiweb-navn:
"
begin math pyk define peano commutativity as "peano commutativity" end define end math
end "
\section{\TeX{} definitioner} \label{sec:texdefinitioner}
\display{"
begin math tex define weakening as "Weakening" end define end math
end "}
\display{"
begin math tex define double mp prime as "DoubleMP'" end define end math
end "}
\display{"
begin math tex define conditioned mp prime as "ConditionedMP'" end define end math
end "}
\display{"
begin math tex define double conditioned mp prime as "DoubleConditionedMP'" end define end math
end "}
\display{"
begin math tex define imply transitivity as "ImplyTransitivity" end define end math
end "}
\display{"
begin math tex define permute antecedents as "PermuteAntecedents" end define end math
end "}
\display{"
begin math tex define add one as "AddOne" end define end math
end "}
\display{"
begin math tex define substitution macro as "SubstitutionMacro" end define end math
end "}
\display{"
begin math tex define induction macro as "InductionMacro" end define end math
end "}
\display{"
begin math tex define equal reflexivity as "EqualReflexivity" end define end math
end "}
\display{"
begin math tex define equal symmetry as "EqualSymmetry" end define end math
end "}
\display{"
begin math tex define equal symmetry rule as "EqualSymmetryRule" end define end math
end "}
\display{"
begin math tex define equal transitivity as "EqualTransitivity" end define end math
end "}
\display{"
begin math tex define equal transitivity rule as "EqualTransitivityRule" end define end math
end "}
\display{"
begin math tex define equal transitivity conditioned rule as "EqualTransitivityCondRule" end define end math
end "}
\display{"
begin math tex define mendelson three two d as "Mendelson3.2(d)" end define end math
end "}
\display{"
begin math tex define mendelson three two d rule as "Mendelson3.2(d)Rule" end define end math
end "}
\display{"
begin math tex define mendelson three two d conditioned rule as "Mendelson3.2(d)CondRule" end define end math
end "}
\display{"
begin math tex define mendelson three two f base as "Mendelson3.2(f)Base" end define end math
end "}
\display{"
begin math tex define mendelson three two f induction as "Mendelson3.2(f)Indu" end define end math
end "}
\display{"
begin math tex define mendelson three two f as "Mendelson3.2(f)" end define end math
end "}
\display{"
begin math tex define mendelson three two g base as "Mendelson3.2(g)Base" end define end math
end "}
\display{"
begin math tex define mendelson three two g induction as "Mendelson3.2(g)Indu" end define end math
end "}
\display{"
begin math tex define mendelson three two g as "Mendelson3.2(g)" end define end math
end "}
\display{"
begin math tex define mendelson three two g rt switch as "Mendelson3.2(g)Switch" end define end math
end "}
\display{"
begin math tex define plus commutativity base as "PlusCommutativityBase" end define end math
end "}
\display{"
begin math tex define plus commutativity induction as "PlusCommutativityIndu" end define end math
end "}
\display{"
begin math tex define plus commutativity as "PlusCommutativity" end define end math
end "}
\section{Litteratur}
\bibliography{/net/urd/home/disk15/eriksen/.logiweb/peano-commutativity/page}
\end{document}
End of file
latex page
bibtex page
latex page
latex page"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,