Kommutativitet for plusoperatoren

Anders Bøggild-Povlsen (boggild@diku.dk) & Nicolai Esbensen(nies@diku.dk)

GRD-2005-06-29.UTC:16:44:29.722893

Contents

1 Forord 2

2 Peano-systemet 2

3 Introduktion 3

4 Hjælpesætninger 4 4.1 Introduktion af metavariabel . . . . . . . . . . . . . . . . . . . . 4 4.2 Kommutativitet ved medfører . . . . . . . . . . . . . . . . . . . . 4 4.3 Transitivitet for medfører . . . . . . . . . . . . . . . . . . . . . . 5

5 Bevis af lemmaer 6 5.1 Bevis for LEMMA3.2(a) . . . . . . . . . . . . . . . . . . . . . . . 6 5.2 Bevis for LEMMA3.2(b) . . . . . . . . . . . . . . . . . . . . . . . 6 5.3 Bevis for LEMMA3.2(c) . . . . . . . . . . . . . . . . . . . . . . . 6 5.4 Bevis for LEMMA3.2(d) . . . . . . . . . . . . . . . . . . . . . . . 7 5.5 Kort omkring induktionsbeviserne . . . . . . . . . . . . . . . . . 8 5.6 Bevis for LEMMA3.2(f) . . . . . . . . . . . . . . . . . . . . . . . 8

5.6.1 Bevis for basistilfælde i LEMMA3.2(f) . . . . . . . . . . . 8 5.6.2 Bevis for induktionsskridt i LEMMA3.2(f) . . . . . . . . . 8 5.6.3 Samling af delbeviser . . . . . . . . . . . . . . . . . . . . . 9

5.7 Bevis for LEMMA3.2(g) . . . . . . . . . . . . . . . . . . . . . . . 9 5.7.1 Bevis for basistilfælde for LEMMA3.2(g) . . . . . . . . . 9 5.7.2 Bevis for induktionsskridt for LEMMA3.2(g) . . . . . . . 10 5.7.3 Samling af delbeviser . . . . . . . . . . . . . . . . . . . . . 11

5.8 Bevis for LEMMA3.2(h) . . . . . . . . . . . . . . . . . . . . . . . 11 5.8.1 Bevis for basistilfælde for LEMMA3.2(h) . . . . . . . . . 11 5.8.2 Bevis for induktionsskridt for LEMMA3.2(h) . . . . . . . 12 5.8.3 Samling af delbeviser . . . . . . . . . . . . . . . . . . . . . 12

6 Litteratur 13 7 TEX definitioner 14 8 Sidens navn 14

1 Forord

Denne rapport er bevistjekket og verificet korrekt, vha. systemet logiweb. Systemet muliggør verificering af dokumenter skrevet i sproget pyk, der er en sammensmeltning mellem latex-kode og de konstruktioner der er defineret i de inkluderede sider, og de konstruktioner der genkendes internt i pyk-oversætteren. Udover at verificere beviser publicerer logiweb siderne på Internettet i div. formater. Dette dokument er et således et produkt af et kompileret pyk-dokument. Index-siden for dette dokument er at finde på adressen:

http://www.diku.dk/ grue/logiweb/20050502/home/nies/rapport/fixed/ De efterfølgende beviser bygger på axiomer og inferensregler givet inden

for peanosystemet. Vi giver en kort historisk gennemgang af systemet i næste afsnit (2). Målet med projektet har været at bevise kommutativitet for plusoperatoren (5.8), vi kan i skrivende stund konkludere at det mål er nået.

2 Peano-systemet

I 1889 publicerede Peano en formalisering af de naturlige tal. Denne formalisering bestod af 5 axiomer kendt som Peano’s Postulater.

1 0 er et naturligt tal^{1}.

2 Hvis x er et naturligt tal, så findes der et andet naturligt tal x′ (efterfølgeren til x).

3 0 ≠ x′ for ethvert naturligt tal x.

4 Hvis x′ = y′ gælder det at x = y

5 Induktion: Q er et udtryk der gælder eller ikke gælder. Hvis tallet 0 har Q’s egenskab og en given variabel x og dens efterfœlger x′ har egenskaben, har alle naturlige tal egenskaben. Altså udtrykket gælder for alle naturlige tal.

