"File page.tex
\documentclass [fleqn]{article}
\setlength {\overfullrule }{1mm}
\input{lgwinclude}
\usepackage{latexsym}
%\setlength{\parindent}{0em}
%\setlength{\parskip}{1ex}
% The font of each Logiweb construct is under tight control except that
% strings are typeset in whatever font is in effect at the time of
% typesetting. This is done to enhance the readability of strings in the
% TeX source generated by Logiweb. The default font for typesetting
% strings is \rm:
\everymath{\rm}
\usepackage{makeidx}
\usepackage{page}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
\newlength{\bracketwidth}
\settowidth{\bracketwidth}{$[{}$}
\newcommand{\back}{\protect\makebox[-1.0\bracketwidth]{}}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
\hypersetup{pdftitle=Introduction to Logiweb}
\hypersetup{colorlinks=true}
\bibliographystyle{plain}
% \tex{something} writes something to page.otx for later inclusion
\newwrite\outex
\newtoks\toktex
\immediate\openout\outex=page.otx
\newcommand{\tex}[1]{\toktex={\item #1}\immediate\write\outex{\the\toktex}}
% \test{something} writes something to page.tst for later inclusion
\newwrite\outest
\immediate\openout\outest=page.tst
\newcommand{\test}[1]{\toktex={\item #1}\immediate\write\outest{\the\toktex}}
% Concerning \catcode`\@=11 : See the TeXbook, Appendix B (page 344).
% \afterheading suppresses indentation once, c.f. latex.ltx.
% \display{something} displays something as a displayed equation except
% that linebreaking is possible and displaymath is not turned on by default.
% The first paragraph after \display{something} is unindented.
% Glue below formulas may be wrong. The definition of \display misses
% something like \addvspace{\belowdisplayskip}.
\catcode`\@=11
\def\afterheading{\@afterheading}
\catcode`\@=12
\newcommand{\display}[1]{\begin{list}{}{\setlength{\leftmargin}{\mathindent}}
\item #1\end{list}
\afterheading}
\newcommand{\statement}[1]{\begin{list}{}{\setlength{\leftmargin}{0mm}}
\item #1\end{list}
\afterheading}
\begin {document}
\title {Formelt bevis for kummutativitet af addition under Peanos axiomer}
\author {Anders Vaaben Andersen}
\maketitle
\tableofcontents
"
begin ragged right
end "
\section{Indledning}
F\o lgende er en besvarelse af rapport opgaven p\aa \space logik kurset ved DIKU for\aa ret 2005 udarbejdet af Anders Vaaben Andersen.
Sigtet med opgaven er at f\o re l\ae seren gennem et bevis for
"
begin bracket var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var end bracket
end " med udgangspunkt i Peanos axiomer.
Det er tilstr\ae bt at rapporten kan l\ae ses uden st\o rre forh\aa ndskendskab til formel bevisf\o relse, dog forventes et kendskab til de
logiske symboler, samt kendskab til begreberne frie og bundne variable.
Beviset er produceret i pyk sproget hvilket har muliggjort en maskinel kontrol af bevisets korrekthed og er publiceret p\aa \space DIKUS
lokale logiweb system. Fra webadressen
http://www.diku.dk/~grue/logiweb/20050502/home/vaaben/proofreport/latest/
kan man hente denne rapport b\aa de som
pyk kildetekst, som LaTeX fil, som dvi eller som pdf. Yderligere kan man p\aa \space den ovenst\aa ende URL se at Logiweb siden er godkendt.
Siden er baseret p\aa den oprindelige 'Peano' side af Klaus Grue og alle dens konstruktioner er inkluderet direkte p\aa siden. Denne side kan findes p\aa \space
http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/GRD-2005-06-22-UTC-07-23-31-271829/
Fokus vil prim\ae rt v\ae re p\aa \space hvorledes et formelt bevis forl\o ber samt metoder til at undg\aa \space at beviserne bliver for store og uoverskuelige. Der vil undervejs blive
refereret til s\ae tninger fra \cite{Mendelson} desuden vil beviserne i hovedtr\ae k v\ae re f\o rt p\aa \space samme m\aa de.
\section{Logiweb}
Kort fortalt er Logiweb \cite{logiweb} et system til at publicere sider med matematisk indhold, hvor korrektheden af det matematiske indhold bliver kontrolleret af Logiweb serveren.
En Logiweb side starter som en pyk kildetekst, der indeholder f\o lgende elementer:
\begin{itemize}
\item PAGE, som definerer sidens navn.
\item BIBLIOGRAPHY, referencer til andre Logiweb sider, hvorfra pyk konstruktioner importeres.
\item PREASSOCIATIVE/POSTASSOCIATIVE der bestemmer associativitets regler samt hvilke konstruktioner, der skal importeres fra siderne i bibliografien.
\item BODY indeholder kroppen af en TeX fil med pyk konstruktioner indlejret.
\end{itemize}
Pyk konstruktionerne bliver dels oversat til et bin\ae rt format der kan l\ae ses af logiweb serveren og dels oversat til TeX.
Den bin\ae re version bruges til at checke sidens korrekthed, mens TeX versionen automatisk bliver oversat til dvi og pdf n\aa r pyk compileren er f\ae rdig.
Noget egentligt kendskab til Logiweb foruds\ae ttes ikke i det f\o lgende da pyk compileren i samarbejde med TeX producerer l\ae selig matematisk notation.
S\aa fremt l\ae seren har et \o nske om at tilegne sig yderligere kendskab til logiweb systemet kan hevises til base page som denne rapports Logiweb side inkluderer
(http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/latest/).
Alternativt kan man
hente kildeteksten fra den URL, der blev n\ae vnt i indledningen. Hvis man allerede er fortrolig med TeXs syntaks burde det v\ae re nemt at identificere de dele der bliver fortolket af pyk
kompileren. De forskellige centrale pyk konstruktioner kan desuden ses i fodnoterne efterh\aa nden som de bliver introduceret mens appendix A indeholder alle de knap s\aa \space centrale.
\section{Peano aritmetik}
Som n\ae vnt indledningsvis vil rapporten gennemg\aa \space
et formelt bevis for s\ae tningen
"
begin bracket peano all var x peano var indeed peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var end bracket
end ". Peanos axiomer
der vil blive benyttet som udgangspunkt for beviset er en axiomatisering af de naturlige tal samt symbolerne plus, gange og lighed. P\aa \space et intuitivt
plan er axiomerne oplagt sande udsagn om de naturlige tal, men hvad der er knap s\aa \space
oplagt er at de medf\o rer grundl\ae ggende egenskaber som associativitet, distributivitet og
den egenskab som vil blive vist i det f\o lgende: kommutativitet.
Hvor man i de fleste matematiske tekster vil undlade detaljer der m\aa \space betragtes som indlysende vil beviset i det efterf\o lgende v\ae re udpenslet s\aa ledes at enhvert argument
kan spores tilbage til axiomerne. Hovedmotivationen for axiomatisering og formel logik har netop v\ae ret at give matematik et s\aa \space solidt grundlag at intet var overladt til intuition, samt undg\aa
de paradokser der opstod af et for l\o st matematisk fundament.
\subsection{Symboler i Peano aritmetik}
\subsubsection{Termer}
Termer er opbygget af f\o lgende symboler:
\begin{itemize}
\item Variable, der repr\ae senteres af de sm\aa \space bogstaver fra det engelske alfabet: "
begin bracket var a peano var end bracket
end " - "
begin bracket var z peano var end bracket
end ". "
begin math define pyk of peano zero as text "peano zero" end text end define end math
then math define tex of peano zero as text "
\dot{0}" end text end define end math
end " svarer til symbolet nul. Alle andre tal defineres induktivt som efterf\o lgere "
begin math define pyk of var x peano succ as text "* peano succ" end text end define end math
then math define tex of var x peano succ as text "#1.'" end text end define end math
end ", af hinanden.
\item Derudover kan termer indeholde plus "
begin math define pyk of var x peano plus var y as text "* peano plus *" end text end define end math
then math define tex of var x peano plus var y as text "#1.
\mathop{\dot{+}} #2." end text end define end math
end "
\item Gange
"
begin math define pyk of var x peano times var y as text "* peano times *" end text end define end math
then math define tex of var x peano times var y as text "#1.
\mathop{\dot{\cdot}} #2." end text end define end math
end ".
\end{itemize}
\subsubsection{Formularer}
Formularer er opbygget af:
\begin{itemize}
\item Lighed "
begin math define pyk of var x peano is var y as text "* peano is *" end text end define end math
then math define tex of var x peano is var y as text "#1.
\stackrel{p}{=} #2." end text end define end math
end " mellem termer.
\item Negation "
begin math define pyk of peano not var x as text "peano not *" end text end define end math
then math define tex of peano not var x as text "
\dot{\neg}\, #1." end text end define end math
end " af en formular
\item Implikation "
begin math define pyk of var x peano imply var y as text "* peano imply *" end text end define end math
then math define tex of var x peano imply var y as text "#1.
\mathrel{\dot{\Rightarrow}} #2." end text end define end math
end " mellem formularer.
\item universel kvantifisering "
begin math define pyk of peano all var x indeed var y as text "peano all * indeed *" end text end define end math
then math define tex of peano all var x indeed var y as text "
\dot{\forall} #1.
\colon #2." end text end define end math
end " af en formular.
\end{itemize}
Bem\ae rk at implikation i det f\o lgende er h\o jre associativ modsat konventionen i Mendelson.
\subsubsection{Andre symboler}
Derudover kan f\o lgende almindeligt kendte symboler umiddelbart defineres udfra de ovenst\aa ende:
\begin{itemize}
\item Een: "
begin math define pyk of peano one as text "peano one" end text end define end math
then math define tex of peano one as text "
\dot{1}" end text end define end math
end " som \display{"
begin math define macro of peano one as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano one as peano zero peano succ end define end quote end define end define end math
end "}
\item To: "
begin math define pyk of peano two as text "peano two" end text end define end math
then math define tex of peano two as text "
\dot{2}" end text end define end math
end " som \display{"
begin math define macro of peano two as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano two as peano one peano succ end define end quote end define end define end math
end "}
\item Logisk og: "
begin math define pyk of var x peano and var y as text "* peano and *" end text end define end math
then math define tex of var x peano and var y as text "#1.
\mathrel{\dot{\wedge}} #2." end text end define end math
end " som \display{"
begin math define macro of var x peano and var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x peano and var y as peano not parenthesis var x peano imply peano not var y end parenthesis end define end quote end define end define end math
end "}
\item Logisk eller: "
begin math define pyk of var x peano or var y as text "* peano or *" end text end define end math
then math define tex of var x peano or var y as text "#1.
\mathrel{\dot{\vee}} #2." end text end define end math
end " som \display{"
begin math define macro of var x peano or var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x peano or var y as peano not var x peano imply var y end define end quote end define end define end math
end "}
\item Biimplikation: "
begin math define pyk of var x peano iff var y as text "* peano iff *" end text end define end math
then math define tex of var x peano iff var y as text "#1.
\mathrel{\dot{\Leftrightarrow}} #2." end text end define end math
end " som \display{"
begin math define macro of var x peano iff var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x peano iff var y as parenthesis var x peano imply var y end parenthesis peano and parenthesis var y peano imply var x end parenthesis end define end quote end define end define end math
end "}
\item Eksistens: "
begin math define pyk of peano exist var x indeed var y as text "peano exist * indeed *" end text end define end math
then math define tex of peano exist var x indeed var y as text "
\dot{\exists} #1.
\colon #2." end text end define end math
end " som \display{"
begin math define macro of peano exist var x indeed var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano exist var x indeed var y as peano not peano all var x indeed peano not var y end define end quote end define end define end math
end "}
\end{itemize}
Symbolerne er defineret som makroer, dvs pyk compileren erstatter dem med definition f\o r siden bliver kontrolleret. Jeg har dog valgt udelukkende at holde mig til de oprindelige symboler da jeg synes
det g\o r det v\ae sentligt nemmere at overskue korrektheden af et bevis end n\aa r forskellige symboler d\ae kker over helt \ae kvivalente udsagn.
Det skal bem\ae rkes at hvor Mendelson skelner i sin notation mellem termer og formularer, s\aa \space er der i den underliggendende pyk implementation for denne rapport benyttet s\aa kaldte metavariable til b\aa de termer og formularer.
Dog kan man altid udlede af konteksten hvad et symbol repr\ae senterer s\aa \space det burde ikke skabe forvirring.
\subsection{Axiomer}
Axiomerne er det fundament hvoraf s\ae tningerne i en teori kan opbygges. L\o st sagt kan man beskrive dem som de 'grundantagelser' der er n\o dvendige f\o r man kan drage konklusioner om noget som helst.
Peano aritmetikken best\aa r af 14 axiomer samt 2 slutningsregler, hvoraf de 5 f\o rste axiomer er de logiske axiomer, der er f\ae lles for alle f\o rste ordens teorier, mens de 9 '\ae gte' axiomer er specifikke
for Peano aritmetik.
System "
begin math define pyk of system prime s as text "system prime s" end text end define end math
then math define tex of system prime s as text "
S'" end text end define end math
end " \display{"
begin math define statement of system prime s as all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano plus metavar var b end metavar peano succ peano is metavar var a end metavar peano plus metavar var b end metavar peano succ rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano succ peano is metavar var b end metavar peano succ peano imply metavar var a end metavar peano is metavar var b end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar rule plus all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed peano nonfree quote metavar var x end metavar end quote in quote metavar var a end metavar end quote end nonfree endorse peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano all metavar var x end metavar indeed metavar var b end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano times metavar var b end metavar peano succ peano is metavar var a end metavar peano times metavar var b end metavar peano plus metavar var a end metavar rule plus all metavar var a end metavar indeed metavar var a end metavar peano plus peano zero peano is metavar var a end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var x end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var x end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var x end metavar is metavar var x end metavar peano succ end sub endorse metavar var b end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar rule plus all metavar var a end metavar indeed not peano zero peano is metavar var a end metavar peano succ rule plus all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer peano all metavar var x end metavar indeed metavar var a end metavar rule plus all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse peano all metavar var x end metavar indeed metavar var b end metavar peano imply metavar var a end metavar rule plus all metavar var a end metavar indeed metavar var a end metavar peano times peano zero peano is peano zero end define end math
end "}
\subsubsection{De logiske axiomer}
De logiske axiomer besk\ae ftiger sig ikke med termer men udelukkende med sammenh\ae nge mellem formularer. A1 - A3 er de grundl\ae ggende for formelle teorier, mens A4-A5 yderligere fastl\ae gger
en f\o rste ordens teori.
"
begin math define pyk of axiom prime a one as text "axiom prime a one" end text end define end math
then math define tex of axiom prime a one as text "
A1'" end text end define end math
end ",
"
begin math define pyk of axiom prime a two as text "axiom prime a two" end text end define end math
then math define tex of axiom prime a two as text "
A2'" end text end define end math
end ",
"
begin math define pyk of axiom prime a three as text "axiom prime a three" end text end define end math
then math define tex of axiom prime a three as text "
A3'" end text end define end math
end ",
"
begin math define pyk of axiom prime a four as text "axiom prime a four" end text end define end math
then math define tex of axiom prime a four as text "
A4'" end text end define end math
end ", og
"
begin math define pyk of axiom prime a five as text "axiom prime a five" end text end define end math
then math define tex of axiom prime a five as text "
A5'" end text end define end math
end "
\display{"
begin math define statement of axiom prime a one as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end define
then define proof of axiom prime a one as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a two as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define
then define proof of axiom prime a two as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a three as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end define
then define proof of axiom prime a three as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a four as system prime s infer all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse peano all metavar var x end metavar indeed metavar var b end metavar peano imply metavar var a end metavar end define
then define proof of axiom prime a four as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a five as system prime s infer all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed peano nonfree quote metavar var x end metavar end quote in quote metavar var a end metavar end quote end nonfree endorse peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano all metavar var x end metavar indeed metavar var b end metavar end define
then define proof of axiom prime a five as rule tactic end define end math
end "}
B\aa de axiom A4 og A5 har sidebetingelser for deres anvendelse. A4s sidebetingelse kr\ae ver at "
begin bracket metavar var c end metavar end bracket
end " er fri for "
begin bracket metavar var x end metavar end bracket
end " i "
begin bracket metavar var b end metavar end bracket
end ".
"
begin bracket metavar var x end metavar end bracket
end " kan eventuelt v\ae re lig "
begin bracket metavar var c end metavar end bracket
end "
A5s sidebetingelser er at der ikke findes nogen frie forekomster af "
begin bracket metavar var x end metavar end bracket
end " i "
begin bracket metavar var a end metavar end bracket
end ".
\subsubsection{Slutningsregler}
De to slutningsregler Peano aritmetik er:
"
begin math define pyk of rule prime mp as text "rule prime mp" end text end define end math
then math define tex of rule prime mp as text "
MP'" end text end define end math
end " og
"
begin math define pyk of rule prime gen as text "rule prime gen" end text end define end math
then math define tex of rule prime gen as text "
Gen'" end text end define end math
end "
\display{"
begin math define statement of rule prime mp as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar end define
then define proof of rule prime mp as rule tactic end define end math
end "}
\display{"
begin math define statement of rule prime gen as system prime s infer all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer peano all metavar var x end metavar indeed metavar var a end metavar end define
then define proof of rule prime gen as rule tactic end define end math
end "}
Bem\ae rk at begge regler benytter symbolet $\vdash{}$. Symbolet betyder at det der st\aa r efter det sidste $\vdash$ symbol kan konkluderes hvis man allerede har vist de
formularer, der st\aa r foran $\vdash$ symbolerne. Intuitivt svarer det til symbolet $\mathrel{\dot{\Rightarrow}}$ men med den afg\o rende forskel at $\mathrel{\dot{\Rightarrow}}$ er et symbol i Peano sproget
mens $\vdash$ betyder at det er en foruds\ae tning der skal v\ae re opfyldt f\o r man kan bruge en s\ae tningen eller reglen. Modus ponens der er den prim\ae re logiske slutningsregel g\o r
os i stand til at slutte "
begin bracket metavar var b end metavar end bracket
end " n\aa r man allerede har vist "
begin bracket metavar var a end metavar peano imply metavar var b end metavar end bracket
end " hvis man allerede har vist "
begin bracket metavar var a end metavar end bracket
end ".
Jeg vil senere komme ind p\aa \space hvorledes man kan konstruere et bevis for at "
begin bracket metavar var a end metavar peano imply metavar var b end metavar end bracket
end " n\aa r man har et bevis for "
begin bracket metavar var a end metavar infer metavar var b end metavar end bracket
end ".
I det f\o lgende vil jeg betegne det der st\aa r foran $\vdash$ som en 'foruds\ae tning', mens jeg vil betegne det der st\aa r foran $\mathrel{\dot{\Rightarrow}}$ som en 'hypotese'. Desuden vil
jeg for s\ae tninger med flere hypoteser ( f.eks "
begin bracket metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar end bracket
end " ) betegne hypotesen l\ae ngst til venstre som den f\o rste eller forreste mens jeg for
foruds\ae tninger vil betegne foruds\ae tningen l\ae ngst til h\o jre som den f\o rste eller forreste.
\subsubsection{De \ae gte axiomer}
De sidste 9 axiomer er regneregler, der fastl\ae gger egenskaberne for plus, gange og lighed. Axiomerne der er valgt afviger en smule fra dem, der er beskrevet i Mendelson idet
Mendelsons axiomer udtaler sig om forhold mellem variable mens disse axiomer udtaler sig om forhold mellem termer. De to axiomss\ae t er dog fuldst\ae ndigt \ae kvivalente og kan
hver is\ae r nemt udledes fra det andet.
Bem\ae rk det sidste og meget centrale axiom. Det er dette axiom, der tillader induktionsbeviser, hvilket bliver essentielt i de tre store afsluttende s\ae tninger fra Mendelson.
"
begin math define pyk of axiom prime s one as text "axiom prime s one" end text end define end math
then math define tex of axiom prime s one as text "
S1'" end text end define end math
end ",
"
begin math define pyk of axiom prime s two as text "axiom prime s two" end text end define end math
then math define tex of axiom prime s two as text "
S2'" end text end define end math
end ",
"
begin math define pyk of axiom prime s three as text "axiom prime s three" end text end define end math
then math define tex of axiom prime s three as text "
S3'" end text end define end math
end ",
"
begin math define pyk of axiom prime s four as text "axiom prime s four" end text end define end math
then math define tex of axiom prime s four as text "
S4'" end text end define end math
end ",
"
begin math define pyk of axiom prime s five as text "axiom prime s five" end text end define end math
then math define tex of axiom prime s five as text "
S5'" end text end define end math
end ",
"
begin math define pyk of axiom prime s six as text "axiom prime s six" end text end define end math
then math define tex of axiom prime s six as text "
S6'" end text end define end math
end ",
"
begin math define pyk of axiom prime s seven as text "axiom prime s seven" end text end define end math
then math define tex of axiom prime s seven as text "
S7'" end text end define end math
end ",
"
begin math define pyk of axiom prime s eight as text "axiom prime s eight" end text end define end math
then math define tex of axiom prime s eight as text "
S8'" end text end define end math
end ",
"
begin math define pyk of axiom prime s nine as text "axiom prime s nine" end text end define end math
then math define tex of axiom prime s nine as text "
S9'" end text end define end math
end ".
\display{"
begin math define statement of axiom prime s one as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar end define
then define proof of axiom prime s one as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s two as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ end define
then define proof of axiom prime s two as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s three as system prime s infer all metavar var a end metavar indeed not peano zero peano is metavar var a end metavar peano succ end define
then define proof of axiom prime s three as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s four as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano succ peano is metavar var b end metavar peano succ peano imply metavar var a end metavar peano is metavar var b end metavar end define
then define proof of axiom prime s four as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s five as system prime s infer all metavar var a end metavar indeed metavar var a end metavar peano plus peano zero peano is metavar var a end metavar end define
then define proof of axiom prime s five as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s six as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano plus metavar var b end metavar peano succ peano is metavar var a end metavar peano plus metavar var b end metavar peano succ end define
then define proof of axiom prime s six as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s seven as system prime s infer all metavar var a end metavar indeed metavar var a end metavar peano times peano zero peano is peano zero end define
then define proof of axiom prime s seven as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s eight as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano times metavar var b end metavar peano succ peano is metavar var a end metavar peano times metavar var b end metavar peano plus metavar var a end metavar end define
then define proof of axiom prime s eight as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s nine as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var x end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var x end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var x end metavar is metavar var x end metavar peano succ end sub endorse metavar var b end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar end define
then define proof of axiom prime s nine as rule tactic end define end math
end "}
\section{S\ae tninger}
Som n\ae vnt indledningsvis vil beviset blive f\o rt fra bar bund. Dvs de eneste linjer der kan bruges i beviset er axiomer, slutningsregler eller s\ae tninger, der er bevist p\aa \space denne logiweb side.
Jeg vil i nogle tilf\ae lde pr\ae sentere beviserne i omvendt r\ae kkef\o lge s\aa ledes at man p\aa \space forh\aa nd kan se at de enkelte lemmaer tjener et form\aa l.
I hovedtr\ae k vil beviserne f\o lge de beviser, der er beskrevet i Mendelson, men specielt i forbindelse med brug af s\ae tning 2.5 (Deduktions s\ae tningen) vil der blive foretaget nogle afvigelser.
Indledningsvis vil jeg dog bevise nogle helt grundl\ae ggende egenskaber ved Peano aritmetik. Det allerf\o rste resultat der skal vises er f\o lgende:
\subsection{Mendelson Lemma 3.2 (a)}
"
begin math define pyk of lemma prime l three two a as text "lemma prime l three two a" end text end define end math
then math define tex of lemma prime l three two a as text "L3.2(a)'" end text end define end math
end "
Det f\o rste bevis stammer fra den oprindelige Peano side og da beviset er rimeligt simpelt er det en god introduktion til hvordan et formelt bevis ser ud:
"
begin math define pyk of mendelson three two a as text "mendelson three two a" end text end define end math
then math define tex of mendelson three two a as text "
M3.2(a)" end text end define end math
end "
\statement{"
begin math define statement of lemma prime l three two a as system prime s infer all metavar var a end metavar indeed metavar var a end metavar peano is metavar var a end metavar end define end math
end "}
\statement{"
begin math define proof of lemma prime l three two a as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed axiom prime s five conclude metavar var a end metavar peano plus peano zero peano is metavar var a end metavar cut axiom prime s one conclude metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano is metavar var a end metavar cut rule prime mp modus ponens metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano is metavar var a end metavar modus ponens metavar var a end metavar peano plus peano zero peano is metavar var a end metavar conclude metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano is metavar var a end metavar cut rule prime mp modus ponens metavar var a end metavar peano plus peano zero peano is metavar var a end metavar peano imply metavar var a end metavar peano is metavar var a end metavar modus ponens metavar var a end metavar peano plus peano zero peano is metavar var a end metavar conclude metavar var a end metavar peano is metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "}
Den allerf\o rste linje siger at beviset g\ae lder for vilk\aa rlige "
begin bracket metavar var a end metavar end bracket
end ".
Linje 2 og 3 instantierer axiomerne S5 og S1. Bem\ae rk at for linje S1 i linje 3 er "
begin bracket metavar var c end metavar end bracket
end " og "
begin bracket metavar var b end metavar end bracket
end " valgt lig "
begin bracket metavar var a end metavar end bracket
end " s\aa ledes at de to hypoteser
er lig hinanden og konklusionen er det \o nskede resultat. Samtidig er S5 i linje to valgt s\aa \space den matcher de to hypoteser i linje tre.
Derfor kan beviset nemt afsluttes ved at bruge modus ponens med linje to p\aa \space linje tre og derefter en gang til med linje to p\aa \space linje fire.
Bem\ae rk brugen af trekant symbolet. For hver foruds\ae tning til en regel eller s\ae tning beskriver udtrykket efter et af trekantsymbolerne hvordan foruds\ae tningen er overholdt. Fremover vil modus ponens dog istedet
v\ae re repr\ae senteret ved symbolet $\unrhd$ mellem de to foruds\ae tninger.
\subsection{Mendelson Lemma 3.2 (b)}
I sit bevis for n\ae ste bevis benytter Mendelson f\o lgende tautologi
"
begin bracket metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end bracket
end ", men som det kan ses
af beviset er der benyttet en lidt anden s\ae tning.
"
begin math define pyk of lemma prime l three two b as text " lemma prime l three two b" end text end define end math
then math define tex of lemma prime l three two b as text "M3.2(b)" end text end define end math
end "
\statement{"
begin math define statement of lemma prime l three two b as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end define end math
end "}
\statement{"
begin math define proof of lemma prime l three two b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed axiom prime s one conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut lemma prime l three two a conclude metavar var t end metavar peano is metavar var t end metavar cut mendelson corollary one ten b modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar modus ponens metavar var t end metavar peano is metavar var t end metavar conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end quote state proof state cache var c end expand end define end math
end "}
Den afg\o rende observation her er at tautologien ovenfor essentielt svarer til M1.10(b), der udsiger "
begin bracket metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar infer metavar var a end metavar peano imply metavar var b end metavar end bracket
end ". Som det kan ses af beviset er det netop denne regel der er benyttet den afsluttende linje.
M1.10(b) opn\aa s ved en enkelt anvendelse af deduktions s\ae tningen (M1.9) p\aa \space f\o lgende trivielle s\ae tning:
"
begin math define pyk of mendelson corollary one ten pre b as text "mendelson corollary one ten pre b" end text end define end math
then math define tex of mendelson corollary one ten pre b as text "
M1.10(b_-)" end text end define end math
end "
\statement{"
begin math define statement of mendelson corollary one ten pre b as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar infer metavar var a end metavar infer metavar var c end metavar end define end math
end "}
\statement{"
begin math define proof of mendelson corollary one ten pre b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar infer metavar var a end metavar infer rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar conclude metavar var b end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar conclude metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "}
Bem\ae rk at jeg kalder s\ae tningen M1.10($b_-$) selv om den ikke er n\ae vnt i Mendelson. Navnet skyldes at den svarer til M1.10(b) hvor M1.10(b) i stedet for den f\o rste foruds\ae tning har en hypotese.
Problemet er nu at M1.9 ikke bliver bevist formelt s\aa ledes at man uden videre kan introducere det p\aa \space siden og rent faktisk g\ae lder M1.9 ikke ubetinget for f\o rste ordens teorier.
Til geng\ae eld pr\ae senteres en betinget version for f\o rste ordens teorier, hvor der tages forbehold ved brugen af Gen i beviser:
M2.5: Antag at der i et bevis for "
begin bracket metavar var b end metavar infer metavar var c end metavar end bracket
end " ikke benyttes Gen p\aa \space
en linje som afh\ae nger af "
begin bracket metavar var b end metavar end bracket
end " s\aa ledes at den kvantifiserede variabel er en af "
begin bracket metavar var b end metavar end bracket
end "s frie variable. Da eksisterer et bevis for
"
begin bracket metavar var b end metavar peano imply metavar var c end metavar end bracket
end "
Hertil bem\ae rkes at ovenst\aa ende bevis ikke benytter Gen og korollar 1.10 g\ae lder derfor ogs\aa \space
i f\o rste ordens teorier.
Beviset er dog langt fra f\ae rdigt idet M2.5 ikke er et formelt bevis og derfor ikke uden videre kan inkluderes p\aa \space
siden. Beviset er derimod konstruktivt, dvs den skitserer en algoritme til at konvertere et bevis for en s\ae tning med en foruds\ae tning til et bevis, for en s\ae tning med en tilsvarende hypotese.
\subsubsection{Deduktions algoritmen}
I f\o rste omgang beskrives den 'r\aa ' \space ufortolkede version af deduktionsalgoritmen.
Indledningsvis ekspanderes alle beviser s\aa ledes at beviset udelukkende best\aa r af hypoteser, axiomer og de to regler.
Deduktions algoritmen for at \ae ndre en foruds\ae tning til en hypotese "
begin bracket metavar var h end metavar end bracket
end " forl\o ber s\aa ledes, hvor de s\ae tninger
der refereres til f\o lger umiddelbart efter:
\begin{itemize}
\item Hypotesen erstattes af 5 linjer der, viser at "
begin bracket metavar var h end metavar peano imply metavar var h end metavar end bracket
end ", hvor de 5 linjer svarer til beviset for "
begin bracket mendelson one seven end bracket
end "
\item En linje best\aa ende af et axiom p\aa \space
formen "
begin bracket metavar var a end metavar end bracket
end " erstattes af tre linjer, der viser at "
begin bracket metavar var h end metavar peano imply metavar var a end metavar end bracket
end " med to linjer der svarer til "
begin bracket hypothesize end bracket
end " samt det oprindelige axiom.
\item Tilsvarende erstattes en linje med modus ponens der virker ved "
begin bracket metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar end bracket
end "
med 3 linjer, der udf\o rer "
begin bracket metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer metavar var h end metavar peano imply metavar var a end metavar infer metavar var h end metavar peano imply metavar var b end metavar end bracket
end " svarende til "
begin bracket hypothetical rule prime mp end bracket
end "..
\item En linje med Gen erstattes af 3 linjer, der erstatter "
begin bracket peano all metavar var x end metavar indeed metavar var a end metavar end bracket
end " med "
begin bracket metavar var h end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar end bracket
end " svarende til "
begin bracket hypothetical rule prime gen end bracket
end ".
\item For hver linje over hypotesen tilf\o jes 2 linjer svarende til "
begin bracket hypothesize end bracket
end ".
\end{itemize}
F\o lgende fire s\ae tninger stammer fra den oprindelige Peano side og er yderst anvendelige n\aa r man vil konvertere et bevis med foruds\ae tninger til et bevis for en s\ae tning med en foruds\ae tning mindre.
Lemma "
begin math define pyk of mendelson one seven as text "mendelson one seven" end text end define end math
then math define tex of mendelson one seven as text "
M1.7" end text end define end math
end ", svarer til M1.7 og udsiger:
\statement{"
begin math define statement of mendelson one seven as system prime s infer all metavar var b end metavar indeed metavar var b end metavar peano imply metavar var b end metavar end define end math
end "}
\statement{"
begin math define proof of mendelson one seven as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var b end metavar indeed axiom prime a one conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut axiom prime a two conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut axiom prime a one conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var b end metavar end quote state proof state cache var c end expand end define end math
end "}
\subsubsection{Hypothetitisk modus ponens}
Hypotetisk modus ponens "
begin math define pyk of hypothetical rule prime mp as text "hypothetical rule prime mp" end text end define end math
then math define tex of hypothetical rule prime mp as text "
MP'_h" end text end define end math
end " tillader brugen af modus ponens 'bag' en hypotese. Dvs. begge foruds\ae tninger samt konklusionen har den samme hypotese.
\statement{"
begin math define statement of hypothetical rule prime mp as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer metavar var h end metavar peano imply metavar var a end metavar infer metavar var h end metavar peano imply metavar var b end metavar end define end math
end "}
\statement{"
begin math define proof of hypothetical rule prime mp as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer metavar var h end metavar peano imply metavar var a end metavar infer axiom prime a two conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar modus ponens metavar var h end metavar peano imply metavar var a end metavar conclude metavar var h end metavar peano imply metavar var b end metavar end quote state proof state cache var c end expand end define end math
end "}
Hvor de tre sidste linjer er dem, der blev n\ae vnt i algoritmen.
\subsubsection{Tilf\o j hypotese}
Lemma "
begin math define pyk of hypothesize as text "hypothesize" end text end define end math
then math define tex of hypothesize as text "
Tilf\o j hypotese" end text end define end math
end " tillader som tilf\o je en vilk\aa rlig hypotese til foruds\ae tningen:
\statement{"
begin math define statement of hypothesize as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer metavar var h end metavar peano imply metavar var a end metavar end define end math
end "}
\statement{"
begin math define proof of hypothesize as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer axiom prime a one conclude metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar modus ponens metavar var a end metavar conclude metavar var h end metavar peano imply metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "}
De to nederste linjer samt forudg\aa ende instantiering af selve axiomet udg\o r de n\ae vnte tre linjer
\subsubsection{Hypotetisk generalisering}
Hhypotetisk generalisering "
begin math define pyk of hypothetical rule prime gen as text "hypothetical rule prime gen" end text end define end math
then math define tex of hypothetical rule prime gen as text "
Gen'_h" end text end define end math
end " tillader som ved hypotetisk modus ponens at man kan benytte "
begin math rule prime gen end math
end " 'bag' en foranst\aa ende hypotese "
begin math metavar var h end metavar end math
end ":
\statement{"
begin math define statement of hypothetical rule prime gen as system prime s infer all metavar var h end metavar indeed all metavar var x end metavar indeed all metavar var a end metavar indeed peano nonfree quote metavar var x end metavar end quote in quote metavar var h end metavar end quote end nonfree endorse metavar var h end metavar peano imply metavar var a end metavar infer metavar var h end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar end define end math
end "}
\statement{"
begin math define proof of hypothetical rule prime gen as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var x end metavar indeed all metavar var a end metavar indeed peano nonfree quote metavar var x end metavar end quote in quote metavar var h end metavar end quote end nonfree endorse metavar var h end metavar peano imply metavar var a end metavar infer axiom prime a five modus probans peano nonfree quote metavar var x end metavar end quote in quote metavar var h end metavar end quote end nonfree conclude peano all metavar var x end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar cut rule prime gen modus ponens metavar var h end metavar peano imply metavar var a end metavar conclude peano all metavar var x end metavar indeed metavar var h end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens peano all metavar var x end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar modus ponens peano all metavar var x end metavar indeed metavar var h end metavar peano imply metavar var a end metavar conclude metavar var h end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "}
De tre sidste linjer er dem, der fremkommer af deduktions algoritmen.
\subsubsection{Korollar M1.10b}
Med disse redskaber kan vi nu returnere til beviset for "
begin math define pyk of mendelson corollary one ten b as text "mendelson corollary one ten b" end text end define end math
then math define tex of mendelson corollary one ten b as text "
M1.10(b)" end text end define end math
end ". Husk at beviset for M1.10($b_-$) netop svarer til M1.10b bortset fra at konklusionens hypotese indg\aa r som en foruds\ae tning.
\statement{"
begin math define statement of mendelson corollary one ten b as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar infer metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
Det resulterende bevis er oversat linje for linje fra M1.10(pre-b)med de ovenst\aa ende regler:
\statement{"
begin math define proof of mendelson corollary one ten b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar infer hypothesize modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut hypothesize modus ponens metavar var b end metavar conclude metavar var a end metavar peano imply metavar var b end metavar cut mendelson one seven conclude metavar var a end metavar peano imply metavar var a end metavar cut hypothetical rule prime mp modus ponens metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar peano imply metavar var a end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut hypothetical rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar conclude metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "}
Hvis man ikke t\ae ller den enkelte define med er beviset nu blevet en linje l\ae ngere for hver af de to resterende foruds\ae tninger, men svarer ellers fuldst\ae ndig til det oprindelige.
Det er dog v\ae rd at bem\ae rke at eftersom "
begin bracket metavar var a end metavar end bracket
end " er identisk med "
begin bracket metavar var h end metavar end bracket
end " konkluderer den f\o rste modus ponens at
"
begin bracket metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar end bracket
end " hvilket stadig haves som foruds\ae tninger, hvilket g\o r linjen overfl\o dig.
Med beviset for M1.10(b) er beviset for M3.2(b) samtidig blevet afsluttet. Det kan sikkert virke p\aa \space
l\ae seren som en un\o dvendigt detaljeret gennemgang af et ikke s\ae rligt kompliceret bevis, men metoden med brug af s\ae tninger, der kun modificerer konklusionen og ikke hypotesen af et udsagn,
viser sig helt uundv\ae rlig i de senere induktionsbeviser.
Hvor Mendelson i sine beviser hver gang starter med en foruds\ae tning som han til sidst \ae ndrer til en hypotese ved brug af deduktions s\ae tningen (M2.5), bliver man her n\o dt til at
sl\ae be hypotesen med fra start til slut. Netop derfor er det afg\o rende at have de s\ae tninger, der tillader at hypotesen kan ignoreres.
\subsection{M3.2(c)}
Den n\ae ste s\ae tning, der bliver brug for minder i udpr\ae get grad om axiom S1, men med termerne permuteret s\aa ledes at den ikke kan opn\aa s
ved en direkte anvendelse af axiomet:
"
begin math define pyk of lemma prime l three two c as text " lemma prime l three two c" end text end define end math
then math define tex of lemma prime l three two c as text "M3.2(c)" end text end define end math
end "
\statement{"
begin math define statement of lemma prime l three two c as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end define end math
end "}
\statement{"
begin math define proof of lemma prime l three two c as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed axiom prime s one conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut lemma prime l three two b conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut mendelson corollary one ten a modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar modus ponens metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define end math
end "}
Som det kan ses kan termerne i axiom S1 v\ae lges s\aa ledes at den resulterende tautologi kun afviger fra det \o nskede i den forreste hypotese. Desuden fort\ae ller
foreg\aa ende s\ae tning at den forreste hypotese er lig den forreste version. For at n\aa \space
resultatet benyttes endnu et korollar M1.10(a). "
begin math define pyk of mendelson corollary one ten a as text " mendelson corollary one ten a " end text end define end math
then math define tex of mendelson corollary one ten a as text "M1.10(a)" end text end define end math
end "
\statement{"
begin math define statement of mendelson corollary one ten a as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
\statement{"
begin math define proof of mendelson corollary one ten a as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var b end metavar peano imply metavar var c end metavar infer mendelson one seven conclude metavar var a end metavar peano imply metavar var a end metavar cut hypothesize modus ponens metavar var a end metavar peano imply metavar var b end metavar conclude metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut hypothesize modus ponens metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut hypothetical rule prime mp modus ponens metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar modus ponens metavar var a end metavar peano imply metavar var a end metavar conclude metavar var a end metavar peano imply metavar var b end metavar cut hypothetical rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar conclude metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "}
Beviset konstrueres helt analogt til M1.10(b)
\subsection{M3.2(d)}
Ligesom foreg\aa ende s\ae tning minder M3.2(d) om axiom S1, men i dette tilf\ae lde kan s\ae tningen ikke instantieres fra de forudg\aa ende s\aa ledes
at det kun er forreste hypotese der afviger fra det \o nskede. Udgangspunktet for s\ae tningen bliver M3.2(c) der instantieres s\aa ledes at konklusionen
svarer til konklusionen for den \o nskede s\ae tning.
Der har indsneget sig en mindre fejl i Mendelson idet beviset for M3.2(d) resulterer i
"
begin bracket metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end bracket
end ", mens
det han oprindelig kalder M3.2(d) er "
begin bracket metavar var r end metavar peano is metavar var t end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end bracket
end ".
S\ae tningerne er essentielt forskellige dvs, man kan ikke bare instantiere den anden version ved at bytte om p\aa \space
termernes navne. Da de f\o lgende resultater kr\ae ver begge versioner
har jeg kaldt den s\ae tning Mendelson f\aa r vist for M3.2(d)(I), mens s\ae tningen som den bliver beskrevet indledningsvis er kaldt M3.2(d)(II).
\statement{"
begin math define statement of lemma prime l three two d one as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end define end math
end "}
"
begin math define pyk of lemma prime l three two d one as text " lemma prime l three two d one" end text end define end math
then math define tex of lemma prime l three two d one as text "M3.2(d) (I)" end text end define end math
end "
\statement{"
begin math define proof of lemma prime l three two d one as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed lemma prime l three two c conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut mendelson corollary one ten b plus plus modus ponens metavar var r end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut lemma prime l three two b conclude metavar var s end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut mendelson corollary one ten a modus ponens metavar var s end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar modus ponens metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define end math
end "}
Den helt afg\o rende linje i ovenst\aa ende bevis er nummer fem, hvor en ny version af korollar 1.10(b) benyttes (jeg har kaldt den korollar M1.10($b_+$), selv om denne formulering af s\ae tningen heller ikke
findes i Mendelson). I den nye version a M1.10($b_+$) er endnu en foruds\ae tning fjernet og tilf\o jet som hypotese. At foreg\aa ende version ikke er tilstr\ae kkelig kan ses af at den bagerste hypotese ikke l\ae ngere
er en tautologi som i beviset for M3.2(b) (hvor man benyttede det allerede viste "
begin bracket metavar var t end metavar peano is metavar var t end metavar end bracket
end ")
Beviset for korollar M1.10(b) indeholder ligesom beviset for M1.10($b_-$) ikke nogen linjer der bruger Gen. Derfor kan vi uden bekymring bruge deduktions algoritmen endnu en gang, men sp\o rgsm\aa let er nu hvorledes dette
g\o res nemmest. Problemet med deduktionsalgoritmen er at den ekspanderer et bevis ganske voldsomt. Et bevis med n linjer og en enkelt foruds\ae tning, der skal fjernes vokser til et bevis med 3n+2 linjer og tilsvarende vil
yderligere fjernelse af foruds\ae tninger f\aa
beviset til at vokse med ca. en faktor tre.
Men inspireret af beviset for M1.10(b), hvor der fandtes en metode til at overs\ae tte beviset linje for linje til et bevis af essentielt samme st\o rrelse, vil jeg nu
for\o ge at generalisere metoden s\aa \space
jeg kan fjerne to foruds\ae tninger uden at beviset vokser eller bliver ul\ae seligt
Jeg har dog undladt Gen, da den ikke er n\o dvendig til beviset.
Lemma "
begin math define pyk of hypothesize plus plus as text "hypothesize plus plus" end text end define end math
then math define tex of hypothesize plus plus as text "
Tilf\o j hypotese_+" end text end define end math
end " tillader som tilf\o je en vilk\aa rlig hypotese til foruds\ae tningen
\statement{"
begin math define statement of hypothesize plus plus as system prime s infer all metavar var i end metavar indeed all metavar var h end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar end define end math
end "}
\statement{"
begin math define proof of hypothesize plus plus as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var i end metavar indeed all metavar var h end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer hypothesize modus ponens metavar var a end metavar conclude metavar var h end metavar peano imply metavar var a end metavar cut hypothesize modus ponens metavar var h end metavar peano imply metavar var a end metavar conclude metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "}
Ved ovenst\aa ende er der snydt lidt i den forstand at beviset ikke bygger p\aa \space
deduktions algoritmen. Beviset kan dog stadig uden videre generaliseres til flere hypoteser.
Hypotetisk modus ponens "
begin math define pyk of hypothetical rule prime mp plus plus as text "hypothetical rule prime mp plus plus" end text end define end math
then math define tex of hypothetical rule prime mp plus plus as text "
MP'_h+" end text end define end math
end "
\statement{"
begin math define statement of hypothetical rule prime mp plus plus as system prime s infer all metavar var i end metavar indeed all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar infer metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar end define end math
end "}
\statement{"
begin math define proof of hypothetical rule prime mp plus plus as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var i end metavar indeed all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar infer axiom prime a two conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar cut hypothesize modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar conclude metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar cut hypothetical rule prime mp modus ponens metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar modus ponens metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar cut hypothetical rule prime mp modus ponens metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar modus ponens metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var a end metavar conclude metavar var i end metavar peano imply metavar var h end metavar peano imply metavar var b end metavar end quote state proof state cache var c end expand end define end math
end "}
Modus ponens generaliserers umiddelbart til to hypoteser ved at konvertere beviset for modus ponens med en hypotese. Bem\ae rk at beviset stadig ekspanderer med en enkelt linie, hvilket skyldes at axiom to ikke
p\aa \space
forh\aa nd er bevist i en hypotetisk udgave. Der er dog stadig ingen problemer med at beviset ekspanderer ukontrollabelt ved yderligere generalisering idet man ved endnu et genneml\o b af algoritmen erstatter 'Tilf\o j hypotese' med
'Tilf\o j hypotese+'.
Det er knap s\aa \space
\aa benlyst hvordan man introducerer foruds\ae tning nummer to "
begin bracket metavar var b end metavar end bracket
end " som en hypotese. Husk at hvis der i det oprindelige bevis er blevet benyttet "
begin bracket metavar var b end metavar end bracket
end "
vil der efter f\o rste genneml\o b af algoritmen v\ae re en 'Tilf\o j hypotese' der fort\ae ller at "
begin bracket metavar var a end metavar peano imply metavar var b end metavar end bracket
end ". Men n\aa r foruds\ae tningen "
begin bracket metavar var b end metavar end bracket
end " fjernes
er ovenst\aa ende ikke l\ae ngere sandt og hvor man i de \o vrige tilf\ae lde kan erstatte 'Tilf\o j hypotese' med 'Tilf\o j hypotese+' s\aa \space er foruds\ae tningen for brug af lemmaet ikke l\ae ngere til stede.
Algoritmen fungerer ikke desto mindre stadigv\ae k s\aa \space det man skal huske er at f\aa hypoteserne introduceret korrekt. Hertil bruges:
"
begin math define pyk of mendelson one seven plus plus as text "mendelson one seven plus plus" end text end define end math
then math define tex of mendelson one seven plus plus as text "
M1.7_+" end text end define end math
end ".
\statement{"
begin math define statement of mendelson one seven plus plus as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end define end math
end "}
\statement{"
begin math define proof of mendelson one seven plus plus as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed mendelson one seven conclude metavar var b end metavar peano imply metavar var b end metavar cut axiom prime a one conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut hypothesize modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut hypothetical rule prime mp modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar modus ponens metavar var b end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end quote state proof state cache var c end expand end define end math
end "}
Hvor M1.7 bliver brugt til at introducere f\o rste hypotese bliver $M1.7_+$ bliver brugt til at introducere hypotese nummer to.
$M1.7_+$ kan ligeledes generaliseres til flere hypoteser. Man skal dog v\ae re opm\ae rksom p\aa \space at mens de tre nederste linjer skal igennem algoritmen igen, s\aa \space
den tilsvarende regel med en hypotese mere, s\aa \space
skal linjen der instantierer M1.7 forblive uber\o rt.
Ovenst\aa ende er et bevis for axiom A1 og kunne derfor nemt v\ae re undv\ae ret. Men hvor man ved to hypoteser f\aa r s\ae tningen for\ae rende vil man ved f.eks tre hypoteser skulle vise
"
begin bracket metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end bracket
end " som kan vises med udgangspunkt i M1.7++ .
For nu at vende tilbage til udgangspunktet:
Lemma "
begin math define pyk of mendelson corollary one ten b plus plus as text "mendelson corollary one ten b plus plus" end text end define end math
then math define tex of mendelson corollary one ten b plus plus as text "
M1.10(b_+)" end text end define end math
end "
\statement{"
begin math define statement of mendelson corollary one ten b plus plus as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
\statement{"
begin math define proof of mendelson corollary one ten b plus plus as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer mendelson one seven plus plus conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut mendelson one seven conclude metavar var a end metavar peano imply metavar var a end metavar cut hypothesize modus ponens metavar var a end metavar peano imply metavar var a end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar cut hypothesize plus plus modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut hypothetical rule prime mp plus plus modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut hypothetical rule prime mp plus plus modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "}
Hermed er beviset for s\ae tning M3.2(d)(I). S\ae tning M3.2(d)(II) f\o lger umiddelbart:
\statement{"
begin math define statement of lemma prime l three two d two as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var r end metavar peano is metavar var t end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end define end math
end "}
"
begin math define pyk of lemma prime l three two d two as text " lemma prime l three two d two" end text end define end math
then math define tex of lemma prime l three two d two as text "M3.2(d) (II)" end text end define end math
end "
\statement{"
begin math define proof of lemma prime l three two d two as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed lemma prime l three two d one conclude metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut mendelson corollary one ten b plus plus modus ponens metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define end math
end "}
De beviste s\ae tninger giver os nu f\o lgende fundamentale egenskaber ved lighed:
\begin{itemize}
\item M3.2(a): refleksivitet
\item M3.2(b): symmetri
\item M3.2(c+d): transitivitet (delvis, men tilstr\ae kkeligt til vores form\aa l)
\end{itemize}
\subsection{Flere hypotetiske lemmaer}
Jeg kan allerede nu afsl\o re at der ikke kommer flere s\ae tninger, hvor h\aa ndtering af to hypoteser er n\o dvendigt. Til geng\ae ld
vil der v\ae re flittig brug af s\ae ningerne, der h\aa ndterer en enkelt hypotese. Dertil vil f\o lgende simple s\ae tninger hj\ae lpe med at holde
beviserne korte og overskuelige idet man slipper for at instantiere 'Tilf\o j hypotese' hver gang man instantierer et lemma eller axiom.
"
begin math define pyk of hypothetical three two a as text "hypothetical three two a" end text end define end math
then math define tex of hypothetical three two a as text "
M3.2(a)_h" end text end define end math
end "
\statement{"
begin math define statement of hypothetical three two a as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar end define end math
end "}
\statement{"
begin math define proof of hypothetical three two a as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed lemma prime l three two a conclude metavar var t end metavar peano is metavar var t end metavar cut hypothesize modus ponens metavar var t end metavar peano is metavar var t end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar end quote state proof state cache var c end expand end define end math
end "}
"
begin math define pyk of hypothetical three two b as text "hypothetical three two b" end text end define end math
then math define tex of hypothetical three two b as text "
M3.2(b)_h" end text end define end math
end "
\statement{"
begin math define statement of hypothetical three two b as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end define
then define proof of hypothetical three two b as rule tactic end define end math
end "}
\statement{"
begin math define proof of hypothetical three two b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer axiom prime s one conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut hypothesize modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut hypothetical three two a conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var t end metavar conclude metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end quote state proof state cache var c end expand end define end math
end "}
"
begin math define pyk of hypothetical three one s two as text "hypothetical three one s two" end text end define end math
then math define tex of hypothetical three one s two as text "
M3.1(S2')_h" end text end define end math
end "
\statement{"
begin math define statement of hypothetical three one s two as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var t end metavar peano succ peano is metavar var r end metavar peano succ end define end math
end "}
\statement{"
begin math define proof of hypothetical three one s two as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer axiom prime s two conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano succ peano is metavar var r end metavar peano succ cut hypothesize modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano succ peano is metavar var r end metavar peano succ conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano succ peano is metavar var r end metavar peano succ cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano succ peano is metavar var r end metavar peano succ modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano succ peano is metavar var r end metavar peano succ end quote state proof state cache var c end expand end define end math
end "}
"
begin math define pyk of hypothetical three one s one as text "hypothetical three one s one" end text end define end math
then math define tex of hypothetical three one s one as text "
M3.1(S1')_h" end text end define end math
end "
\statement{"
begin math define statement of hypothetical three one s one as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end define end math
end "}
\statement{"
begin math define proof of hypothetical three one s one as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar infer axiom prime s one conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut hypothesize modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar conclude metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define end math
end "}
"
begin math define pyk of hypothetical three two c as text "hypothetical three two c" end text end define end math
then math define tex of hypothetical three two c as text "
M3.2(c)_h" end text end define end math
end "
\statement{"
begin math define statement of hypothetical three two c as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar infer metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end define end math
end "}
\statement{"
begin math define proof of hypothetical three two c as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar infer lemma prime l three two c conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut hypothesize modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar conclude metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar modus ponens metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define end math
end "}
"
begin math define pyk of hypothetical three one s five as text "hypothetical three one s five" end text end define end math
then math define tex of hypothetical three one s five as text "
M3.1(S5')_h" end text end define end math
end "
\statement{"
begin math define statement of hypothetical three one s five as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano plus peano zero peano is metavar var t end metavar end define end math
end "}
\statement{"
begin math define proof of hypothetical three one s five as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed axiom prime s five conclude metavar var t end metavar peano plus peano zero peano is metavar var t end metavar cut hypothesize modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar conclude metavar var h end metavar peano imply metavar var t end metavar peano plus peano zero peano is metavar var t end metavar end quote state proof state cache var c end expand end define end math
end "}
"
begin math define pyk of hypothetical three one s six as text "hypothetical three one s six" end text end define end math
then math define tex of hypothetical three one s six as text "
M3.1(S6')_h" end text end define end math
end "
\statement{"
begin math define statement of hypothetical three one s six as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano plus metavar var r end metavar peano succ peano is metavar var t end metavar peano plus metavar var r end metavar peano succ end define end math
end "}
\statement{"
begin math define proof of hypothetical three one s six as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed axiom prime s six conclude metavar var t end metavar peano plus metavar var r end metavar peano succ peano is metavar var t end metavar peano plus metavar var r end metavar peano succ cut hypothesize modus ponens metavar var t end metavar peano plus metavar var r end metavar peano succ peano is metavar var t end metavar peano plus metavar var r end metavar peano succ conclude metavar var h end metavar peano imply metavar var t end metavar peano plus metavar var r end metavar peano succ peano is metavar var t end metavar peano plus metavar var r end metavar peano succ end quote state proof state cache var c end expand end define end math
end "}
"
begin math define pyk of hypothetical three two d as text " hypothetical three two d" end text end define end math
then math define tex of hypothetical three two d as text "M3.2(d)_h" end text end define end math
end "
\statement{"
begin math define statement of hypothetical three two d as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar infer metavar var h end metavar peano imply metavar var s end metavar peano is metavar var t end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end define end math
end "}
\statement{"
begin math define proof of hypothetical three two d as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar infer metavar var h end metavar peano imply metavar var s end metavar peano is metavar var t end metavar infer lemma prime l three two d one conclude metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut hypothesize modus ponens metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var h end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar modus ponens metavar var h end metavar peano imply metavar var s end metavar peano is metavar var t end metavar conclude metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar modus ponens metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar conclude metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define end math
end "}
Flere af de ovenst\aa ende s\ae tninger afviger fra den oprindelige version ved at de har erstattet hypoteser med foruds\ae tninger. Dette giver mening i de kommende lange beviser idet man for hver foruds\ae tning
sparer den modus ponens der skal til for at fjerne en hypotese. Det kr\ae ver
til geng\ae ld at foruds\ae tningerne er bevist.
\subsection{Lemma M3.2(h)(I)}
Nu er fundamentet lagt til at induktions beviset kan p\aa \space begyndes. Som sagt \o nskes s\ae tningen "
begin bracket var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var end bracket
end " bevist for alle x og y. For at f\o lge
Mendelson vil beviset derfor blive f\o rt i tre trin ved induktion over "
begin math var y peano var end math
end ".
"
begin math define pyk of lemma prime l three two h one as text " lemma prime l three two h one" end text end define end math
then math define tex of lemma prime l three two h one as text "M3.2(h) (I)" end text end define end math
end "
\statement{"
begin math define statement of lemma prime l three two h one as system prime s infer var x peano var peano plus peano zero peano is peano zero peano plus var x peano var end define end math
end "}
\statement{"
begin math define proof of lemma prime l three two h one as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var x peano var peano plus peano zero peano is var x peano var cut mendelson three two f conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var cut axiom prime a four at var x peano var conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var x peano var peano is peano zero peano plus var x peano var cut rule prime mp modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var x peano var peano is peano zero peano plus var x peano var modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var conclude var x peano var peano is peano zero peano plus var x peano var cut lemma prime l three two c conclude var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano plus peano zero peano is peano zero peano plus var x peano var cut rule prime mp modus ponens var x peano var peano plus peano zero peano is var x peano var peano imply var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano plus peano zero peano is peano zero peano plus var x peano var modus ponens var x peano var peano plus peano zero peano is var x peano var conclude var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano plus peano zero peano is peano zero peano plus var x peano var cut rule prime mp modus ponens var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano plus peano zero peano is peano zero peano plus var x peano var modus ponens var x peano var peano is peano zero peano plus var x peano var conclude var x peano var peano plus peano zero peano is peano zero peano plus var x peano var end quote state proof state cache var c end expand end define end math
end "}
Bem\ae rk at der ikke l\ae ngere benyttes termer (repr\ae senteret ved metavariable), men konkrete variable hvilket skyldes at axiom S9 ikke er gyldigt for vilk\aa rlige termer.
Som det kan ses giver det nogle ekstra linjer i beviset n\aa r et resultat for en konkret variabel skal konverteres til det tilsvarende resultat for en anden variabel.
Der mangler stadig resultatet for M3.2(f):
"
begin math define pyk of mendelson three two f as text "mendelson three two f" end text end define end math
then math define tex of mendelson three two f as text "
M3.2(f)" end text end define end math
end "
\statement{"
begin math define statement of mendelson three two f as system prime s infer peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var end define end math
end "}
\statement{"
begin math define proof of mendelson three two f as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime a one conclude var x peano imply var x peano imply var x cut hypothetical three one s five conclude var x peano imply var x peano imply var x peano imply peano zero peano plus peano zero peano is peano zero cut hypothetical three two b modus ponens var x peano imply var x peano imply var x peano imply peano zero peano plus peano zero peano is peano zero conclude var x peano imply var x peano imply var x peano imply peano zero peano is peano zero peano plus peano zero cut rule prime mp modus ponens var x peano imply var x peano imply var x peano imply peano zero peano is peano zero peano plus peano zero modus ponens var x peano imply var x peano imply var x conclude peano zero peano is peano zero peano plus peano zero cut mendelson one seven conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var cut hypothetical three one s two modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut hypothetical three one s six conclude var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut hypothetical three two b modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut hypothetical three two c modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut rule prime gen modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut axiom prime s nine conclude peano zero peano is peano zero peano plus peano zero peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var cut rule prime mp modus ponens peano zero peano is peano zero peano plus peano zero peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var modus ponens peano zero peano is peano zero peano plus peano zero conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var cut rule prime mp modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var end quote state proof state cache var c end expand end define end math
end "}
M3.2(f) er et fuldt induktionsbevis, hvor der i f\o rste del udnyttes refleksivitet af lighed og i anden del transitivitet af lighed. Induktions axiomet bliver f\o rst instantieret mod slutningen efter at begge dets
hypoteser er bevist som tautologier. Linje 7-11 illustrerer brugen af den teknik, der tillader at f\o re
formelle beviser uden referencer til deduktions s\ae tningen og uden at \o del\ae gge bevisets overskuelighed. Den lidt sp\o jse brug af "
begin bracket metavar var z end metavar end bracket
end " i starten af beviset skyldes at beviset stammer
fra den oprindelige Peano side hvor M3.2(b) kun var vist i en hypotetisk udgave. Der tilf\o jes derfor en vilk\aa rlig tautologi f\o r s\ae tningen bruges for derefter at blive smidt v\ae k.
Med M3.2(f) fuldst\ae ndigg\o r f\o rste del af beviset for kommutativet, nemlig det simple tilf\ae lde hvor "
begin bracket var y peano var end bracket
end " er "
begin bracket peano zero end bracket
end ".
\subsection{Lemma M3.2(g)}
Inden M3.2(h) kan afsluttes er der brug for et sidste, men ganske omfattende induktionsbevis:
"
begin math define pyk of lemma prime l three two g as text " lemma prime l three two g" end text end define end math
then math define tex of lemma prime l three two g as text "M3.2(g)" end text end define end math
end "
\statement{"
begin math define statement of lemma prime l three two g as system prime s infer var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ end define end math
end "}
\statement{"
begin math define proof of lemma prime l three two g as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var y peano var peano succ peano plus peano zero peano is var y peano var peano succ cut axiom prime s five conclude var y peano var peano plus peano zero peano is var y peano var cut axiom prime s two conclude var y peano var peano plus peano zero peano is var y peano var peano imply var y peano var peano plus peano zero peano succ peano is var y peano var peano succ cut rule prime mp modus ponens var y peano var peano plus peano zero peano is var y peano var peano imply var y peano var peano plus peano zero peano succ peano is var y peano var peano succ modus ponens var y peano var peano plus peano zero peano is var y peano var conclude var y peano var peano plus peano zero peano succ peano is var y peano var peano succ cut lemma prime l three two d two conclude var y peano var peano succ peano plus peano zero peano is var y peano var peano succ peano imply var y peano var peano plus peano zero peano succ peano is var y peano var peano succ peano imply var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ cut rule prime mp modus ponens var y peano var peano succ peano plus peano zero peano is var y peano var peano succ peano imply var y peano var peano plus peano zero peano succ peano is var y peano var peano succ peano imply var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ modus ponens var y peano var peano succ peano plus peano zero peano is var y peano var peano succ conclude var y peano var peano plus peano zero peano succ peano is var y peano var peano succ peano imply var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ cut rule prime mp modus ponens var y peano var peano plus peano zero peano succ peano is var y peano var peano succ peano imply var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ modus ponens var y peano var peano plus peano zero peano succ peano is var y peano var peano succ conclude var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ cut mendelson one seven conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut hypothetical three one s six conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano succ cut hypothetical three one s two modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ cut hypothetical three two c modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano succ modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ cut hypothetical three one s six conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut hypothetical three one s two modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano plus var x peano var peano succ peano succ peano is var y peano var peano plus var x peano var peano succ peano succ cut hypothetical three two d modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano plus var x peano var peano succ peano succ peano is var y peano var peano plus var x peano var peano succ peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ cut axiom prime s nine conclude var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ peano imply peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ peano imply peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut rule prime mp modus ponens var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ peano imply peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ peano imply peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ modus ponens var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ conclude peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ peano imply peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut rule prime gen modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ conclude peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ cut rule prime mp modus ponens peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ peano imply peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ modus ponens peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ conclude peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut axiom prime a four at var x peano var conclude peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut rule prime mp modus ponens peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ modus ponens peano all var x peano var indeed var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ end quote state proof state cache var c end expand end define end math
end "}
Ligesom i M3.2 (f) er det transitivitets s\ae tningerne, der binder de forskellige linjer sammen i beviset mens udsagnene der kombineres i dette bevis stammer fra axiomerne S2, S5 og S6.
Jeg har med vilje byttet om p\aa \space
variablene x og y i forhold til Mendelsons formulering idet M3.2(h)(II) bruger s\ae tningen i den formulering. Jeg slipper derfor
for at bruge Gen og A4 til at skifte variable.
\subsection{Lemma M3.2(h)(II)}
Nu kan den sidste hypotese i induktionen bevises. Med udgangspunkt i axiom S6 og forrige resultat kan beviset strikkes
sammen ved symmetri og transitivitets s\ae tningerne:
"
begin math define pyk of lemma prime l three two h two as text " lemma prime l three two h two" end text end define end math
then math define tex of lemma prime l three two h two as text "M3.2(h) (II)" end text end define end math
end "
\statement{"
begin math define statement of lemma prime l three two h two as system prime s infer var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var end define end math
end "}
\statement{"
begin math define proof of lemma prime l three two h two as lambda var c dot lambda var x dot proof expand quote system prime s infer mendelson one seven conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var cut hypothetical three one s six conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ cut lemma prime l three two g conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut hypothesize modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut hypothetical three one s two modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut hypothetical three two c modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut hypothetical three two d modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var end quote state proof state cache var c end expand end define end math
end "}
\subsection{Lemma M3.2(h)}
"
begin math define pyk of lemma prime l three two h as text " lemma prime l three two h" end text end define end math
then math define tex of lemma prime l three two h as text "M3.2(h)" end text end define end math
end "
\statement{"
begin math define statement of lemma prime l three two h as system prime s infer peano all var x peano var indeed peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var end define end math
end "}
"
begin math define pyk of lemma prime l three two f as text " lemma prime l three two f" end text end define end math
then math define tex of lemma prime l three two f as text "M3.2(f)" end text end define end math
end "
Nu kan brikkerne samles ved en sidste gang at instantiere S9:
\statement{"
begin math define proof of lemma prime l three two h as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s nine conclude var x peano var peano plus peano zero peano is peano zero peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var cut lemma prime l three two h one conclude var x peano var peano plus peano zero peano is peano zero peano plus var x peano var cut lemma prime l three two h two conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var cut rule prime gen modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var conclude peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var cut rule prime mp modus ponens var x peano var peano plus peano zero peano is peano zero peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var modus ponens var x peano var peano plus peano zero peano is peano zero peano plus var x peano var conclude peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var cut rule prime mp modus ponens peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano imply peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var modus ponens peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var conclude peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var cut rule prime gen modus ponens peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var conclude peano all var x peano var indeed peano all var y peano var indeed var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var end quote state proof state cache var c end expand end define end math
end "}
Beviset er afsluttet og siden godkendt af Logiweb serveren.
\section{Konklusion}
Beviset er i hovedtr\ae k gennemf\o rt som beskrevet i Mendelson, men hvor Mendelson bruger deduktions s\ae tningen (M2.5) som garanti for eksistensen af et bevis, har
kravet til denne opgave v\ae ret konstruktionen af et s\aa dant bevis. Derfor er der to grundl\ae ggende strategier, man kan f\o lge:
Implementer et program, der konstruerer et bevis med hypoteser udfra et bevis med foruds\ae tninger. Jeg er overbevist om at dette kan lade sig g\o re inden for Logiweb systemet, men
vil kr\ae ve at man benytter v\ae sentlig mere kompliceret og grundl\ae ggende funktionalitet i systemet end det er der er benyttet til denne side.
Alternativt kan man som illustreret i rapporten hvorledes man udleder s\ae tningerne, med udgangspunkt i den konstruktive algoritme bag M2.5.
Ved omhyggeligt at konstruere hj\ae lpes\ae tninger baseret p\aa \space deduktions algoritmen kan man manuelt modificere sine beviser uden at de bliver uoverskuelige eller eksploderer i st\o rrelse.
\appendix
\section{Pyk definitioner}
\subsection{Sidens navn}
\display{"
begin math define pyk of proofreport as text "proofreport" end text end define end math
end "}
\subsection{Modus ponens}
"
begin math define pyk of var x hypothetical modus ponens var y as text "* hypothetical modus ponens *" end text end define end math
then math define tex of var x hypothetical modus ponens var y as text "#1.
\unrhd_h #2." end text end define end math
end "
\display{"
begin math define macro of var x hypothetical modus ponens var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x hypothetical modus ponens var y as hypothetical rule prime mp modus ponens var x modus ponens var y end define end quote end define end define end math
end "}
"
begin math define pyk of var x macro modus ponens var y as text "* macro modus ponens *" end text end define end math
then math define tex of var x macro modus ponens var y as text "#1.
\unrhd #2." end text end define end math
end "
\display{"
begin math define macro of var x macro modus ponens var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x macro modus ponens var y as rule prime mp modus ponens var x modus ponens var y end define end quote end define end define end math
end "}
\subsection{Variable}
"
begin math define pyk of var x peano var as text "* peano var" end text end define end math
then math define tex of var x peano var as text "
\dot{#1.
}" end text end define end math
end "
"
begin math define pyk of var x is peano var as text "* is peano var" end text end define end math
then math define tex of var x is peano var as text "#1.
{} ^ {\cal P}" end text end define end math
end "
\display{"
begin math define value of var x is peano var as var x term root equal quote var x peano var end quote end define end math
end "}
"
begin math define pyk of peano a as text "peano a" end text end define end math
then math define tex of peano a as text "
\dot{\mathit{a}}" end text end define end math
end "
\display{"
begin math define macro of peano a as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano a as var a peano var end define end quote end define end define end math
end "}%
\subsection{ free og nonefree }
"
begin math define pyk of peano nonfree var x in var y end nonfree as text "peano nonfree * in * end nonfree" end text end define end math
then math define tex of peano nonfree var x in var y end nonfree as text "
\dot{nonfree}(#1.
,#2.
)" end text end define end math
end "
"
begin math define pyk of peano nonfree star var x in var y end nonfree as text "peano nonfree star * in * end nonfree" end text end define end math
then math define tex of peano nonfree star var x in var y end nonfree as text "
\dot{nonfree}^*(#1.
,#2.
)" end text end define end math
end "
\display{"
begin math define value of peano nonfree var x in var y end nonfree as newline tagged if var y is peano var then not var x term equal var y else newline tagged if not var y term root equal quote peano all var x indeed var y end quote then peano nonfree star var x in var y tail end nonfree else newline tagged if var x term equal var y first then true else peano nonfree var x in var y second end nonfree end if end if end if end define end math
end "}
\display{"
begin math define value of peano nonfree star var x in var y end nonfree as var x tagged guard tagged if var y then true else tagged if peano nonfree var x in var y head end nonfree then peano nonfree star var x in var y tail end nonfree else false end if end if end define end math
end "}%
%
"
begin math define pyk of peano free var a set var x to var b end free as text "peano free * set * to * end free" end text end define end math
then math define tex of peano free var a set var x to var b end free as text "
\dot{free}\langle #1.
| #2.
:= #3.
\rangle" end text end define end math
end "
"
begin math define pyk of peano free star var a set var x to var b end free as text "peano free star * set * to * end free" end text end define end math
then math define tex of peano free star var a set var x to var b end free as text "
\dot{free}{}^*\langle #1.
| #2.
:= #3.
\rangle" end text end define end math
end "
"
begin bracket var a end bracket
end "
\display{"
begin math define value of peano free var a set var x to var b end free as var x tagged guard var b tagged guard newline tagged if var a is peano var then true else newline tagged if not var a term root equal quote peano all var u indeed var v end quote then peano free star var a tail set var x to var b end free else newline tagged if var a first term equal var x then true else newline tagged if peano nonfree var x in var a second end nonfree then true else newline tagged if not peano nonfree var a first in var b end nonfree then false else newline peano free var a second set var x to var b end free end if end if end if end if end if end define end math
end "}
\display{"
begin math define value of peano free star var a set var x to var b end free as var x tagged guard var b tagged guard tagged if var a then true else tagged if peano free var a head set var x to var b end free then peano free star var a tail set var x to var b end free else false end if end if end define end math
end "}%
%
"
begin math define pyk of peano sub var a is var b where var x is var c end sub as text "peano sub * is * where * is * end sub" end text end define end math
then math define tex of peano sub var a is var b where var x is var c end sub as text "#1.
{\equiv}\langle #2.
|#3.
:=#4.
\rangle" end text end define end math
end "
"
begin math define pyk of peano sub star var a is var b where var x is var c end sub as text "peano sub star * is * where * is * end sub" end text end define end math
then math define tex of peano sub star var a is var b where var x is var c end sub as text "#1.
{\equiv}\langle^* #2.
|#3.
:=#4.
\rangle" end text end define end math
end "
\display{"
begin math define value of peano sub var a is var b where var x is var c end sub as var a tagged guard var x tagged guard var c tagged guard newline tagged if tagged if var b term root equal quote peano all var u indeed var v end quote then var b first term equal var x else false end if then var a term equal var b else newline tagged if var b is peano var and var b term equal var x then var a term equal var c else tagged if newline var a term root equal var b then peano sub star var a tail is var b tail where var x is var c end sub else false end if end if end if end define end math
end "}
\display{"
begin math define value of peano sub star var a is var b where var x is var c end sub as var b tagged guard var x tagged guard var c tagged guard tagged if var a then true else tagged if peano sub var a head is var b head where var x is var c end sub then peano sub star var a tail is var b tail where var x is var c end sub else false end if end if end define end math
end "}%
%
\subsection{Variables of Peano arithmetic}\label{section:VariablesOfPeanoArithmetic}
"
begin math define pyk of peano b as text "peano b" end text end define end math
then math define tex of peano b as text "
\dot{\mathit{b}}" end text end define end math
end ",
"
begin math define pyk of peano c as text "peano c" end text end define end math
then math define tex of peano c as text "
\dot{\mathit{c}}" end text end define end math
end ",
"
begin math define pyk of peano d as text "peano d" end text end define end math
then math define tex of peano d as text "
\dot{\mathit{d}}" end text end define end math
end ",
"
begin math define pyk of peano e as text "peano e" end text end define end math
then math define tex of peano e as text "
\dot{\mathit{e}}" end text end define end math
end ",
"
begin math define pyk of peano f as text "peano f" end text end define end math
then math define tex of peano f as text "
\dot{\mathit{f}}" end text end define end math
end ",
"
begin math define pyk of peano g as text "peano g" end text end define end math
then math define tex of peano g as text "
\dot{\mathit{g}}" end text end define end math
end ",
"
begin math define pyk of peano h as text "peano h" end text end define end math
then math define tex of peano h as text "
\dot{\mathit{h}}" end text end define end math
end ",
"
begin math define pyk of peano i as text "peano i" end text end define end math
then math define tex of peano i as text "
\dot{\mathit{i}}" end text end define end math
end ",
"
begin math define pyk of peano j as text "peano j" end text end define end math
then math define tex of peano j as text "
\dot{\mathit{j}}" end text end define end math
end ",
"
begin math define pyk of peano k as text "peano k" end text end define end math
then math define tex of peano k as text "
\dot{\mathit{k}}" end text end define end math
end ",
"
begin math define pyk of peano l as text "peano l" end text end define end math
then math define tex of peano l as text "
\dot{\mathit{l}}" end text end define end math
end ",
"
begin math define pyk of peano m as text "peano m" end text end define end math
then math define tex of peano m as text "
\dot{\mathit{m}}" end text end define end math
end ",
"
begin math define pyk of peano n as text "peano n" end text end define end math
then math define tex of peano n as text "
\dot{\mathit{n}}" end text end define end math
end ",
"
begin math define pyk of peano o as text "peano o" end text end define end math
then math define tex of peano o as text "
\dot{\mathit{o}}" end text end define end math
end ",
"
begin math define pyk of peano p as text "peano p" end text end define end math
then math define tex of peano p as text "
\dot{\mathit{p}}" end text end define end math
end ",
"
begin math define pyk of peano q as text "peano q" end text end define end math
then math define tex of peano q as text "
\dot{\mathit{q}}" end text end define end math
end ",
"
begin math define pyk of peano r as text "peano r" end text end define end math
then math define tex of peano r as text "
\dot{\mathit{r}}" end text end define end math
end ",
"
begin math define pyk of peano s as text "peano s" end text end define end math
then math define tex of peano s as text "
\dot{\mathit{s}}" end text end define end math
end ",
"
begin math define pyk of peano t as text "peano t" end text end define end math
then math define tex of peano t as text "
\dot{\mathit{t}}" end text end define end math
end ",
"
begin math define pyk of peano u as text "peano u" end text end define end math
then math define tex of peano u as text "
\dot{\mathit{u}}" end text end define end math
end ",
"
begin math define pyk of peano v as text "peano v" end text end define end math
then math define tex of peano v as text "
\dot{\mathit{v}}" end text end define end math
end ",
"
begin math define pyk of peano w as text "peano w" end text end define end math
then math define tex of peano w as text "
\dot{\mathit{w}}" end text end define end math
end ",
"
begin math define pyk of peano x as text "peano x" end text end define end math
then math define tex of peano x as text "
\dot{\mathit{x}}" end text end define end math
end ",
"
begin math define pyk of peano y as text "peano y" end text end define end math
then math define tex of peano y as text "
\dot{\mathit{y}}" end text end define end math
end "
"
begin math define pyk of peano z as text "peano z" end text end define end math
then math define tex of peano z as text "
\dot{\mathit{z}}" end text end define end math
end "
"
begin math define macro of peano b as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano b as var b peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano c as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano c as var c peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano d as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano d as var d peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano e as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano e as var e peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano f as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano f as var f peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano g as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano g as var g peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano h as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano h as var h peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano i as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano i as var i peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano j as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano j as var j peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano k as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano k as var k peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano l as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano l as var l peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano m as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano m as var m peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano n as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano n as var n peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano o as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano o as var o peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano p as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano p as var p peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano q as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano q as var q peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano r as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano r as var r peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano s as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano s as var s peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano t as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano t as var t peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano u as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano u as var u peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano v as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano v as var v peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano w as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano w as var w peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano x as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano x as var x peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano y as var y peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano z as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano z as var z peano var end define end quote end define end define end math
end ".
\subsection{\TeX\ definitions}\label{section:TexDefinitions}
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\immediate\closeout\outex
\input{./page.otx}
\item \mbox{}
\end{list}
\subsection{Test}
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\immediate\closeout\outest
\input{./page.tst}
\item \mbox{}
\end{list}
\subsection{Priority table}\label{section:PriorityTable}
"
begin flush left math define priority of proofreport as preassociative priority proofreport equal priority base equal priority bracket x end bracket equal priority big bracket x end bracket equal priority math x end math equal priority flush left x end left equal priority var x equal priority var y equal priority var z equal priority proclaim x as x end proclaim equal priority define x of x as x end define equal priority pyk equal priority tex equal priority tex name equal priority priority equal priority x equal priority true equal priority if x then x else x end if equal priority introduce x of x as x end introduce equal priority value equal priority claim equal priority bottom equal priority function f of x end function equal priority identity x end identity equal priority false equal priority untagged zero equal priority untagged one equal priority untagged two equal priority untagged three equal priority untagged four equal priority untagged five equal priority untagged six equal priority untagged seven equal priority untagged eight equal priority untagged nine equal priority zero equal priority one equal priority two equal priority three equal priority four equal priority five equal priority six equal priority seven equal priority eight equal priority nine equal priority var a equal priority var b equal priority var c equal priority var d equal priority var e equal priority var f equal priority var g equal priority var h equal priority var i equal priority var j equal priority var k equal priority var l equal priority var m equal priority var n equal priority var o equal priority var p equal priority var q equal priority var r equal priority var s equal priority var t equal priority var u equal priority var v equal priority var w equal priority tagged parenthesis x end tagged equal priority tagged if x then x else x end if equal priority array x is x end array equal priority left equal priority center equal priority right equal priority empty equal priority substitute x set x to x end substitute equal priority map tag x end tag equal priority raw map untag x end untag equal priority map untag x end untag equal priority normalizing untag x end untag equal priority apply x to x end apply equal priority apply one x to x end apply equal priority identifier x end identifier equal priority identifier one x plus id x end identifier equal priority array plus x and x end plus equal priority array remove x array x level x end remove equal priority array put x value x array x level x end put equal priority array add x value x index x value x level x end add equal priority bit x of x end bit equal priority bit one x of x end bit equal priority example rack equal priority vector hook equal priority bibliography hook equal priority dictionary hook equal priority body hook equal priority codex hook equal priority expansion hook equal priority code hook equal priority cache hook equal priority diagnose hook equal priority pyk aspect equal priority tex aspect equal priority texname aspect equal priority value aspect equal priority message aspect equal priority macro aspect equal priority definition aspect equal priority unpack aspect equal priority claim aspect equal priority priority aspect equal priority lambda identifier equal priority apply identifier equal priority true identifier equal priority if identifier equal priority quote identifier equal priority proclaim identifier equal priority define identifier equal priority introduce identifier equal priority hide identifier equal priority pre identifier equal priority post identifier equal priority eval x stack x cache x end eval equal priority eval two x ref x id x stack x cache x end eval equal priority eval three x function x stack x cache x end eval equal priority eval four x arguments x stack x cache x end eval equal priority lookup x stack x default x end lookup equal priority abstract x term x stack x cache x end abstract equal priority quote x end quote equal priority expand x state x cache x end expand equal priority expand two x definition x state x cache x end expand equal priority expand list x state x cache x end expand equal priority macro equal priority macro state equal priority zip x with x end zip equal priority assoc one x address x index x end assoc equal priority protect x end protect equal priority self equal priority macro define x as x end define equal priority value define x as x end define equal priority intro define x as x end define equal priority pyk define x as x end define equal priority tex define x as x end define equal priority tex name define x as x end define equal priority priority table x end table equal priority macro define one equal priority macro define two x end define equal priority macro define three x end define equal priority macro define four x state x cache x definition x end define equal priority state expand x state x cache x end expand equal priority quote expand x term x stack x end expand equal priority quote expand two x term x stack x end expand equal priority quote expand three x term x stack x value x end expand equal priority quote expand star x term x stack x end expand equal priority parenthesis x end parenthesis equal priority aspect x subcodex x end aspect equal priority aspect x term x cache x end aspect equal priority tuple x end tuple equal priority tuple one x end tuple equal priority tuple two x end tuple equal priority let two x apply x end let equal priority let one x apply x end let equal priority claim define x as x end define equal priority checker equal priority check x cache x end check equal priority check two x cache x def x end check equal priority check three x cache x def x end check equal priority check list x cache x end check equal priority check list two x cache x value x end check equal priority test x end test equal priority false test x end test equal priority raw test x end test equal priority message equal priority message define x as x end define equal priority the statement aspect equal priority statement equal priority statement define x as x end define equal priority example axiom equal priority example scheme equal priority example rule equal priority absurdity equal priority contraexample equal priority example theory primed equal priority example lemma equal priority metavar x end metavar equal priority meta a equal priority meta b equal priority meta c equal priority meta d equal priority meta e equal priority meta f equal priority meta g equal priority meta h equal priority meta i equal priority meta j equal priority meta k equal priority meta l equal priority meta m equal priority meta n equal priority meta o equal priority meta p equal priority meta q equal priority meta r equal priority meta s equal priority meta t equal priority meta u equal priority meta v equal priority meta w equal priority meta x equal priority meta y equal priority meta z equal priority sub x set x to x end sub equal priority sub star x set x to x end sub equal priority the empty set equal priority example remainder equal priority make visible x end visible equal priority intro x index x pyk x tex x end intro equal priority intro x pyk x tex x end intro equal priority error x term x end error equal priority error two x term x end error equal priority proof x term x cache x end proof equal priority proof two x term x end proof equal priority sequent eval x term x end eval equal priority seqeval init x term x end eval equal priority seqeval modus x term x end eval equal priority seqeval modus one x term x sequent x end eval equal priority seqeval verify x term x end eval equal priority seqeval verify one x term x sequent x end eval equal priority sequent eval plus x term x end eval equal priority seqeval plus one x term x sequent x end eval equal priority seqeval minus x term x end eval equal priority seqeval minus one x term x sequent x end eval equal priority seqeval deref x term x end eval equal priority seqeval deref one x term x sequent x end eval equal priority seqeval deref two x term x sequent x def x end eval equal priority seqeval at x term x end eval equal priority seqeval at one x term x sequent x end eval equal priority seqeval infer x term x end eval equal priority seqeval infer one x term x premise x sequent x end eval equal priority seqeval endorse x term x end eval equal priority seqeval endorse one x term x side x sequent x end eval equal priority seqeval est x term x end eval equal priority seqeval est one x term x name x sequent x end eval equal priority seqeval est two x term x name x sequent x def x end eval equal priority seqeval all x term x end eval equal priority seqeval all one x term x variable x sequent x end eval equal priority seqeval cut x term x end eval equal priority seqeval cut one x term x forerunner x end eval equal priority seqeval cut two x term x forerunner x sequent x end eval equal priority computably true x end true equal priority claims x cache x ref x end claims equal priority claims two x cache x ref x end claims equal priority the proof aspect equal priority proof equal priority lemma x says x end lemma equal priority proof of x reads x end proof equal priority in theory x lemma x says x end lemma equal priority in theory x antilemma x says x end antilemma equal priority in theory x rule x says x end rule equal priority in theory x antirule x says x end antirule equal priority verifier equal priority verify one x end verify equal priority verify two x proofs x end verify equal priority verify three x ref x sequents x diagnose x end verify equal priority verify four x premises x end verify equal priority verify five x ref x array x sequents x end verify equal priority verify six x ref x list x sequents x end verify equal priority verify seven x ref x id x sequents x end verify equal priority cut x and x end cut equal priority head x end head equal priority tail x end tail equal priority rule one x theory x end rule equal priority rule x subcodex x end rule equal priority rule tactic equal priority plus x and x end plus equal priority theory x end theory equal priority theory two x cache x end theory equal priority theory three x name x end theory equal priority theory four x name x sum x end theory equal priority example axiom lemma primed equal priority example scheme lemma primed equal priority example rule lemma primed equal priority contraexample lemma primed equal priority example axiom lemma equal priority example scheme lemma equal priority example rule lemma equal priority contraexample lemma equal priority example theory equal priority ragged right equal priority ragged right expansion equal priority parameter term x stack x seed x end parameter equal priority parameter term star x stack x seed x end parameter equal priority instantiate x with x end instantiate equal priority instantiate star x with x end instantiate equal priority occur x in x substitution x end occur equal priority occur star x in x substitution x end occur equal priority unify x with x substitution x end unify equal priority unify star x with x substitution x end unify equal priority unify two x with x substitution x end unify equal priority ell a equal priority ell b equal priority ell c equal priority ell d equal priority ell e equal priority ell f equal priority ell g equal priority ell h equal priority ell i equal priority ell j equal priority ell k equal priority ell l equal priority ell m equal priority ell n equal priority ell o equal priority ell p equal priority ell q equal priority ell r equal priority ell s equal priority ell t equal priority ell u equal priority ell v equal priority ell w equal priority ell x equal priority ell y equal priority ell z equal priority ell big a equal priority ell big b equal priority ell big c equal priority ell big d equal priority ell big e equal priority ell big f equal priority ell big g equal priority ell big h equal priority ell big i equal priority ell big j equal priority ell big k equal priority ell big l equal priority ell big m equal priority ell big n equal priority ell big o equal priority ell big p equal priority ell big q equal priority ell big r equal priority ell big s equal priority ell big t equal priority ell big u equal priority ell big v equal priority ell big w equal priority ell big x equal priority ell big y equal priority ell big z equal priority ell dummy equal priority sequent reflexivity equal priority tactic reflexivity equal priority sequent commutativity equal priority tactic commutativity equal priority the tactic aspect equal priority tactic equal priority tactic define x as x end define equal priority proof expand x state x cache x end expand equal priority proof expand list x state x cache x end expand equal priority proof state equal priority conclude one x cache x end conclude equal priority conclude two x proves x cache x end conclude equal priority conclude three x proves x lemma x substitution x end conclude equal priority conclude four x lemma x end conclude equal priority peano zero equal priority peano one equal priority peano two equal priority peano a equal priority peano b equal priority peano c equal priority peano d equal priority peano e equal priority peano f equal priority peano g equal priority peano h equal priority peano i equal priority peano j equal priority peano k equal priority peano l equal priority peano m equal priority peano n equal priority peano o equal priority peano p equal priority peano q equal priority peano r equal priority peano s equal priority peano t equal priority peano u equal priority peano v equal priority peano w equal priority peano x equal priority peano y equal priority peano z equal priority peano nonfree x in x end nonfree equal priority peano nonfree star x in x end nonfree equal priority peano free x set x to x end free equal priority peano free star x set x to x end free equal priority peano sub x is x where x is x end sub equal priority peano sub star x is x where x is x end sub equal priority system prime s equal priority axiom prime a one equal priority axiom prime a two equal priority axiom prime a three equal priority axiom prime a four equal priority axiom prime a five equal priority axiom prime s one equal priority axiom prime s two equal priority axiom prime s three equal priority axiom prime s four equal priority axiom prime s five equal priority axiom prime s six equal priority axiom prime s seven equal priority axiom prime s eight equal priority axiom prime s nine equal priority rule prime mp equal priority rule prime gen equal priority lemma prime l three two a equal priority nani nase kita...:54 equal priority nani nase kita...:55 equal priority nani nase kita...:56 equal priority lemma prime l three two b equal priority lemma prime l three two c equal priority lemma prime l three two d one equal priority lemma prime l three two d two equal priority lemma prime l three two f equal priority lemma prime l three two g equal priority lemma prime l three two h one equal priority lemma prime l three two h two equal priority lemma prime l three two h equal priority nani nase kita...:66 equal priority hypothetical three two d equal priority mendelson corollary one ten a equal priority mendelson corollary one ten b equal priority mendelson corollary one ten pre b equal priority mendelson corollary one ten b plus plus equal priority hypothetical rule prime mp plus plus equal priority hypothesize plus plus equal priority mendelson one seven plus plus equal priority mendelson one seven equal priority hypothetical rule prime mp equal priority hypothesize equal priority hypothetical rule prime gen equal priority mendelson three two a equal priority hypothetical three two a equal priority hypothetical three two b equal priority hypothetical three one s one equal priority hypothetical three two c equal priority hypothetical three one s two equal priority hypothetical three one s five equal priority hypothetical three one s six equal priority mendelson three two f end priority greater than preassociative priority x sub x end sub equal priority x prime equal priority x assoc x end assoc equal priority x set x to x end set equal priority x set multi x to x end set equal priority x peano var end priority greater than preassociative priority unicode start of text x end unicode text equal priority unicode end of text equal priority text x end text equal priority text x plus x equal priority text x plus indent x equal priority
unicode newline x equal priority unicode space x equal priority unicode exclamation mark x equal priority unicode quotation mark x equal priority unicode number sign x equal priority unicode dollar sign x equal priority unicode percent x equal priority unicode ampersand x equal priority unicode apostrophe x equal priority unicode left parenthesis x equal priority unicode right parenthesis x equal priority unicode asterisk x equal priority unicode plus sign x equal priority unicode comma x equal priority unicode hyphen x equal priority unicode period x equal priority unicode slash x equal priority unicode zero x equal priority unicode one x equal priority unicode two x equal priority unicode three x equal priority unicode four x equal priority unicode five x equal priority unicode six x equal priority unicode seven x equal priority unicode eight x equal priority unicode nine x equal priority unicode colon x equal priority unicode semicolon x equal priority unicode less than x equal priority unicode equal sign x equal priority unicode greater than x equal priority unicode question mark x equal priority unicode commercial at x equal priority unicode capital a x equal priority unicode capital b x equal priority unicode capital c x equal priority unicode capital d x equal priority unicode capital e x equal priority unicode capital f x equal priority unicode capital g x equal priority unicode capital h x equal priority unicode capital i x equal priority unicode capital j x equal priority unicode capital k x equal priority unicode capital l x equal priority unicode capital m x equal priority unicode capital n x equal priority unicode capital o x equal priority unicode capital p x equal priority unicode capital q x equal priority unicode capital r x equal priority unicode capital s x equal priority unicode capital t x equal priority unicode capital u x equal priority unicode capital v x equal priority unicode capital w x equal priority unicode capital x x equal priority unicode capital y x equal priority unicode capital z x equal priority unicode left bracket x equal priority unicode backslash x equal priority unicode right bracket x equal priority unicode circumflex x equal priority unicode underscore x equal priority unicode grave accent x equal priority unicode small a x equal priority unicode small b x equal priority unicode small c x equal priority unicode small d x equal priority unicode small e x equal priority unicode small f x equal priority unicode small g x equal priority unicode small h x equal priority unicode small i x equal priority unicode small j x equal priority unicode small k x equal priority unicode small l x equal priority unicode small m x equal priority unicode small n x equal priority unicode small o x equal priority unicode small p x equal priority unicode small q x equal priority unicode small r x equal priority unicode small s x equal priority unicode small t x equal priority unicode small u x equal priority unicode small v x equal priority unicode small w x equal priority unicode small x x equal priority unicode small y x equal priority unicode small z x equal priority unicode left brace x equal priority unicode vertical line x equal priority unicode right brace x equal priority unicode tilde x equal priority preassociative x greater than x equal priority postassociative x greater than x equal priority priority x equal x equal priority priority x end priority equal priority newline x equal priority macro newline x end priority greater than preassociative priority x bit nil equal priority x bit one equal priority binary equal priority x color x end color equal priority x color star x end color end priority greater than preassociative priority x apply x equal priority x tagged apply x end priority greater than preassociative priority x raw head equal priority x raw tail equal priority x cardinal untag equal priority x head equal priority x tail equal priority x is singular equal priority x is cardinal equal priority x is data equal priority x is atomic equal priority x cardinal retract equal priority x tagged retract equal priority x boolean retract equal priority x ref equal priority x id equal priority x debug equal priority x root equal priority x zeroth equal priority x first equal priority x second equal priority x third equal priority x fourth equal priority x fifth equal priority x sixth equal priority x seventh equal priority x eighth equal priority x ninth equal priority x is error equal priority x is metavar equal priority x is metaclosed equal priority x is metaclosed star equal priority x peano succ end priority greater than preassociative priority x times x equal priority x times zero x equal priority x peano times x end priority greater than preassociative priority x plus x equal priority x plus zero x equal priority x plus one x equal priority x minus x equal priority x minus zero x equal priority x minus one x equal priority x peano plus x end priority greater than preassociative priority x term plus x end plus equal priority x term union x equal priority x term minus x end minus end priority greater than postassociative priority x raw pair x equal priority x eager pair x equal priority x tagged pair x equal priority x untagged double x equal priority x pair x equal priority x double x end priority greater than postassociative priority x comma x end priority greater than preassociative priority x boolean equal x equal priority x data equal x equal priority x cardinal equal x equal priority x peano equal x equal priority x tagged equal x equal priority x math equal x equal priority x reduce to x equal priority x term equal x equal priority x term list equal x equal priority x term root equal x equal priority x term in x equal priority x term subset x equal priority x term set equal x equal priority x sequent equal x equal priority x free in x equal priority x free in star x equal priority x free for x in x equal priority x free for star x in x equal priority x claim in x equal priority x less x equal priority x less zero x equal priority x less one x equal priority x peano is x equal priority x is peano var end priority greater than preassociative priority not x equal priority peano not x end priority greater than preassociative priority x and x equal priority x macro and x equal priority x simple and x equal priority x claim and x equal priority x peano and x end priority greater than preassociative priority x or x equal priority x parallel x equal priority x macro or x equal priority x peano or x end priority greater than preassociative priority peano all x indeed x equal priority peano exist x indeed x end priority greater than postassociative priority x macro imply x equal priority x peano imply x equal priority x peano iff x end priority greater than postassociative priority x guard x equal priority x tagged guard x end priority greater than preassociative priority x select x else x end select end priority greater than preassociative priority lambda x dot x equal priority tagging x equal priority open if x then x else x equal priority let x be x in x equal priority let x abbreviate x in x end priority greater than preassociative priority x init equal priority x modus equal priority x verify equal priority x curry plus equal priority x curry minus equal priority x dereference end priority greater than preassociative priority x at x equal priority x modus ponens x equal priority x modus probans x equal priority x conclude x equal priority x macro modus ponens x equal priority x hypothetical modus ponens x end priority greater than postassociative priority x infer x equal priority x endorse x equal priority x id est x end priority greater than preassociative priority all x indeed x end priority greater than postassociative priority x rule plus x end priority greater than postassociative priority x cut x end priority greater than preassociative priority x proves x end priority greater than preassociative priority x proof of x reads x equal priority line x because x indeed x end line x equal priority because x indeed x qed equal priority line x premise x end line x equal priority line x side condition x end line x equal priority arbitrary x end line x equal priority locally define x as x end line x end priority greater than postassociative priority x
then x equal priority x
begin x
end x end priority greater than preassociative priority x tab x end priority greater than preassociative priority x row
x end priority greater than unicode end of text end define end math end left
end "
\section{Index}
\newcommand\myidxitem{\par\noindent}
\renewenvironment{theindex}{\let\item\myidxitem}{}
\printindex
\section{Bibliografi}
\bibliography{./page}
\section{Pyk kildetekst}
\end{document}
End of file
File page.bib
@article {berline97,
author = {C. Berline and K. Grue},
title = {A $\kappa$-denotational semantics for {M}ap {T}heory
in {ZFC+SI}},
journal = TCS,
year = {1997},
volume = {179},
number = {1--2},
pages = {137--202},
month = {jun}}
@book {church41,
author = {A. Church},
title = {The Calculi of Lambda-Conversion},
publisher = {Princeton University Press},
year = {1941}}
@Article {godel,
author = {K. G{\"!o}del},
title = {{\"!U}ber for\-mal un\-ent\-scheid\-ba\-re
\mbox{S\"!at}\-ze der \mbox{Prin}\-ci\-pia
\mbox{Mathe}\-ma\-ti\-ca und ver\-wand\-ter
\mbox{Sys}\-teme \mbox{I}},
journal = {Mo\-nats\-hef\-te f{\"!u}r Mathe\-ma\-tik und Phy\-sik},
year = {19\-31},
volume = {12},
number = {\mbox{XXXVIII}},
pages = {173-198}}
@book {Gordon79,
author = {M. J. Gordon, A. J. Milner, C. P. Wadsworth},
title = {Edinburgh {LCF}, A mechanised logic of computation},
publisher = {Springer-Verlag},
year = {1979},
volume = {78},
series = {Lecture Notes in Computer Science}}
@article {grue92,
author = {K. Grue},
title = {Map Theory},
journal = TCS,
year = {1992},
volume = {102},
number = {1},
pages = {1--133},
month = {jul}}
@inproceedings{Logiweb,
author = {K. Grue},
title = {Logiweb},
editor = {Fairouz Kamareddine},
booktitle = {Mathematical Knowledge Management Symposium 2003},
publisher = {Elsevier},
series = {Electronic Notes in Theoretical Computer Science},
volume = {93},
year = {2004},
pages = {70--101}}
@article {mccarthy60,
author = {J. McCarthy},
title = {Recursive functions of symbolic expressions and their
computation by machine},
journal = {Communications of the ACM},
year = {1960},
pages = {184--195}}
@book {mendelson,
author = {E. Mendelson},
title = {Introduction to Mathematical Logic},
publisher = {Wadsworth and Brooks},
year = {1987},
edition = {3.}}
@book {TeXbook,
author = {D. Knuth},
title = {The TeXbook},
publisher = {Addison Wesley},
year = {1983}}
End of file
File page.sty
% thebibliography environment from
% /usr/share/texmf/tex/latex/base/book.cls
% with \chapter removed
\renewenvironment{thebibliography}[1]
{\list{\@biblabel{\@arabic\c@enumiv}}%
{\settowidth\labelwidth{\@biblabel{#1}}%
\leftmargin\labelwidth
\advance\leftmargin\labelsep
\@openbib@code
\usecounter{enumiv}%
\let\p@enumiv\@empty
\renewcommand\theenumiv{\@arabic\c@enumiv}}%
\sloppy
\clubpenalty4000
\@clubpenalty \clubpenalty
\widowpenalty4000%
\sfcode`\.\@m}
{\def\@noitemerr
{\@latex@warning{Empty `thebibliography' environment}}%
\endlist}
End of file
latex page
makeindex page
bibtex page
latex page
makeindex page
latex page"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,