{ Logiweb, a system for electronic distribution of mathematics Copyright (C) 2004 Klaus Grue This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307 USA Contact: Klaus Grue, DIKU, Universitetsparken 1, DK2100 Copenhagen, Denmark, grue@diku.dk, http://yoa.dk/, http://www.diku.dk/~grue/ Logiweb is a system for distribution of mathematical definitions, lemmas, and proofs. For more on Logiweb, consult http://yoa.dk/. } PAGE proofreport BIBLIOGRAPHY base: nani tesu teke kitu tate suke tena kusu kiku suti nase kite tise sini tetu tasi keti kuku tani keta tune senu kunu sene kinu sene kuku sise nasa natu PREASSOCIATIVE base: bracket * end bracket, peano zero, peano one, peano two, peano a, peano b, peano c, peano d, peano e, peano f, peano g, peano h, peano i, peano j, peano k, peano l, peano m, peano n, peano o, peano p, peano q, peano r, peano s, peano t, peano u, peano v, peano w, peano x, peano y, peano z, peano nonfree * in * end nonfree, peano nonfree star * in * end nonfree, peano free * set * to * end free, peano free star * set * to * end free, peano sub * is * where * is * end sub, peano sub star * is * where * is * end sub, system prime s, axiom prime a one, axiom prime a two, axiom prime a three, axiom prime a four, axiom prime a five, axiom prime s one, axiom prime s two, axiom prime s three, axiom prime s four, axiom prime s five, axiom prime s six, axiom prime s seven, axiom prime s eight, axiom prime s nine, rule prime mp, rule prime gen, lemma prime l three two a, tautology one, tautology two, tautology three, lemma prime l three two b, lemma prime l three two c, lemma prime l three two d one, lemma prime l three two d two, lemma prime l three two f, lemma prime l three two g, lemma prime l three two h one, lemma prime l three two h two, lemma prime l three two h, hypothetical three two g, hypothetical three two d, mendelson corollary one ten a, mendelson corollary one ten b, mendelson corollary one ten pre b, mendelson corollary one ten b plus plus, hypothetical rule prime mp plus plus, hypothesize plus plus, mendelson one seven plus plus, mendelson one seven, hypothetical rule prime mp, hypothesize, hypothetical rule prime gen, mendelson three two a, hypothetical three two a, hypothetical three two b, hypothetical three one s one, hypothetical three two c, hypothetical three one s two, hypothetical three one s five, hypothetical three one s six, mendelson three two f PREASSOCIATIVE base: * sub * end sub, * peano var PREASSOCIATIVE base: unicode start of text * end unicode text PREASSOCIATIVE base: * bit nil PREASSOCIATIVE base: * apply * PREASSOCIATIVE base: * raw head, * peano succ PREASSOCIATIVE base: * times *, * peano times * PREASSOCIATIVE base: * plus *, * peano plus * PREASSOCIATIVE base: * term plus * end plus POSTASSOCIATIVE base: * raw pair * POSTASSOCIATIVE base: * comma * PREASSOCIATIVE base: * boolean equal *, * peano is *, * is peano var PREASSOCIATIVE base: not *, peano not * PREASSOCIATIVE base: * and *, * peano and * PREASSOCIATIVE base: * or *, * peano or * PREASSOCIATIVE peano all * indeed *, peano exist * indeed * POSTASSOCIATIVE base: * macro imply *, * peano imply *, * peano iff * POSTASSOCIATIVE base: * guard * PREASSOCIATIVE base: * select * else * end select PREASSOCIATIVE base: lambda * dot * PREASSOCIATIVE base: * init PREASSOCIATIVE base: * at *, * macro modus ponens *, * hypothetical modus ponens * POSTASSOCIATIVE base: * infer * PREASSOCIATIVE base: all * indeed * POSTASSOCIATIVE base: * rule plus * POSTASSOCIATIVE base: * cut * PREASSOCIATIVE base: * proves * PREASSOCIATIVE base: locally define * as * end line * POSTASSOCIATIVE base: * then * PREASSOCIATIVE base: * tab * PREASSOCIATIVE base: * row * BODY "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 "[ ragged right expansion ]" \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 "[ bracket peano x peano plus peano y peano is peano y peano plus peano x end bracket]" 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 "[ bracket peano all peano x indeed peano all peano y indeed peano x peano plus peano y peano is peano y peano plus peano x end bracket ]". 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: "[ bracket peano a end bracket]" - "[ bracket peano z end bracket]". "[ intro peano zero pyk "peano zero" tex " \dot{0}" end intro ]" svarer til symbolet nul. Alle andre tal defineres induktivt som efterf\o lgere "[ intro var x peano succ pyk "* peano succ" tex "#1.'" end intro ]", af hinanden. \item Derudover kan termer indeholde plus "[ intro var x peano plus var y pyk "* peano plus *" tex "#1. \mathop{\dot{+}} #2." end intro ]" \item Gange "[ intro var x peano times var y pyk "* peano times *" tex "#1. \mathop{\dot{\cdot}} #2." end intro ]". \end{itemize} \subsubsection{Formularer} Formularer er opbygget af: \begin{itemize} \item Lighed "[ intro var x peano is var y index "p" pyk "* peano is *" tex "#1. \stackrel{p}{=} #2." end intro ]" mellem termer. \item Negation "[ intro peano not var x pyk "peano not *" tex " \dot{\neg}\, #1." end intro ]" af en formular \item Implikation "[ intro var x peano imply var y pyk "* peano imply *" tex "#1. \mathrel{\dot{\Rightarrow}} #2." end intro ]" mellem formularer. \item universel kvantifisering "[ intro peano all var x indeed var y pyk "peano all * indeed *" tex " \dot{\forall} #1. \colon #2." end intro ]" 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: "[ intro peano one pyk "peano one" tex " \dot{1}" end intro ]" som \display{"[ math macro define peano one as peano zero peano succ end define end math ]"} \item To: "[ intro peano two pyk "peano two" tex " \dot{2}" end intro ]" som \display{"[ math macro define peano two as peano one peano succ end define end math ]"} \item Logisk og: "[ intro var x peano and var y pyk "* peano and *" tex "#1. \mathrel{\dot{\wedge}} #2." end intro ]" som \display{"[ math 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 math ]"} \item Logisk eller: "[ intro var x peano or var y pyk "* peano or *" tex "#1. \mathrel{\dot{\vee}} #2." end intro ]" som \display{"[ math macro define var x peano or var y as peano not var x peano imply var y end define end math ]"} \item Biimplikation: "[ intro var x peano iff var y pyk "* peano iff *" tex "#1. \mathrel{\dot{\Leftrightarrow}} #2." end intro ]" som \display{"[ math 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 math ]"} \item Eksistens: "[ intro peano exist var x indeed var y pyk "peano exist * indeed *" tex " \dot{\exists} #1. \colon #2." end intro ]" som \display{"[ math macro define peano exist var x indeed var y as peano not peano all var x indeed peano not var y end define end math ]"} \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 "[ intro system prime s index "S'" pyk "system prime s" tex " S'" end intro ]" \display{"[ math theory system prime s end theory end math ]"} \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. "[ intro axiom prime a one index "A1'" pyk "axiom prime a one" tex " A1'" end intro ]", "[ intro axiom prime a two index "A2'" pyk "axiom prime a two" tex " A2'" end intro ]", "[ intro axiom prime a three index "A3'" pyk "axiom prime a three" tex " A3'" end intro ]", "[ intro axiom prime a four index "A4'" pyk "axiom prime a four" tex " A4'" end intro ]", og "[ intro axiom prime a five index "A5'" pyk "axiom prime a five" tex " A5'" end intro ]" \display{"[ math in theory system prime s rule axiom prime a one says all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime a two says all meta a indeed all meta b indeed all meta c indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime a three says all meta a indeed all meta b indeed parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime a four says all meta c indeed all meta a indeed all meta x indeed all meta b indeed peano sub quote meta a end quote is quote meta b end quote where quote meta x end quote is quote meta c end quote end sub endorse peano all meta x indeed meta b peano imply meta a end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime a five says all meta x indeed all meta a indeed all meta b indeed peano nonfree quote meta x end quote in quote meta a end quote end nonfree endorse peano all meta x indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply peano all meta x indeed meta b end rule end math ]"} B\aa de axiom A4 og A5 har sidebetingelser for deres anvendelse. A4s sidebetingelse kr\ae ver at "[ bracket meta c end bracket]" er fri for "[ bracket meta x end bracket]" i "[ bracket meta b end bracket]". "[ bracket meta x end bracket]" kan eventuelt v\ae re lig "[ bracket meta c end bracket]" A5s sidebetingelser er at der ikke findes nogen frie forekomster af "[ bracket meta x end bracket]" i "[ bracket meta a end bracket]". \subsubsection{Slutningsregler} De to slutningsregler Peano aritmetik er: "[ intro rule prime mp index "MP'" pyk "rule prime mp" tex " MP'" end intro ]" og "[ intro rule prime gen index "Gen'" pyk "rule prime gen" tex " Gen'" end intro ]" \display{"[ math in theory system prime s rule rule prime mp says all meta a indeed all meta b indeed meta a peano imply meta b infer meta a infer meta b end rule end math ]"} \display{"[ math in theory system prime s rule rule prime gen says all meta x indeed all meta a indeed meta a infer peano all meta x indeed meta a end rule end math ]"} 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 "[ bracket meta b end bracket ]" n\aa r man allerede har vist "[ bracket meta a peano imply meta b end bracket]" hvis man allerede har vist "[ bracket meta a end bracket ]". Jeg vil senere komme ind p\aa \space hvorledes man kan konstruere et bevis for at "[ bracket meta a peano imply meta b end bracket]" n\aa r man har et bevis for "[ bracket meta a infer meta b end bracket]". 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 "[ bracket meta i peano imply meta h peano imply meta a end bracket ]" ) 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. "[ intro axiom prime s one index "S1'" pyk "axiom prime s one" tex " S1'" end intro ]", "[ intro axiom prime s two index "S2'" pyk "axiom prime s two" tex " S2'" end intro ]", "[ intro axiom prime s three index "S3'" pyk "axiom prime s three" tex " S3'" end intro ]", "[ intro axiom prime s four index "S4'" pyk "axiom prime s four" tex " S4'" end intro ]", "[ intro axiom prime s five index "S5'" pyk "axiom prime s five" tex " S5'" end intro ]", "[ intro axiom prime s six index "S6'" pyk "axiom prime s six" tex " S6'" end intro ]", "[ intro axiom prime s seven index "S7'" pyk "axiom prime s seven" tex " S7'" end intro ]", "[ intro axiom prime s eight index "S8'" pyk "axiom prime s eight" tex " S8'" end intro ]", "[ intro axiom prime s nine index "S9'" pyk "axiom prime s nine" tex " S9'" end intro ]". \display{"[ math in theory system prime s rule axiom prime s one says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta a peano is meta c peano imply meta b peano is meta c end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s two says all meta a indeed all meta b indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s three says all meta a indeed not peano zero peano is meta a peano succ end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s four says all meta a indeed all meta b indeed meta a peano succ peano is meta b peano succ peano imply meta a peano is meta b end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s five says all meta a indeed meta a peano plus peano zero peano is meta a end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s six says all meta a indeed all meta b indeed meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s seven says all meta a indeed meta a peano times peano zero peano is peano zero end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s eight says all meta a indeed all meta b indeed meta a peano times parenthesis meta b peano succ end parenthesis peano is parenthesis meta a peano times meta b end parenthesis peano plus meta a end rule end math ]"} \display{"[ math in theory system prime s rule axiom prime s nine says all meta a indeed all meta b indeed all meta c indeed all meta x indeed macro newline peano sub meta b is meta a where meta x is peano zero end sub endorse peano sub meta c is meta a where meta x is meta x peano succ end sub endorse macro newline meta b peano imply peano all meta x indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta x indeed meta a end rule end math ]"} \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)} "[ intro lemma prime l three two a index "L3.2(a)'" pyk "lemma prime l three two a" tex "L3.2(a)'" end intro ]" 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: "[ intro mendelson three two a index "M3.2(a)" pyk "mendelson three two a" tex " M3.2(a)" end intro ]" \statement{"[ math in theory system prime s lemma lemma prime l three two a says all meta a indeed meta a peano is meta a end lemma end math ]"} \statement{"[ math system prime s proof of lemma prime l three two a reads arbitrary meta a end line line ell b because axiom prime s five indeed meta a peano plus peano zero peano is meta a end line line ell c because axiom prime s one indeed meta a peano plus peano zero peano is meta a peano imply macro newline meta a peano plus peano zero peano is meta a peano imply meta a peano is meta a end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed meta a peano plus peano zero peano is meta a peano imply meta a peano is meta a end line because rule prime mp modus ponens ell d modus ponens ell b indeed meta a peano is meta a qed end math ]"} Den allerf\o rste linje siger at beviset g\ae lder for vilk\aa rlige "[ bracket meta a end bracket ]". Linje 2 og 3 instantierer axiomerne S5 og S1. Bem\ae rk at for linje S1 i linje 3 er "[ bracket meta c end bracket]" og "[ bracket meta b end bracket]" valgt lig "[ bracket meta a end bracket]" 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 "[ bracket parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta b peano imply meta a peano imply meta c end parenthesis end bracket ]", men som det kan ses af beviset er der benyttet en lidt anden s\ae tning. "[ intro lemma prime l three two b index "M3.2(b)" pyk " lemma prime l three two b" tex "M3.2(b)" end intro ]" \statement{"[ math in theory system prime s lemma lemma prime l three two b says all meta t indeed all meta r indeed meta t peano is meta r peano imply meta r peano is meta t end lemma end math ]"} \statement{"[ math system prime s proof of lemma prime l three two b reads arbitrary meta t end line arbitrary meta r end line line ell a because axiom prime s one indeed meta t peano is meta r peano imply meta t peano is meta t peano imply meta r peano is meta t end line line ell b because lemma prime l three two a indeed meta t peano is meta t end line because mendelson corollary one ten b modus ponens ell a modus ponens ell b indeed meta t peano is meta r peano imply meta r peano is meta t qed end math]"} Den afg\o rende observation her er at tautologien ovenfor essentielt svarer til M1.10(b), der udsiger "[ bracket meta a peano imply meta b peano imply meta c infer meta b infer meta a peano imply meta b end bracket ]". 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: "[ intro mendelson corollary one ten pre b index "mendelson corollary one ten pre b" pyk "mendelson corollary one ten pre b" tex " M1.10(b_-)" end intro ]" \statement{"[ math in theory system prime s lemma mendelson corollary one ten pre b says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta b infer meta a infer meta c end lemma end math ]"} \statement{"[ math system prime s proof of mendelson corollary one ten pre b reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b peano imply meta c end line line ell b premise meta b end line line ell c premise meta a end line line ell d because ell a macro modus ponens ell c indeed meta b peano imply meta c end line because ell d macro modus ponens ell b indeed meta c qed end math]"} 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 "[ bracket meta b infer meta c end bracket ]" ikke benyttes Gen p\aa \space en linje som afh\ae nger af "[ bracket meta b end bracket ]" s\aa ledes at den kvantifiserede variabel er en af "[ bracket meta b end bracket ]"s frie variable. Da eksisterer et bevis for "[ bracket meta b peano imply meta c end bracket ]" 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 "[ bracket meta h end bracket ]" 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 "[ bracket meta h peano imply meta h end bracket ]", hvor de 5 linjer svarer til beviset for "[ bracket mendelson one seven end bracket ]" \item En linje best\aa ende af et axiom p\aa \space formen "[ bracket meta a end bracket]" erstattes af tre linjer, der viser at "[ bracket meta h peano imply meta a end bracket ]" med to linjer der svarer til "[ bracket hypothesize end bracket ]" samt det oprindelige axiom. \item Tilsvarende erstattes en linje med modus ponens der virker ved "[ bracket meta a peano imply meta b infer meta a infer meta b end bracket ]" med 3 linjer, der udf\o rer "[ bracket meta h peano imply meta a peano imply meta b infer meta h peano imply meta a infer meta h peano imply meta b end bracket ]" svarende til "[ bracket hypothetical rule prime mp end bracket]".. \item En linje med Gen erstattes af 3 linjer, der erstatter "[ bracket peano all meta x indeed meta a end bracket ]" med "[ bracket meta h peano imply peano all meta x indeed meta a end bracket]" svarende til "[ bracket hypothetical rule prime gen end bracket]". \item For hver linje over hypotesen tilf\o jes 2 linjer svarende til "[ bracket hypothesize end bracket ]". \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 "[ intro mendelson one seven index "M1.7" pyk "mendelson one seven" tex " M1.7" end intro ]", svarer til M1.7 og udsiger: \statement{"[ math in theory system prime s lemma mendelson one seven says all meta b indeed meta b peano imply meta b end lemma end math ]"} \statement{"[ math system prime s proof of mendelson one seven reads arbitrary meta b end line line ell a because axiom prime a one indeed meta b peano imply parenthesis meta b peano imply meta b end parenthesis peano imply meta b end line line ell c because axiom prime a two indeed parenthesis meta b peano imply parenthesis meta b peano imply meta b end parenthesis peano imply meta b end parenthesis peano imply macro newline parenthesis meta b peano imply meta b peano imply meta b end parenthesis peano imply meta b peano imply meta b end line line ell d because ell c macro modus ponens ell a indeed parenthesis meta b peano imply meta b peano imply meta b end parenthesis peano imply meta b peano imply meta b end line line ell b because axiom prime a one indeed meta b peano imply meta b peano imply meta b end line because ell d macro modus ponens ell b indeed meta b peano imply meta b qed end math ]"} \subsubsection{Hypothetitisk modus ponens} Hypotetisk modus ponens "[ intro hypothetical rule prime mp index "MP" pyk "hypothetical rule prime mp" tex " MP'_h" end intro ]" tillader brugen af modus ponens 'bag' en hypotese. Dvs. begge foruds\ae tninger samt konklusionen har den samme hypotese. \statement{"[ math in theory system prime s lemma hypothetical rule prime mp says all meta h indeed all meta a indeed all meta b indeed meta h peano imply meta a peano imply meta b infer meta h peano imply meta a infer meta h peano imply meta b end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical rule prime mp reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line line ell a premise meta h peano imply meta a peano imply meta b end line line ell b premise meta h peano imply meta a end line line ell c because axiom prime a two indeed parenthesis meta h peano imply meta a peano imply meta b end parenthesis peano imply parenthesis meta h peano imply meta a end parenthesis peano imply meta h peano imply meta b end line line ell d because ell c macro modus ponens ell a indeed parenthesis meta h peano imply meta a end parenthesis peano imply meta h peano imply meta b end line because ell d macro modus ponens ell b indeed meta h peano imply meta b qed end math ]"} Hvor de tre sidste linjer er dem, der blev n\ae vnt i algoritmen. \subsubsection{Tilf\o j hypotese} Lemma "[ intro hypothesize index "hypothesize" pyk "hypothesize" tex " Tilf\o j hypotese" end intro ]" tillader som tilf\o je en vilk\aa rlig hypotese til foruds\ae tningen: \statement{"[ math in theory system prime s lemma hypothesize says all meta h indeed all meta a indeed meta a infer meta h peano imply meta a end lemma end math ]"} \statement{"[ math system prime s proof of hypothesize reads arbitrary meta h end line arbitrary meta a end line line ell a premise meta a end line line ell b because axiom prime a one indeed meta a peano imply meta h peano imply meta a end line because ell b macro modus ponens ell a indeed meta h peano imply meta a qed end math ]"} 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 "[ intro hypothetical rule prime gen index "Gen" pyk "hypothetical rule prime gen" tex " Gen'_h" end intro ]" tillader som ved hypotetisk modus ponens at man kan benytte "[ math rule prime gen end math ]" 'bag' en foranst\aa ende hypotese "[ math meta h end math ]": \statement{"[ math in theory system prime s lemma hypothetical rule prime gen says all meta h indeed all meta x indeed all meta a indeed peano nonfree quote meta x end quote in quote meta h end quote end nonfree endorse meta h peano imply meta a infer meta h peano imply peano all meta x indeed meta a end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical rule prime gen reads arbitrary meta h end line arbitrary meta x end line arbitrary meta a end line line ell a side condition peano nonfree quote meta x end quote in quote meta h end quote end nonfree end line line ell b premise meta h peano imply meta a end line line ell c because axiom prime a five modus probans ell a indeed peano all meta x indeed parenthesis meta h peano imply meta a end parenthesis peano imply meta h peano imply peano all meta x indeed meta a end line line ell d because rule prime gen modus ponens ell b indeed peano all meta x indeed parenthesis meta h peano imply meta a end parenthesis end line because ell c macro modus ponens ell d indeed meta h peano imply peano all meta x indeed meta a qed end math ]"} 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 "[ intro mendelson corollary one ten b index "mendelson corollary one ten b" pyk "mendelson corollary one ten b" tex " M1.10(b)" end intro ]". 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{"[ math in theory system prime s lemma mendelson corollary one ten b says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta b infer meta a peano imply meta c end lemma end math ]"} Det resulterende bevis er oversat linje for linje fra M1.10(pre-b)med de ovenst\aa ende regler: \statement{"[ math system prime s proof of mendelson corollary one ten b reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line locally define meta h as meta a end line line ell a premise meta a peano imply meta b peano imply meta c end line line ell b premise meta b end line line ell c because hypothesize modus ponens ell a indeed meta h peano imply meta a peano imply meta b peano imply meta c end line line ell d because hypothesize modus ponens ell b indeed meta h peano imply meta b end line line ell e because mendelson one seven indeed meta h peano imply meta a end line line ell f because ell c hypothetical modus ponens ell e indeed meta h peano imply meta b peano imply meta c end line because ell f hypothetical modus ponens ell d indeed meta h peano imply meta c qed end math]"} 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 "[ bracket meta a end bracket]" er identisk med "[ bracket meta h end bracket]" konkluderer den f\o rste modus ponens at "[ bracket meta a peano imply meta b peano imply meta c end bracket ]" 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: "[ intro lemma prime l three two c index "M3.2(c)" pyk " lemma prime l three two c" tex "M3.2(c)" end intro ]" \statement{"[ math in theory system prime s lemma lemma prime l three two c says all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end lemma end math ]"} \statement{"[ math system prime s proof of lemma prime l three two c reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a because axiom prime s one indeed meta r peano is meta t peano imply meta r peano is meta s peano imply meta t peano is meta s end line line ell b because lemma prime l three two b indeed meta t peano is meta r peano imply meta r peano is meta t end line because mendelson corollary one ten a modus ponens ell b modus ponens ell a indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s qed end math]"} 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). "[ intro mendelson corollary one ten a index "M1.10(a)" pyk " mendelson corollary one ten a " tex "M1.10(a)" end intro ]" \statement{"[ math in theory system prime s lemma mendelson corollary one ten a says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b infer meta b peano imply meta c infer meta a peano imply meta c end lemma end math ]"} \statement{"[ math system prime s proof of mendelson corollary one ten a reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b end line line ell b premise meta b peano imply meta c end line locally define meta h as meta a end line line ell c because mendelson one seven indeed meta h peano imply meta a end line line ell d because hypothesize modus ponens ell a indeed meta h peano imply meta a peano imply meta b end line line ell e because hypothesize modus ponens ell b indeed meta h peano imply meta b peano imply meta c end line line ell f because ell d hypothetical modus ponens ell c indeed meta h peano imply meta b end line because ell e hypothetical modus ponens ell f indeed meta h peano imply meta c qed end math]"} 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 "[ bracket meta s peano is meta t peano imply meta r peano is meta t peano imply meta r peano is meta s end bracket]", mens det han oprindelig kalder M3.2(d) er "[ bracket meta r peano is meta t peano imply meta s peano is meta t peano imply meta r peano is meta s end bracket]". 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{"[ math in theory system prime s lemma lemma prime l three two d one says all meta t indeed all meta r indeed all meta s indeed meta s peano is meta t peano imply meta r peano is meta t peano imply meta r peano is meta s end lemma end math ]"} "[ intro lemma prime l three two d one index "M3.2(d) (I)" pyk " lemma prime l three two d one" tex "M3.2(d) (I)" end intro ]" \statement{"[ math system prime s proof of lemma prime l three two d one reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a because lemma prime l three two c indeed meta r peano is meta t peano imply meta t peano is meta s peano imply meta r peano is meta s end line line ell b because mendelson corollary one ten b plus plus modus ponens ell a indeed meta t peano is meta s peano imply meta r peano is meta t peano imply meta r peano is meta s end line line ell d because lemma prime l three two b indeed meta s peano is meta t peano imply meta t peano is meta s end line because mendelson corollary one ten a modus ponens ell d modus ponens ell b indeed meta s peano is meta t peano imply meta r peano is meta t peano imply meta r peano is meta s qed end math]"} 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 "[ bracket meta t peano is meta t end bracket ]") 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 "[ intro hypothesize plus plus index "hypothesize plus plus" pyk "hypothesize plus plus" tex " Tilf\o j hypotese_+" end intro ]" tillader som tilf\o je en vilk\aa rlig hypotese til foruds\ae tningen \statement{"[ math in theory system prime s lemma hypothesize plus plus says all meta i indeed all meta h indeed all meta a indeed meta a infer meta i peano imply meta h peano imply meta a end lemma end math ]"} \statement{"[ math system prime s proof of hypothesize plus plus reads arbitrary meta i end line arbitrary meta h end line arbitrary meta a end line line ell a premise meta a end line line ell b because hypothesize modus ponens ell a indeed meta h peano imply meta a end line because hypothesize modus ponens ell b indeed meta i peano imply meta h peano imply meta a qed end math ]"} 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 "[ intro hypothetical rule prime mp plus plus index "MP" pyk "hypothetical rule prime mp plus plus" tex " MP'_h+" end intro ]" \statement{"[ math in theory system prime s lemma hypothetical rule prime mp plus plus says all meta i indeed all meta h indeed all meta a indeed all meta b indeed meta i peano imply meta h peano imply meta a peano imply meta b infer meta i peano imply meta h peano imply meta a infer meta i peano imply meta h peano imply meta b end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical rule prime mp plus plus reads arbitrary meta i end line arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line line ell a premise meta i peano imply meta h peano imply meta a peano imply meta b end line line ell b premise meta i peano imply meta h peano imply meta a end line line ell c because axiom prime a two indeed parenthesis meta h peano imply meta a peano imply meta b end parenthesis peano imply parenthesis meta h peano imply meta a end parenthesis peano imply meta h peano imply meta b end line line ell z because hypothesize modus ponens ell c indeed meta i peano imply parenthesis meta h peano imply meta a peano imply meta b end parenthesis peano imply parenthesis meta h peano imply meta a end parenthesis peano imply meta h peano imply meta b end line line ell d because ell z hypothetical modus ponens ell a indeed meta i peano imply parenthesis meta h peano imply meta a end parenthesis peano imply meta h peano imply meta b end line because ell d hypothetical modus ponens ell b indeed meta i peano imply meta h peano imply meta b qed end math ]"} 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 "[ bracket meta b end bracket ]" som en hypotese. Husk at hvis der i det oprindelige bevis er blevet benyttet "[ bracket meta b end bracket ]" vil der efter f\o rste genneml\o b af algoritmen v\ae re en 'Tilf\o j hypotese' der fort\ae ller at "[ bracket meta a peano imply meta b end bracket ]". Men n\aa r foruds\ae tningen "[ bracket meta b end bracket ]" 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: "[ intro mendelson one seven plus plus index "mendelson one seven plus plus" pyk "mendelson one seven plus plus" tex " M1.7_+" end intro ]". \statement{"[ math in theory system prime s lemma mendelson one seven plus plus says all meta a indeed all meta b indeed meta b peano imply meta a peano imply meta b end lemma end math ]"} \statement{"[ math system prime s proof of mendelson one seven plus plus reads arbitrary meta a end line arbitrary meta b end line line ell a because mendelson one seven indeed meta b peano imply meta b end line line ell b because axiom prime a one indeed meta b peano imply meta a peano imply meta b end line line ell c because hypothesize modus ponens ell b indeed meta b peano imply meta b peano imply meta a peano imply meta b end line because ell c hypothetical modus ponens ell a indeed meta b peano imply meta a peano imply meta b qed end math]"} 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 "[ bracket meta c peano imply meta b peano imply meta a peano imply meta c end bracket]" som kan vises med udgangspunkt i M1.7++ . For nu at vende tilbage til udgangspunktet: Lemma "[ intro mendelson corollary one ten b plus plus index "M1.10(b+)" pyk "mendelson corollary one ten b plus plus" tex " M1.10(b_+)" end intro ]" \statement{"[ math in theory system prime s lemma mendelson corollary one ten b plus plus says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta b peano imply meta a peano imply meta c end lemma end math ]"} \statement{"[ math system prime s proof of mendelson corollary one ten b plus plus reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b peano imply meta c end line line ell b because mendelson one seven plus plus indeed meta b peano imply meta a peano imply meta b end line line ell c because mendelson one seven indeed meta a peano imply meta a end line line ell d because hypothesize modus ponens ell c indeed meta b peano imply meta a peano imply meta a end line line ell e because hypothesize plus plus modus ponens ell a indeed meta b peano imply meta a peano imply meta a peano imply meta b peano imply meta c end line line ell f because hypothetical rule prime mp plus plus modus ponens ell e modus ponens ell d indeed meta b peano imply meta a peano imply meta b peano imply meta c end line because hypothetical rule prime mp plus plus modus ponens ell f modus ponens ell b indeed meta b peano imply meta a peano imply meta c qed end math]"} Hermed er beviset for s\ae tning M3.2(d)(I). S\ae tning M3.2(d)(II) f\o lger umiddelbart: \statement{"[ math in theory system prime s lemma lemma prime l three two d two says all meta t indeed all meta r indeed all meta s indeed meta r peano is meta t peano imply meta s peano is meta t peano imply meta r peano is meta s end lemma end math ]"} "[ intro lemma prime l three two d two index "M3.2(d) (II)" pyk " lemma prime l three two d two" tex "M3.2(d) (II)" end intro ]" \statement{"[ math system prime s proof of lemma prime l three two d two reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a because lemma prime l three two d one indeed meta s peano is meta t peano imply meta r peano is meta t peano imply meta r peano is meta s end line because mendelson corollary one ten b plus plus modus ponens ell a indeed meta r peano is meta t peano imply meta s peano is meta t peano imply meta r peano is meta s qed end math]"} 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. "[ intro hypothetical three two a index "M3.2(a)" pyk "hypothetical three two a" tex " M3.2(a)_h" end intro ]" \statement{"[ math in theory system prime s lemma hypothetical three two a says all meta h indeed all meta t indeed meta h peano imply meta t peano is meta t end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical three two a reads arbitrary meta h end line arbitrary meta t end line line ell a because lemma prime l three two a indeed meta t peano is meta t end line because hypothesize modus ponens ell a indeed meta h peano imply meta t peano is meta t qed end math ]"} "[ intro hypothetical three two b index "M3.2(b)" pyk "hypothetical three two b" tex " M3.2(b)_h" end intro ]" \statement{"[ math in theory system prime s rule hypothetical three two b says all meta h indeed all meta t indeed all meta r indeed meta h peano imply meta t peano is meta r infer meta h peano imply meta r peano is meta t end rule end math ]"} \statement{"[ math system prime s proof of hypothetical three two b reads arbitrary meta h end line arbitrary meta t end line arbitrary meta r end line line ell a premise meta h peano imply meta t peano is meta r end line line ell b because axiom prime s one indeed meta t peano is meta r peano imply meta t peano is meta t peano imply meta r peano is meta t end line line ell c because hypothesize modus ponens ell b indeed meta h peano imply meta t peano is meta r peano imply meta t peano is meta t peano imply meta r peano is meta t end line line ell d because ell c hypothetical modus ponens ell a indeed meta h peano imply meta t peano is meta t peano imply meta r peano is meta t end line line ell e because hypothetical three two a indeed meta h peano imply meta t peano is meta t end line because ell d hypothetical modus ponens ell e indeed meta h peano imply meta r peano is meta t qed end math ]"} "[ intro hypothetical three one s two index "M3.1(S2)" pyk "hypothetical three one s two" tex " M3.1(S2')_h" end intro ]" \statement{"[ math in theory system prime s lemma hypothetical three one s two says all meta h indeed all meta t indeed all meta r indeed meta h peano imply meta t peano is meta r infer meta h peano imply meta t peano succ peano is meta r peano succ end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical three one s two reads arbitrary meta h end line arbitrary meta t end line arbitrary meta r end line line ell a premise meta h peano imply meta t peano is meta r end line line ell b because axiom prime s two indeed meta t peano is meta r peano imply meta t peano succ peano is meta r peano succ end line line ell c because hypothesize modus ponens ell b indeed meta h peano imply meta t peano is meta r peano imply meta t peano succ peano is meta r peano succ end line because ell c hypothetical modus ponens ell a indeed meta h peano imply meta t peano succ peano is meta r peano succ qed end math]"} "[ intro hypothetical three one s one index "M3.1(S1)" pyk "hypothetical three one s one" tex " M3.1(S1')_h" end intro ]" \statement{"[ math in theory system prime s lemma hypothetical three one s one says all meta h indeed all meta t indeed all meta r indeed all meta s indeed meta h peano imply meta t peano is meta r infer meta h peano imply meta t peano is meta s infer meta h peano imply meta r peano is meta s end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical three one s one reads arbitrary meta h end line arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a premise meta h peano imply meta t peano is meta r end line line ell b premise meta h peano imply meta t peano is meta s end line line ell z because axiom prime s one indeed meta t peano is meta r peano imply meta t peano is meta s peano imply meta r peano is meta s end line line ell c because hypothesize modus ponens ell z indeed meta h peano imply meta t peano is meta r peano imply meta t peano is meta s peano imply meta r peano is meta s end line line ell d because ell c hypothetical modus ponens ell a indeed meta h peano imply meta t peano is meta s peano imply meta r peano is meta s end line because ell d hypothetical modus ponens ell b indeed meta h peano imply meta r peano is meta s qed end math ]"} "[ intro hypothetical three two c index "M3.2(c)" pyk "hypothetical three two c" tex " M3.2(c)_h" end intro ]" \statement{"[ math in theory system prime s lemma hypothetical three two c says all meta h indeed all meta t indeed all meta r indeed all meta s indeed meta h peano imply meta t peano is meta r infer meta h peano imply meta r peano is meta s infer meta h peano imply meta t peano is meta s end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical three two c reads arbitrary meta h end line arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a premise meta h peano imply meta t peano is meta r end line line ell b premise meta h peano imply meta r peano is meta s end line line ell z because lemma prime l three two c indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end line line ell c because hypothesize modus ponens ell z indeed meta h peano imply meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end line line ell d because ell c hypothetical modus ponens ell a indeed meta h peano imply meta r peano is meta s peano imply meta t peano is meta s end line because ell d hypothetical modus ponens ell b indeed meta h peano imply meta t peano is meta s qed end math ]"} "[ intro hypothetical three one s five index "M3.1(S5)" pyk "hypothetical three one s five" tex " M3.1(S5')_h" end intro ]" \statement{"[ math in theory system prime s lemma hypothetical three one s five says all meta h indeed all meta t indeed meta h peano imply meta t peano plus peano zero peano is meta t end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical three one s five reads arbitrary meta h end line arbitrary meta t end line line ell a because axiom prime s five indeed meta t peano plus peano zero peano is meta t end line because hypothesize modus ponens ell a indeed meta h peano imply meta t peano plus peano zero peano is meta t qed end math]"} "[ intro hypothetical three one s six index "M3.1(S6)" pyk "hypothetical three one s six" tex " M3.1(S6')_h" end intro ]" \statement{"[ math in theory system prime s lemma hypothetical three one s six says all meta h indeed all meta t indeed all meta r indeed meta h peano imply meta t peano plus meta r peano succ peano is parenthesis meta t peano plus meta r end parenthesis peano succ end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical three one s six reads arbitrary meta h end line arbitrary meta t end line arbitrary meta r end line line ell a because axiom prime s six indeed meta t peano plus meta r peano succ peano is parenthesis meta t peano plus meta r end parenthesis peano succ end line because hypothesize modus ponens ell a indeed meta h peano imply meta t peano plus meta r peano succ peano is parenthesis meta t peano plus meta r end parenthesis peano succ qed end math]"} "[ intro hypothetical three two d index "M3.2(d) hyp" pyk " hypothetical three two d" tex "M3.2(d)_h" end intro ]" \statement{"[ math in theory system prime s lemma hypothetical three two d says all meta h indeed all meta t indeed all meta r indeed all meta s indeed meta h peano imply meta r peano is meta t infer meta h peano imply meta s peano is meta t infer meta h peano imply meta r peano is meta s end lemma end math ]"} \statement{"[ math system prime s proof of hypothetical three two d reads arbitrary meta h end line arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a premise meta h peano imply meta r peano is meta t end line line ell b premise meta h peano imply meta s peano is meta t end line line ell z because lemma prime l three two d one indeed meta s peano is meta t peano imply meta r peano is meta t peano imply meta r peano is meta s end line line ell c because hypothesize modus ponens ell z indeed meta h peano imply meta s peano is meta t peano imply meta r peano is meta t peano imply meta r peano is meta s end line line ell d because ell c hypothetical modus ponens ell b indeed meta h peano imply meta r peano is meta t peano imply meta r peano is meta s end line because ell d hypothetical modus ponens ell a indeed meta h peano imply meta r peano is meta s qed end math ]"} 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 "[ bracket peano x peano plus peano y peano is peano y peano plus peano x end bracket ]" 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 "[ math peano y end math ]". "[ intro lemma prime l three two h one index "M3.2(h) (I)" pyk " lemma prime l three two h one" tex "M3.2(h) (I)" end intro ]" \statement{"[ math in theory system prime s lemma lemma prime l three two h one says peano x peano plus peano zero peano is peano zero peano plus peano x end lemma end math]"} \statement{"[ math system prime s proof of lemma prime l three two h one reads line ell a because axiom prime s five indeed peano x peano plus peano zero peano is peano x end line line ell b because mendelson three two f indeed peano all peano t indeed peano t peano is peano zero peano plus peano t end line line ell c because axiom prime a four at peano x indeed parenthesis peano all peano t indeed peano t peano is peano zero peano plus peano t end parenthesis peano imply peano x peano is peano zero peano plus peano x end line line ell d because ell c macro modus ponens ell b indeed peano x peano is peano zero peano plus peano x end line line ell z because lemma prime l three two c indeed peano x peano plus peano zero peano is peano x peano imply peano x peano is peano zero peano plus peano x peano imply peano x peano plus peano zero peano is peano zero peano plus peano x end line line ell y because ell z macro modus ponens ell a indeed peano x peano is peano zero peano plus peano x peano imply peano x peano plus peano zero peano is peano zero peano plus peano x end line because ell y macro modus ponens ell d indeed peano x peano plus peano zero peano is peano zero peano plus peano x qed end math]"} 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): "[ intro mendelson three two f index "M3.2(f)" pyk "mendelson three two f" tex " M3.2(f)" end intro ]" \statement{"[ math in theory system prime s lemma mendelson three two f says peano all peano t indeed peano t peano is peano zero peano plus peano t end lemma end math ]"} \statement{"[ math system prime s proof of mendelson three two f reads locally define meta z as var x peano imply var x peano imply var x end line line ell a because axiom prime a one indeed meta z end line line ell b because hypothetical three one s five indeed meta z peano imply peano zero peano plus peano zero peano is peano zero end line line ell c because hypothetical three two b modus ponens ell b indeed meta z peano imply peano zero peano is peano zero peano plus peano zero end line line ell z because ell c macro modus ponens ell a indeed peano zero peano is peano zero peano plus peano zero end line locally define meta h as peano t peano is peano zero peano plus peano t end line line ell d because mendelson one seven indeed meta h peano imply peano t peano is peano zero peano plus peano t end line line ell e because hypothetical three one s two modus ponens ell d indeed meta h peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell f because hypothetical three one s six indeed meta h peano imply peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell g because hypothetical three two b modus ponens ell f indeed meta h peano imply parenthesis peano zero peano plus peano t end parenthesis peano succ peano is peano zero peano plus peano t peano succ end line line ell h because hypothetical three two c modus ponens ell e modus ponens ell g indeed meta h peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end line line ell i because rule prime gen modus ponens ell h indeed peano all peano t indeed parenthesis meta h peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end line line ell j because axiom prime s nine indeed peano zero peano is peano zero peano plus peano zero peano imply peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis peano imply peano all peano t indeed peano t peano is peano zero peano plus peano t end line line ell k because ell j macro modus ponens ell z indeed peano all peano t indeed parenthesis meta h peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis peano imply peano all peano t indeed peano t peano is peano zero peano plus peano t end line because ell k macro modus ponens ell i indeed peano all peano t indeed peano t peano is peano zero peano plus peano t qed end math ]"} 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 "[ bracket meta z end bracket ]" 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 "[ bracket peano y end bracket]" er "[ bracket peano zero end bracket]". \subsection{Lemma M3.2(g)} Inden M3.2(h) kan afsluttes er der brug for et sidste, men ganske omfattende induktionsbevis: "[ intro lemma prime l three two g index "M3.2(g)" pyk " lemma prime l three two g" tex "M3.2(g)" end intro ]" \statement{"[ math in theory system prime s lemma lemma prime l three two g says peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end lemma end math ]"} \statement{"[ math system prime s proof of lemma prime l three two g reads line ell a because axiom prime s five indeed peano y peano succ peano plus peano zero peano is peano y peano succ end line line ell b because axiom prime s five indeed peano y peano plus peano zero peano is peano y end line line ell c because axiom prime s two indeed peano y peano plus peano zero peano is peano y peano imply parenthesis peano y peano plus peano zero end parenthesis peano succ peano is peano y peano succ end line line ell d because ell c macro modus ponens ell b indeed parenthesis peano y peano plus peano zero end parenthesis peano succ peano is peano y peano succ end line line ell e because lemma prime l three two d two indeed peano y peano succ peano plus peano zero peano is peano y peano succ peano imply parenthesis peano y peano plus peano zero end parenthesis peano succ peano is peano y peano succ peano imply peano y peano succ peano plus peano zero peano is parenthesis peano y peano plus peano zero end parenthesis peano succ end line line ell f because ell e macro modus ponens ell a indeed parenthesis peano y peano plus peano zero end parenthesis peano succ peano is peano y peano succ peano imply peano y peano succ peano plus peano zero peano is parenthesis peano y peano plus peano zero end parenthesis peano succ end line line ell g because ell f macro modus ponens ell d indeed peano y peano succ peano plus peano zero peano is parenthesis peano y peano plus peano zero end parenthesis peano succ end line locally define meta h as peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell h because mendelson one seven indeed meta h peano imply peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell i because hypothetical three one s six indeed meta h peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano succ peano plus peano x end parenthesis peano succ end line line ell k because hypothetical three one s two modus ponens ell h indeed meta h peano imply parenthesis peano y peano succ peano plus peano x end parenthesis peano succ peano is parenthesis parenthesis peano y peano plus peano x end parenthesis peano succ end parenthesis peano succ end line line ell l because hypothetical three two c modus ponens ell i modus ponens ell k indeed meta h peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis parenthesis peano y peano plus peano x end parenthesis peano succ end parenthesis peano succ end line line ell o because hypothetical three one s six indeed meta h peano imply peano y peano plus peano x peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell p because hypothetical three one s two modus ponens ell o indeed meta h peano imply parenthesis peano y peano plus peano x peano succ end parenthesis peano succ peano is parenthesis parenthesis peano y peano plus peano x end parenthesis peano succ end parenthesis peano succ end line line ell q because hypothetical three two d modus ponens ell l modus ponens ell p indeed meta h peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ end line line ell r because axiom prime s nine indeed parenthesis peano y peano succ peano plus peano zero peano is parenthesis peano y peano plus peano zero end parenthesis peano succ end parenthesis peano imply peano all peano x indeed parenthesis peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ end parenthesis peano imply peano all peano x indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell s because ell r macro modus ponens ell g indeed peano all peano x indeed parenthesis peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ end parenthesis peano imply peano all peano x indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell t because rule prime gen modus ponens ell q indeed peano all peano x indeed parenthesis meta h peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ end parenthesis end line line ell u because ell s macro modus ponens ell t indeed peano all peano x indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell y because axiom prime a four at peano x indeed peano all peano x indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line because ell y macro modus ponens ell u indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ qed end math]"} 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: "[ intro lemma prime l three two h two index "M3.2(h) (II)" pyk " lemma prime l three two h two" tex "M3.2(h) (II)" end intro ]" \statement{"[ math in theory system prime s lemma lemma prime l three two h two says peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end lemma end math]"} \statement{"[ math system prime s proof of lemma prime l three two h two reads locally define meta h as peano x peano plus peano y peano is peano y peano plus peano x end line line ell j because mendelson one seven indeed meta h peano imply peano x peano plus peano y peano is peano y peano plus peano x end line line ell k because hypothetical three one s six indeed meta h peano imply peano x peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ end line line ell z because lemma prime l three two g indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell u because hypothesize modus ponens ell z indeed meta h peano imply peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell m because hypothetical three one s two modus ponens ell j indeed meta h peano imply parenthesis peano x peano plus peano y end parenthesis peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell o because hypothetical three two c modus ponens ell k modus ponens ell m indeed meta h peano imply peano x peano plus peano y peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line because hypothetical three two d modus ponens ell o modus ponens ell u indeed meta h peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x qed end math]"} \subsection{Lemma M3.2(h)} "[ intro lemma prime l three two h index "M3.2(h)" pyk " lemma prime l three two h" tex "M3.2(h)" end intro ]" \statement{"[ math in theory system prime s lemma lemma prime l three two h says peano all peano x indeed peano all peano y indeed peano x peano plus peano y peano is peano y peano plus peano x end lemma end math]"} "[ intro lemma prime l three two f index "M3.2(f)" pyk " lemma prime l three two f" tex "M3.2(f)" end intro ]" Nu kan brikkerne samles ved en sidste gang at instantiere S9: \statement{"[ math system prime s proof of lemma prime l three two h reads line ell a because axiom prime s nine indeed parenthesis peano x peano plus peano zero peano is peano zero peano plus peano x end parenthesis peano imply peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end parenthesis peano imply peano all peano y indeed peano x peano plus peano y peano is peano y peano plus peano x end line line ell z because lemma prime l three two h one indeed peano x peano plus peano zero peano is peano zero peano plus peano x end line line ell y because lemma prime l three two h two indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end parenthesis end line line ell x because rule prime gen modus ponens ell y indeed peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end parenthesis end line line ell b because ell a macro modus ponens ell z indeed peano all peano y indeed parenthesis peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end parenthesis peano imply peano all peano y indeed peano x peano plus peano y peano is peano y peano plus peano x end line line ell c because ell b macro modus ponens ell x indeed peano all peano y indeed peano x peano plus peano y peano is peano y peano plus peano x end line because rule prime gen modus ponens ell c indeed peano all peano x indeed peano all peano y indeed peano x peano plus peano y peano is peano y peano plus peano x qed end math]"} 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{"[ math pyk define proofreport as "proofreport" end define end math ]"} \subsection{Modus ponens} "[ intro var x hypothetical modus ponens var y pyk "* hypothetical modus ponens *" tex "#1. \unrhd_h #2." end intro ]" \display{"[ math 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 math ]"} "[ intro var x macro modus ponens var y pyk "* macro modus ponens *" tex "#1. \unrhd #2." end intro ]" \display{"[ math macro define var x macro modus ponens var y as rule prime mp modus ponens var x modus ponens var y end define end math ]"} \subsection{Variable} "[ intro var x peano var pyk "* peano var" tex " \dot{#1. }" end intro ]" "[ intro var x is peano var index "P" pyk "* is peano var" tex "#1. {} ^ {\cal P}" end intro ]" \display{"[ math value define var x is peano var as var x term root equal quote var x peano var end quote end define end math ]"} "[ intro peano a index "a" pyk "peano a" tex " \dot{\mathit{a}}" end intro ]" \display{"[ math macro define peano a as var a peano var end define end math ]"}% \subsection{ free og nonefree } "[ intro peano nonfree var x in var y end nonfree index "nonfree" pyk "peano nonfree * in * end nonfree" tex " \dot{nonfree}(#1. ,#2. )" end intro ]" "[ intro peano nonfree star var x in var y end nonfree index "nonfree*" pyk "peano nonfree star * in * end nonfree" tex " \dot{nonfree}^*(#1. ,#2. )" end intro ]" \display{"[ math value define peano nonfree var x in var y end nonfree as newline open if var y is peano var then not var x term equal var y else newline open 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 open if var x term equal var y first then true else peano nonfree var x in var y second end nonfree end define end math ]"} \display{"[ math value define peano nonfree star var x in var y end nonfree as var x tagged guard tagged if var y then true else peano nonfree var x in var y head end nonfree macro and peano nonfree star var x in var y tail end nonfree end if end define end math ]"}% % "[ intro peano free var a set var x to var b end free index "free" pyk "peano free * set * to * end free" tex " \dot{free}\langle #1. | #2. := #3. \rangle" end intro ]" "[ intro peano free star var a set var x to var b end free index "free*" pyk "peano free star * set * to * end free" tex " \dot{free}{}^*\langle #1. | #2. := #3. \rangle" end intro ]" "[ bracket var a end bracket ]" \display{"[ math value define peano free var a set var x to var b end free as var x tagged guard var b tagged guard newline open if var a is peano var then true else newline open 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 open if var a first term equal var x then true else newline open if peano nonfree var x in var a second end nonfree then true else newline open 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 define end math ]"} \display{"[ math value define 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 peano free var a head set var x to var b end free macro and peano free star var a tail set var x to var b end free end if end define end math ]"}% % "[ intro peano sub var a is var b where var x is var c end sub pyk "peano sub * is * where * is * end sub" tex "#1. {\equiv}\langle #2. |#3. :=#4. \rangle" end intro ]" "[ intro peano sub star var a is var b where var x is var c end sub pyk "peano sub star * is * where * is * end sub" tex "#1. {\equiv}\langle^* #2. |#3. :=#4. \rangle" end intro ]" \display{"[ math value define 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 open if var b term root equal quote peano all var u indeed var v end quote macro and var b first term equal var x then var a term equal var b else newline open if var b is peano var and var b term equal var x then var a term equal var c else newline var a term root equal var b macro and peano sub star var a tail is var b tail where var x is var c end sub end define end math ]"} \display{"[ math value define 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 peano sub var a head is var b head where var x is var c end sub macro and peano sub star var a tail is var b tail where var x is var c end sub end if end define end math ]"}% % \subsection{Variables of Peano arithmetic}\label{section:VariablesOfPeanoArithmetic} "[ intro peano b index "b" pyk "peano b" tex " \dot{\mathit{b}}" end intro ]", "[ intro peano c index "c" pyk "peano c" tex " \dot{\mathit{c}}" end intro ]", "[ intro peano d index "d" pyk "peano d" tex " \dot{\mathit{d}}" end intro ]", "[ intro peano e index "e" pyk "peano e" tex " \dot{\mathit{e}}" end intro ]", "[ intro peano f index "f" pyk "peano f" tex " \dot{\mathit{f}}" end intro ]", "[ intro peano g index "g" pyk "peano g" tex " \dot{\mathit{g}}" end intro ]", "[ intro peano h index "h" pyk "peano h" tex " \dot{\mathit{h}}" end intro ]", "[ intro peano i index "i" pyk "peano i" tex " \dot{\mathit{i}}" end intro ]", "[ intro peano j index "j" pyk "peano j" tex " \dot{\mathit{j}}" end intro ]", "[ intro peano k index "k" pyk "peano k" tex " \dot{\mathit{k}}" end intro ]", "[ intro peano l index "l" pyk "peano l" tex " \dot{\mathit{l}}" end intro ]", "[ intro peano m index "m" pyk "peano m" tex " \dot{\mathit{m}}" end intro ]", "[ intro peano n index "n" pyk "peano n" tex " \dot{\mathit{n}}" end intro ]", "[ intro peano o index "o" pyk "peano o" tex " \dot{\mathit{o}}" end intro ]", "[ intro peano p index "p" pyk "peano p" tex " \dot{\mathit{p}}" end intro ]", "[ intro peano q index "q" pyk "peano q" tex " \dot{\mathit{q}}" end intro ]", "[ intro peano r index "r" pyk "peano r" tex " \dot{\mathit{r}}" end intro ]", "[ intro peano s index "s" pyk "peano s" tex " \dot{\mathit{s}}" end intro ]", "[ intro peano t index "t" pyk "peano t" tex " \dot{\mathit{t}}" end intro ]", "[ intro peano u index "u" pyk "peano u" tex " \dot{\mathit{u}}" end intro ]", "[ intro peano v index "v" pyk "peano v" tex " \dot{\mathit{v}}" end intro ]", "[ intro peano w index "w" pyk "peano w" tex " \dot{\mathit{w}}" end intro ]", "[ intro peano x index "x" pyk "peano x" tex " \dot{\mathit{x}}" end intro ]", "[ intro peano y index "y" pyk "peano y" tex " \dot{\mathit{y}}" end intro ]" "[ intro peano z index "z" pyk "peano z" tex " \dot{\mathit{z}}" end intro ]" "[ math macro define peano b as var b peano var end define end math ]", "[ math macro define peano c as var c peano var end define end math ]", "[ math macro define peano d as var d peano var end define end math ]", "[ math macro define peano e as var e peano var end define end math ]", "[ math macro define peano f as var f peano var end define end math ]", "[ math macro define peano g as var g peano var end define end math ]", "[ math macro define peano h as var h peano var end define end math ]", "[ math macro define peano i as var i peano var end define end math ]", "[ math macro define peano j as var j peano var end define end math ]", "[ math macro define peano k as var k peano var end define end math ]", "[ math macro define peano l as var l peano var end define end math ]", "[ math macro define peano m as var m peano var end define end math ]", "[ math macro define peano n as var n peano var end define end math ]", "[ math macro define peano o as var o peano var end define end math ]", "[ math macro define peano p as var p peano var end define end math ]", "[ math macro define peano q as var q peano var end define end math ]", "[ math macro define peano r as var r peano var end define end math ]", "[ math macro define peano s as var s peano var end define end math ]", "[ math macro define peano t as var t peano var end define end math ]", "[ math macro define peano u as var u peano var end define end math ]", "[ math macro define peano v as var v peano var end define end math ]", "[ math macro define peano w as var w peano var end define end math ]", "[ math macro define peano x as var x peano var end define end math ]", "[ math macro define peano y as var y peano var end define end math ]", "[ math macro define peano z as var z peano var end define end math ]". \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} "[ flush left math priority table Priority end table end math end left ]" \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"