Formålet med vores rapport er at bevise kommutativitet for plusoperatoren for de naturlige tal. Vi vil bevise dette ud fra en førsteordens-teori (S′)[1] der er en videreudvikling Peanos postulater. Denne teori har 9 axiomer (S1′ − S9′) og har ikke ækvivalente axiomer til alle Peano’s Postulater. F.eks. er der ikke et axiom der siger at 0 er et heltal, da dette fremgår implicit axiomerne. De ekstra axiomer i S′ omfatter bl.a. en variation af transitivitet (S1′) og det omvendte af Peano’s 4 postulat (S2′).

Derudover bygger S′ også på 5 axiomer (A1′ − A5′) og 2 inferensregler (MP, Gen)^{2} som gælder for førsteordens prædikat-kalkyler.

De enkelte regler og axiomer i den nye teori gennemgås og opskrives i hhv. Mendelson [3] og Peano-siden.

1Oprindeligt 1 er et naturligt tal, da 0 ikke blev betragtet som et naturligt tal

2hhv. Modus ponens og Generalisering

3 Introduktion

I denne rapport vil vi som tidligere nævnt forsøge at bevise LEMMA3.2(h), også kendt som den kommutative lov. Til at hjælpe os med dette har vi axiomerne og inferensreglerne i systemet S′, stillet til rådighed. I litteraturen [3] foreslåes det at vi beviser visse teoremer vha. axiomerne og inferensreglerne givet i S′, og endelig bruge dem til at bevise LEMMA3.2(h). I dette afsnit vil vi opskrive disse teoremer og kort beskrive deres betydning og brug.

Det kan tænkes at vi undervejs kommer til at have brug for hjælpesætninger, disse vil blive introduceret og bevist i afsnit (4).

Det første lemma beskriver egenskaben omkring et givent udtryk T nødvendigvis må evalueres til at være lig den selv^{3}. Dette beskriver således den egenskab vi normalt forventer af lighedsoperatoren^{4} i heltalsaritmetik. Mere avancerede egenskaber ved lighedsopertoren bliver beskrevet i efterfølgende lemmaer.

[S′ lemma LEMMA3.2(a): ∀T : T =^{p} T ] ^{5}

Andet teorem viser en anden egenskab for vores lighedsoperator; nemlig at det er kommutativt. Er alle givne udtryk T lig R, må det nødvendigvis også gælde at R lig T .

[S′ lemma LEMMA3.2(b): ∀T : ∀R: T =^{p} R ˙⇒ R =^{p} T ] ^{6}

Tredje teorem viser at transitivitet for lighedsoperatoren.

[S′ lemma LEMMA3.2(c): ∀T : ∀R: ∀S: T =^{p} R ˙⇒ R =^{p} S ˙⇒ T =^{p} S] ^{7}

Fjerde lemma beskriver samme egenskab som lemma tre, men udnytter samtidigt at lighedstegnet er kommutativt. Dette lemma synes ikke umiddelbart at vise særligt skælsættende egenskaber, men kan vise sig særdeles nyttig i forbindelse med brug af vores inferensregler.

[S′ lemma LEMMA3.2(d): ∀T : ∀R: ∀S: R =^{p} T ˙⇒ S =^{p} T ˙⇒ R =^{p} S] ^{8}

Femte lemma beskriver egenskaben ved heltallet 0, nemlig at addition med 0 ikke ændrer et udtryks værdi.

[S′ lemma LEMMA3.2(f): ṫ =^{p} ˙0 ˙+ ṫ] ^{9}

Næstsidste lemma viser en egenskab ved succesor-operatoren^{10}. Egenskaben der vises er at successor-operatoren er distributiv ved addition. Intuitivt giver dette god mening da plus-operatoren er kommutativ^{11}, og rækkefølgen for evaluering derfor er ligegyldig.

3Et krav for at et givent system er et system med lighed

4Skrives inden for det formulerede peano-system =^{p}

5[LEMMA3.2(a) =^{pyk} “mendelson lemma three two a”]

6[LEMMA3.2(b) =^{pyk} “mendelson lemma three two b”]

7[LEMMA3.2(c) =^{pyk} “mendelson lemma three two c”]

8[LEMMA3.2(d) =^{pyk} “mendelson lemma three two d”]

9[LEMMA3.2(f) =^{pyk} “mendelson lemma three two f”]

10Har den egenskab at der lægges et til udtrykket operatoren anvendes på eksempelvis:

41′ = 42

[S′ lemma LEMMA3.2(g): ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′] ^{12}

Vores endelig lemma, kronen på værket, viser at plus-operatoren er kommutativ, altså at resultatet er uafhængigt af hvilken side operanderne står på.

[S′ lemma LEMMA3.2(h): ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ] ^{13}

4 Hjælpesætninger

I dette afsnit defineres og bevises de benyttede hjælpesætninger, der ligger ud over de allerede definerede sætninger i afsnit 3.

4.1 Introduktion af metavariabel

I løbet af projektet opstod der et behov for at introducere en ny metavariabel til at medføre et andet givent udtryk. Dette vil gælde uafhængigt af den introducerede variabels sandhedsværdi, da det er en forudsætning at den oprindelige sætning gælder footnoteSe evt. sandhedstabellen for medfører i [3] afsnit 1.1. Herunder følger definitionen og beviset for lemmaet.

[S′ lemma IMV: ∀A: ∀B: A ⊢ B ˙⇒ A] ^{14}

S′ proof of IMV:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Premise ≫  A  ;
L04: A1′ ≫  A ˙⇒ B ˙⇒ A  ;
L05: MP′ ⊳ L04 ⊳ L03 ≫  B ˙⇒ A  □

4.2 Kommutativitet ved medfører

Det viser sig at medføreroperatoren er associativ i første led for tre eller flere metavariable, såfremt hele det oprindelige udtryk evaluerer til sand. Dette er netop hvad nedenstående udtryk siger. Dette faktum vil også kunne vises ved tautologi at de to udtryk er logisk ækvivalente, denne mulighed har dog ikke som bevisform, og vil derfor bevise påstanden vha. de givne axiomer og inferensregler.

[S′ lemma CImp: ∀A: ∀B: ∀C: A ˙⇒ C ˙⇒ B ⊢ C ˙⇒ A ˙⇒ B] ^{15} S′ proof of CImp:

11Bemærk at dette ikke er bevist endnu

12[LEMMA3.2(g) =^{pyk} “mendelson lemma three two g”]

13[LEMMA3.2(h) =^{pyk} “mendelson lemma three two h”]

14[IMV =^{pyk} “int mvar”]

15[CImp =^{pyk} “commutative imply”]

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A ˙⇒ C ˙⇒ B  ;
L05: A2′ ≫  {(A ˙⇒ C ˙⇒ B) ˙⇒ (A ˙⇒ C) ˙⇒ \atop (A ˙⇒ B)  ;}
L06: MP′ ⊳ L05 ⊳ L04 ≫  (A ˙⇒ C) ˙⇒ (A ˙⇒ B)  ;
L07: IMV ⊳ L06 ≫  C ˙⇒ (A ˙⇒ C) ˙⇒ (A ˙⇒ B)  ;
L08: A2′ ≫  {(C ˙⇒ (A ˙⇒ C) ˙⇒ (A ˙⇒ B)) ˙⇒ \atop (C ˙⇒ A ˙⇒ C) ˙⇒ (C ˙⇒ A ˙⇒ B) ;}
L09: MP′ ⊳ L08 ⊳ L07 ≫  (C ˙⇒ A ˙⇒ C) ˙⇒ (C ˙⇒ A ˙⇒ B) ;
L10: A1′ ≫  C ˙⇒ A ˙⇒ C  ;
L11: MP′ ⊳ L09 ⊳ L10 ≫  C ˙⇒ A ˙⇒ B  □

4.3 Transitivitet for medfører

Det er ofte en fordel at kunne vise at hvis et givent udtryk medfører et andet, hvor dette endvidere medfører et tredje, må der som konsekvens heraf gælde at det første medfører det tredje. Dette er umiddelbart nemmere at opskrive end forklare, herunder A, B, C (hhv. første, anden og tredje sætning) :

[S′ lemma TImp: ∀A: ∀B: ∀C: A ˙⇒ B ⊢ B ˙⇒ C ⊢ A ˙⇒ C] ^{16} Nedenstående bevis er givet i løsningssiderne i Mendelson [3]. S′ proof of TImp:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A ˙⇒ B  ;
L05: Premise ≫  B ˙⇒ C  ;
L06: A2′ ≫  {(A ˙⇒ B ˙⇒ C) ˙⇒ (A ˙⇒ B) ˙⇒ \atop (A ˙⇒ C)  ;}
L07: A1′ ≫  (B ˙⇒ C) ˙⇒ A ˙⇒ (B ˙⇒ C)  ;
L08: MP′ ⊳ L07 ⊳ L05 ≫  A ˙⇒ B ˙⇒ C  ;
L09: MP′ ⊳ L06 ⊳ L08 ≫  (A ˙⇒ B) ˙⇒ (A ˙⇒ C)  ;
L10: MP′ ⊳ L09 ⊳ L04 ≫  A ˙⇒ C  □

16[TImp =^{pyk} “transitive imply”]

5 Bevis af lemmaer

I dette afsnit beviser vi de beskrevne lemmaer i afsnit 3. Vi vil for hvert bevis genopskrive det lemma der ønskes bevist så arbejdet mod konklusionen er klarere i sammenhængen.

Beviserne bygger i større eller mindre grad på de gennemgåede beviser i Mendelson. Mange steder benyttes tautologier samt deduktions teoremet, disse ting kan ikke direkte benyttes indenfor logiwebsystemet, hvorfor vi beviser os ud af de enkelte linjer vha. de givne axiomer og inferensregler givet i peano-systemet. Det har også været nødvedigt at ekspandere forskellige linjer og intruducere hjælpesætninger (4) enkelte steder.

5.1 Bevis for LEMMA3.2(a)

[S′ lemma LEMMA3.2(a): ∀T : T =^{p} T ]

S′ proof of LEMMA3.2(a):

L01: Arbitrary ≫  T  ;
L02: S5′ ≫  T ˙+ ˙0 =^{p} T  ;
L03: S1′ ≫  {T ˙+ ˙0 =^{p} T ˙⇒ T ˙+ ˙0 =^{p} T ˙⇒ \atop T =^{p} T  ;}
L04: MP′ ⊳ L03 ⊳ L02 ≫  T ˙+ ˙0 =^{p} T ˙⇒ T =^{p} T  ;
L05: MP′ ⊳ L04 ⊳ L02 ≫  T =^{p} T  □

5.2 Bevis for LEMMA3.2(b)

[S′ lemma LEMMA3.2(b): ∀T : ∀R: T =^{p} R ˙⇒ R =^{p} T ]

S′ proof of LEMMA3.2(b):

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: S1′ ≫  T =^{p} R ˙⇒ T =^{p} T ˙⇒ R =^{p} T  ;
L04: CImp ⊳ L03 ≫  T =^{p} T ˙⇒ T =^{p} R ˙⇒ R =^{p} T  ;
L05: LEMMA3.2(a) ≫  T =^{p} T  ;
L06: MP′ ⊳ L04 ⊳ L05 ≫  T =^{p} R ˙⇒ R =^{p} T  □

5.3 Bevis for LEMMA3.2(c)

[S′ lemma LEMMA3.2(c): ∀T : ∀R: ∀S: T =^{p} R ˙⇒ R =^{p} S ˙⇒ T =^{p} S]

S′ proof of LEMMA3.2(c):

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: Arbitrary ≫  S  ;
L04: S1′ ≫  R =^{p} T ˙⇒ R =^{p} S ˙⇒ T =^{p} S  ;
L05: LEMMA3.2(b) ≫  T =^{p} R ˙⇒ R =^{p} T  ;
L06: TImp ⊳ L05 ⊳ L04 ≫  T =^{p} R ˙⇒ R =^{p} S ˙⇒ T =^{p} S  □

5.4 Bevis for LEMMA3.2(d)

[S′ lemma LEMMA3.2(d): ∀T : ∀R: ∀S: R =^{p} T ˙⇒ S =^{p} T ˙⇒ R =^{p} S]

S′ proof of LEMMA3.2(d):

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: Arbitrary ≫  S  ;
L04: LEMMA3.2(c) ≫  R =^{p} T ˙⇒ T =^{p} S ˙⇒ R =^{p} S  ;
L05: CImp ⊳ L04 ≫  T =^{p} S ˙⇒ R =^{p} T ˙⇒ R =^{p} S  ;
L06: LEMMA3.2(b) ≫  S =^{p} T ˙⇒ T =^{p} S  ;
L07: TImp ⊳ L06 ⊳ L05 ≫  S =^{p} T ˙⇒ R =^{p} T ˙⇒ R =^{p} S  ;
L08: CImp ⊳ L07 ≫  R =^{p} T ˙⇒ S =^{p} T ˙⇒ R =^{p} S  □

5.5 Kort omkring induktionsbeviserne

I de efterfølgende beviser benyttes induktion, for at bevise de enkelte lemmaer. Vi gør dette ved seperat at bevise nultilfældet^{17} og induktionskridtet, for til sidst at inducere over de to udtryk og herved nå vores konklusion. Dette er således samme strategi der benyttes i Mendelson [3]. Bemærk at vi i benytter peanovariable, der udelukkende beskriver heltal, i modsætning til de tidligere beviser, hvor vi gennemførte beviserne for arbitrære udtryk. Dette er en nødvendighed, for at kunne benytte peano-induktionsreglen (S9′).

5.6 Bevis for LEMMA3.2(f)

5.6.1 Bevis for basistilfælde i LEMMA3.2(f)

[S′ lemma LEMMA3.2(f)base: ˙0 =^{p} ˙0 ˙+ ˙0] ^{18}

S′ proof of LEMMA3.2(f)base:

L01: S5′ ≫  ˙0 ˙+ ˙0 =^{p} ˙0  ;
L02: LEMMA3.2(b) ≫  ˙0 ˙+ ˙0 =^{p} ˙0 ˙⇒ ˙0 =^{p} ˙0 ˙+ ˙0  ;
L03: MP′ ⊳ L02 ⊳ L01 ≫  ˙0 =^{p} ˙0 ˙+ ˙0  □

5.6.2 Bevis for induktionsskridt i LEMMA3.2(f)

[S′ lemma LEMMA3.2(f)induction: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′] ^{19}

S′ proof of LEMMA3.2(f)induction:

L01: S6′ ≫  ˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′  ;
L02: S2′ ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} (˙0 ˙+ ṫ)′  ;

L03: LEMMA3.2(d) ≫ ṫ′ =^{p} (˙0 ˙+ ṫ)′ ˙⇒ ˙0 ˙+ ṫ′ =^{p}

(˙0 ˙+ ṫ)′ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ;

L04: TImp ⊳ L02 ⊳ L03 ≫

ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′ ˙⇒
ṫ′ =^{p} ˙0 ˙+ ṫ′  ;

L05: CImp ⊳ L04 ≫

˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒
ṫ′ =^{p} ˙0 ˙+ ṫ′  ;
L06: MP′ ⊳ L05 ⊳ L01 ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′  □

17De enkelte delbeviser introduceres i de enkelte underafsnit

18[LEMMA3.2(f)base =^{pyk} “mendelson lemma three two f base”]

19[LEMMA3.2(f)induction =^{pyk} “mendelson lemma three two f induction”]

5.6.3 Samling af delbeviser

[S′ lemma LEMMA3.2(f): ṫ =^{p} ˙0 ˙+ ṫ]

S′ proof of LEMMA3.2(f):

L01: S9′ ≫ ˙0 =^{p} ˙0 ˙+ ˙0 ˙⇒ ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒

ṫ′ =^{p} ˙0 ˙+ ṫ′) ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ;

L02: LEMMA3.2(f)base ≫ ˙0 =^{p} ˙0 ˙+ ˙0 ;

L03: MP′ ⊳ L01 ⊳ L02 ≫ ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′) ˙⇒

˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ;

L04: LEMMA3.2(f)induction ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′  ;
L05: Gen′ ⊳ L04 ≫  ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′)  ;
L06: MP′ ⊳ L03 ⊳ L05 ≫  ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ  ;
L07: A4′ @ ṫ ≫  ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ  ;
L08: MP′ ⊳ L07 ⊳ L06 ≫  ṫ =^{p} ˙0 ˙+ ṫ  □

5.7 Bevis for LEMMA3.2(g)

Bemærk at vi i dette afsnit har været nødt til at ombytte variabelnavnene, i forhold til i Mendelson [3]. Dette skyldes at vi fik en fejl, når vi instatierede lemmaet i LEMMA3.2(h), denne ombytning har dog ingen indflydelse på den egenskab lemmaet beskriver.

5.7.1 Bevis for basistilfælde for LEMMA3.2(g)

[S′ lemma LEMMA3.2(g)base: ṙ′ ˙+ ˙0 =^{p} (ṙ ˙+ ˙0)′] ^{20}

S′ proof of LEMMA3.2(g)base:

L01: S5′ ≫  ṙ′ ˙+ ˙0 =^{p} ṙ′  ;
L02: S5′ ≫  ṙ ˙+ ˙0 =^{p} ṙ  ;
L03: S2′ ≫  ṙ ˙+ ˙0 =^{p} ṙ ˙⇒ (ṙ ˙+ ˙0)′ =^{p} ṙ′  ;
L04: MP′ ⊳ L03 ⊳ L02 ≫  (ṙ ˙+ ˙0)′ =^{p} ṙ′  ;

L05: LEMMA3.2(d) ≫ ṙ′ ˙+ ˙0 =^{p} ṙ′ ˙⇒ (ṙ ˙+ ˙0)′ =^{p} ṙ′ ˙⇒

ṙ′ ˙+ ˙0 =^{p} (ṙ ˙+ ˙0)′ ;

L06: MP′ ⊳ L05 ⊳ L01 ≫  {(ṙ ˙+ ˙0)′ =^{p} ṙ′ ˙⇒ ṙ′ ˙+ ˙0 =^{p} \atop (ṙ ˙+ ˙0)′  ;}
L07: MP′ ⊳ L06 ⊳ L04 ≫  ṙ′ ˙+ ˙0 =^{p} (ṙ ˙+ ˙0)′  □

20[LEMMA3.2(g)base =^{pyk} “mendelson lemma three two g base”]

5.7.2 Bevis for induktionsskridt for LEMMA3.2(g) [S′ lemma LEMMA3.2(g)induction: ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ ṙ′ ˙+ ṫ′ =^{p} (ṙ ˙+ ṫ′)′] ^{21}

S′ proof of LEMMA3.2(g)induction:

L01: S6′ ≫ ṙ′ ˙+ ṫ′ =^{p} (ṙ′ ˙+ ṫ)′ ;

L02: S2′ ≫ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ (ṙ′ ˙+ ṫ)′ =^{p} ((ṙ ˙+ ṫ)′)′ ;

L03: LEMMA3.2(c) ≫ ṙ′ ˙+ ṫ′ =^{p} (ṙ′ ˙+ ṫ)′ ˙⇒ (ṙ′ ˙+ ṫ)′ =^{p}

((ṙ ˙+ ṫ)′)′ ˙⇒ ṙ′ ˙+ ṫ′ =^{p}

((ṙ ˙+ ṫ)′)′ ;

L04: MP′ ⊳ L03 ⊳ L01 ≫

(ṙ′ ˙+ ṫ)′  =^{p} ((ṙ ˙+ ṫ)′)′  ˙⇒

ṙ′ ˙+ ṫ′ =^{p} ((ṙ ˙+ ṫ)′)′ ;

L05: TImp ⊳ L02 ⊳ L04 ≫ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ ṙ′ ˙+ ṫ′ =^{p} ((ṙ ˙+ ṫ)′)′ ;

L06: LEMMA3.2(d) ≫

ṙ′ ˙+ ṫ′  =^{p} ((ṙ ˙+ ṫ)′)′  ˙⇒
(ṙ ˙+ ṫ′)′  =^{p} ((ṙ ˙+ ṫ)′)′  ˙⇒

ṙ′ ˙+ ṫ′ =^{p} (ṙ ˙+ ṫ′)′ ;

L07: TImp ⊳ L05 ⊳ L06 ≫ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ (ṙ ˙+ ṫ′)′ =^{p}

((ṙ ˙+ ṫ)′)′ ˙⇒ ṙ′ ˙+ ṫ′ =^{p} (ṙ ˙+ ṫ′)′ ;

L08: CImp ⊳ L07 ≫

(ṙ ˙+ ṫ′)′  =^{p} ((ṙ ˙+ ṫ)′)′  ˙⇒

ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ ṙ′ ˙+ ṫ′ =^{p} (ṙ ˙+ ṫ′)′ ;

L09: S6′ ≫ ṙ ˙+ ṫ′ =^{p} (ṙ ˙+ ṫ)′ ;

L10: S2′ ≫ ṙ ˙+ ṫ′ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ (ṙ ˙+ ṫ′)′ =^{p} ((ṙ ˙+ ṫ)′)′ ;

L11: MP′ ⊳ L10 ⊳ L09 ≫ (ṙ ˙+ ṫ′)′ =^{p} ((ṙ ˙+ ṫ)′)′ ;

L12: MP′ ⊳ L08 ⊳ L11 ≫ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ ṙ′ ˙+ ṫ′ =^{p} (ṙ ˙+ ṫ′)′ □ [S′ lemma LEMMA3.2(g): ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′]

21[LEMMA3.2(g)induction =^{pyk} “mendelson lemma three two g induction”]

S′ proof of LEMMA3.2(g): L01: S9′ ≫ ṙ′ ˙+ ˙0 =^{p} (ṙ ˙+ ˙0)′ ˙⇒ ˙∀ṫ: (ṙ′ ˙+ ṫ =^{p}

(ṙ ˙+ ṫ)′ ˙⇒ ṙ′ ˙+ ṫ′ =^{p} (ṙ ˙+ ṫ′)′) ˙⇒

˙∀ṫ: ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ;

L02: LEMMA3.2(g)base ≫ ṙ′ ˙+ ˙0 =^{p} (ṙ ˙+ ˙0)′ ;

L03: MP′ ⊳ L01 ⊳ L02 ≫ ˙∀ṫ: (ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒

ṙ′ ˙+ ṫ′ =^{p} (ṙ ˙+ ṫ′)′) ˙⇒

˙∀ṫ: ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ;

L04: LEMMA3.2(g)induction ≫

ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ ṙ′ ˙+ ṫ′ =^{p}
(ṙ ˙+ ṫ′)′ ;

L05: Gen′ ⊳ L04 ≫ ˙∀ṫ: (ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒

ṙ′ ˙+ ṫ′ =^{p} (ṙ ˙+ ṫ′)′) ;

L06: MP′ ⊳ L03 ⊳ L05 ≫ ˙∀ṫ: ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ;

L07: A4′ @ ṫ ≫

˙∀ṫ: ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ ṙ′ ˙+ ṫ =^{p}
(ṙ ˙+ ṫ)′ ;
L08: MP′ ⊳ L07 ⊳ L06 ≫  ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′  □

5.8 Bevis for LEMMA3.2(h)

5.8.1 Bevis for basistilfælde for LEMMA3.2(h)

[S′ lemma LEMMA3.2(h)base: ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ] ^{22}

S′ proof of LEMMA3.2(h)base:

L01: S5′ ≫  ṫ ˙+ ˙0 =^{p} ṫ  ;
L02: LEMMA3.2(f) ≫  ṫ =^{p} ˙0 ˙+ ṫ  ;

L03: LEMMA3.2(c) ≫

ṫ ˙+ ˙0 =^{p} ṫ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒
ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ  ;
L04: MP′ ⊳ L03 ⊳ L01 ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ  ;
L05: MP′ ⊳ L04 ⊳ L02 ≫  ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ  □

22[LEMMA3.2(h)base =^{pyk} “mendelson lemma three two h base”]

5.8.2 Bevis for induktionsskridt for LEMMA3.2(h) [S′ lemma LEMMA3.2(h)induction: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ] ^{23}

S′ proof of LEMMA3.2(h)induction:

L01: S6′ ≫  ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′  ;
L02: LEMMA3.2(g) ≫  ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′  ;

L03: S2′ ≫

ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ (ṫ ˙+ ṙ)′ =^{p}
(ṙ ˙+ ṫ)′ ;

L04: LEMMA3.2(c) ≫ ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′ ˙⇒ (ṫ ˙+ ṙ)′ =^{p}

(ṙ ˙+ ṫ)′ ˙⇒ ṫ ˙+ ṙ′ =^{p} (ṙ ˙+ ṫ)′ ;

L05: MP′ ⊳ L04 ⊳ L01 ≫

(ṫ ˙+ ṙ)′ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ ṫ ˙+ ṙ′ =^{p}
(ṙ ˙+ ṫ)′ ;

L06: TImp ⊳ L03 ⊳ L05 ≫

ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p}
(ṙ ˙+ ṫ)′ ;

L07: LEMMA3.2(d) ≫ ṫ ˙+ ṙ′ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ ṙ′ ˙+ ṫ =^{p}

(ṙ ˙+ ṫ)′ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ ;

L08: TImp ⊳ L06 ⊳ L07 ≫

ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṙ′ ˙+ ṫ =^{p}

(ṙ ˙+ ṫ)′ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ ;

L09: CImp ⊳ L08 ≫

ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ ṫ ˙+ ṙ =^{p}
ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ  ;
L10: MP′ ⊳ L09 ⊳ L02 ≫ ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ □

5.8.3 Samling af delbeviser S′ proof of LEMMA3.2(h): L01: S9′ ≫ ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ ˙⇒ ˙∀ṙ: (ṫ ˙+ ṙ =^{p}

ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ) ˙⇒

˙∀ṙ: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ;

L02: LEMMA3.2(h)base ≫ ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ ;

L03: MP′ ⊳ L01 ⊳ L02 ≫

˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p}
ṙ′ ˙+ ṫ) ˙⇒ ˙∀ṙ: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ;
L04: LEMMA3.2(h)induction ≫ ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ ;

L05: Gen′ ⊳ L04 ≫

˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p}
ṙ′ ˙+ ṫ) ;
L06: MP′ ⊳ L03 ⊳ L05 ≫ ˙∀ṙ: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ;

L07: A4′ @ ṙ ≫

˙∀ṙ: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ =^{p}
ṙ ˙+ ṫ  ;
L08: MP′ ⊳ L07 ⊳ L06 ≫  ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ  □

23[LEMMA3.2(h)induction =^{pyk} “mendelson lemma three two h induction”]

6 Litteratur

[1] K. Grue. Peano Axioms.

http://www.diku.dk/ grue/logiweb/20050502/home/grue/peano/GRD-2005-06-22-UTC-07-23-31-271829/vector/page.lgw

[2] K. Grue. Base Page.

http://www.diku.dk/ grue/logiweb/20050502/home/grue/base/GRD-2005-06-22-UTC-06-58-05-413682/vector/page.lgw

[3] Elliott Mendelson. Introduction to Mathematical Logic - CRC press 2001.

7 TEX definitioner

[LEMMA3.2(a) =^{tex} “LEMMA 3.2(a)”] [LEMMA3.2(b) =^{tex} “LEMMA 3.2(b)”] [LEMMA3.2(c) =^{tex} “LEMMA 3.2(c)”] [LEMMA3.2(d) =^{tex} “LEMMA 3.2(d)”] [LEMMA3.2(f) =^{tex} “LEMMA 3.2(f)”] [LEMMA3.2(g) =^{tex} “LEMMA 3.2(g)”] [LEMMA3.2(h) =^{tex} “LEMMA 3.2(h)”] [IMV =^{tex} “IMV”] [CImp =^{tex} “CImp”] [TImp =^{tex} “TImp”] [LEMMA3.2(f)base =^{tex} “LEMMA 3.2(f) base”] [LEMMA3.2(f)induction =^{tex} “LEMMA 3.2(f) induction”] [LEMMA3.2(g)base =^{tex} “LEMMA 3.2(g) base”] [LEMMA3.2(g)induction =^{tex} “LEMMA 3.2(g) induction”] [LEMMA3.2(h)base =^{tex} “LEMMA 3.2(h) base”] [LEMMA3.2(h)induction =^{tex} “LEMMA 3.2(h) induction”]

8 Sidens navn

[rapport =^{pyk} “rapport”] [ =^{pyk} “blank space”]