Formelt bevis for den kommutative lov for addition i peano-aritmetik

Ole Hyldahl Hansen 260579

30. juni 2005

Indhold

1 Indledning 3

2 Logiweb 3

3 Peano-aritmetik 4 3.1 Grammatik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.2 Meta- og konkrete variabler . . . . . . . . . . . . . . . . . . . . . 5 3.3 Teorien S’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

4 Den kommutative lov for addition 9

4.1 Hjælpesætninger . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.1.1 MPTwice . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.1.2 Lemma M1.7 . . . . . . . . . . . . . . . . . . . . . . . . . 10 4.1.3 Lemma Weaken . . . . . . . . . . . . . . . . . . . . . . . . 10 4.1.4 Tautologi 1 . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4.1.5 Tautologi 2 . . . . . . . . . . . . . . . . . . . . . . . . . . 12 4.1.6 Tautologi 3 . . . . . . . . . . . . . . . . . . . . . . . . . . 12 4.1.7 Tautologi 4 . . . . . . . . . . . . . . . . . . . . . . . . . . 12

4.2 Lemmaer fra Peanoaritmetik . . . . . . . . . . . . . . . . . . . . 13 4.2.1 Lemma 3.2 (a) . . . . . . . . . . . . . . . . . . . . . . . . 13 4.2.2 Lemma 3.2 (b) . . . . . . . . . . . . . . . . . . . . . . . . 13 4.2.3 Lemma 3.2 (c) . . . . . . . . . . . . . . . . . . . . . . . . 14 4.2.4 Lemma 3.2 (d) . . . . . . . . . . . . . . . . . . . . . . . . 14 4.2.5 Lemma 3.2 (f) . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2.6 Lemma 3.2 (g) . . . . . . . . . . . . . . . . . . . . . . . . 16 4.2.7 Lemma 3.2 (g) II . . . . . . . . . . . . . . . . . . . . . . . 17 4.2.8 Lemma 3.2 (h) basis . . . . . . . . . . . . . . . . . . . . . 18

4.3 Kommutativitet - Lemma 3.2 (h) . . . . . . . . . . . . . . . . . . 19

5 Konklusion 20 A Definitioner 21

A.1 Denne sides navn . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 A.2 Variabler i Peano-aritmetik . . . . . . . . . . . . . . . . . . . . . 21

B Litteraturliste 22

1 Indledning

Det skal bevises, at den kommutative lov for addition gælder i Peano-aritmetik. Dette er på ingen måde et nyt resultat, så rapporten skal ses som en opgave i at arbejde med formelle beviser i en logisk teori. Særlig interessent er det, at rapporten er skrevet i systemet Logiweb. Dette tillader en maskine at verificere de givne beviser ud fra de definerede axiomer og inferensregler, men stiller om muligt endnu højere krav til stringens i beviserne end traditionelle beviser inden for logikken. Der vil blive taget udgangspunkt i Mendelson [5], så det meste af arbejdet vil bestå i, at tilpasse beviserne så de kan forstås af Logiweb, og sørge for at alle nødvendige hjælpesætninger er bevist i mindste detalje.

2 Logiweb

Denne rapport er lavet i systemet Logiweb [2]. Systemet giver dels mulighed for at lave præsentable formelle beviser, men dets vigtigste formål er nok at kunne verificere korrekt skrevne beviser. I modsætning til mere traditionelle beviser i den matematiske litteratur kan beviser inden for logikken ofte skrives så tilstrækkeligt formelt op, at de kan verificeres ved en rent mekanisk procedure.

I Logiweb-forstand er denne rapport en side. Sider kan definere et antel logiske teorier og kan publiseres, referere andre sider og selv refereres på en måde meget lig dokumenter på WWW, hvilket skulle gøre det muligt at skabe komplekse logiske teorier ved at basere nye teorier på allerede eksisterende og formelt beviste teorier. Peano-aritmetik er dog en relativt simpel teori, og derfor baserer denne rapport sig kun på de helt basale sider base og check.

Alle matematiske konstruktioner som Logiweb-systemet gøres bekendt med, vises i kantede parenteser, som f.eks. denne reference til et lemma [M1.7]. Læseren er hermed klar over, at konstruktionen er passende defineret på den pågældende side. Lemmaer kan dog stadig postuleres uden beviser, men hvis et bevis er tilstede, vil bevis-checkeren på siden check have verificeret dette og evt. fejl vil blive rapporteret på en særlig diagnose-side.

Under udarbejdelsen er denne rapport løbende blevet checket, og den endelige udgave meldes fri for formelle fejl af Logiweb, hvilket læseren selv kan kontrollere ved at besøge rapportens hjemsted [1] på internettet, hvor også al kildekode er tilgængelig.

Når en konstruktion defineres i logiweb skal både gramatikken og en række aspekter defineres, der tilsammen beskriver for Logiweb hvordan konstruktionen skal bruges, og hvordan den skal optræde i det færdige dokument. Hvordan dette maskineri præcist fungerer er omfattende, og her henvises til base-siden [3]. Her skal blot nævnes, at introduktionen af nye konstruktioner giver anledning til pykfodnoter, der automatisk indsættes af Logiweb. Disse beskriver sammenhængen mellem en konstruktions navn i kildeteksten og i den færdigtformaterede tekst, og kan uden videre ignoreres, hvis man ikke ønsker at læse kildeteksten.

3 Peano-aritmetik

Peano-aritmetik er en formel teori for de naturlige tal, og egner sig godt til behandling i Logiweb. Teorien er relativt enkel at definere, men der kan alligvel bevises en meget stor mængde interessante sætninger. Fordi næsten enhver har regnet med naturlige tal siden barndommen, er Logiweb’s uvilje mod at acceptere andet end strengt formelt korrekte beviser en vigtig egenskab, da man ellers nemt kommer til at benytte ubeviste antagelser, der virker fuldstændigt oplagte.

3.1 Grammatik

Ved en term T i peano-aritmetik forstås en af følgende konstruktioner: konstanten nul [˙0]^{1}, efterfølgeroperatoren [x′]^{2}, plus [x ˙+ y]^{3} og gange [x ˙· y]^{4}. Alle konstruktioner hørende til Peano-aritmetik er i denne rapport markeret med en prik^{5}, for at kunne skelne dem fra lignende konstruktioner defineret på basesiden. Teorien gør også brug af de konkrete variabler [ȧ]^{6}, [ḃ]^{7}, ..., der varierer over konstante termer.

Formler P kan bygges op af lighed [x =^{p} y]^{8}, negation [ ˙¬ x]^{9}, implikation [x ˙⇒ y]^{10} og al-kvantoren [ ˙∀x: y]^{11}.

1[˙0 =^{pyk} “peano zero”]

2[x′ =^{pyk} “∗ peano succ”]

3[x ˙+ y =^{pyk} “∗ peano plus ∗”]

4[x ˙· y =^{pyk} “∗ peano times ∗”]

5Lighed skrives dog [x =^{p} y], da lighed med en prik over betyder “defineres som” i Logiweb.

6[ȧ =^{pyk} “peano a”]

7[ḃ =^{pyk} “peano b”]

8[x =^{p} y =^{pyk} “∗ peano is ∗”]

9[ ˙¬ x =^{pyk} “peano not ∗”]

10[x ˙⇒ y =^{pyk} “∗ peano imply ∗”]

11[ ˙∀x: y =^{pyk} “peano all ∗ indeed ∗”]

Kort kan grammatikken skrives som:

T ::= ˙0 | T′ | T ˙+ T | T ˙· T | v̇ar
F ::= T ˙= T | ˙¬F | F ˙⇒ F | ˙∀v̇ar: F

hvor v̇ar er en vilkårlig konkret variabel. Plus og gange er venstreassociative mens implikation er højreassociativ. Operatorenes præcedens er i faldende orden ′, ˙·, ˙+, ˙¬, ˙∀, ˙⇒. Der er ingen andre konstanter end ˙0, men de øvrige naturlige tal [˙1]^{12}, [˙2]^{13} ..., kan makrodefineres således: [˙1 ¨= ˙0′], [˙2 ¨= ˙1′], ... . I denne rapport vil der dog ikke blive brug for andre tal end [˙0], ligesom gange og negation heller ikke vil blive set mere.

3.2 Meta- og konkrete variabler

Det er vigtigt at skelne skarpt mellem metavariabler og konkrete variabler [ẋ]^{14}. I Logiweb vil metavariabler blive skrevet store og kursiverede, mens konkrete variabler i Peano-aritmetik får en prik over. Eksempelvis er [T ] en metavariabel, mens [ṫ] er den tilsvarende konkrete variabel.

Som udgangspunkt er sætninger omhandlende metavariabler at fortrække fremfor samme sætning involverende konkrete variabler. Med metavariabler kommer Logiweb’s unificeringssystem til sin ret, og man kan frit udskifte variabler med vilkårlige (lovlige) konstruktioner. Visse beviser (specielt beviser involverende induktion) lader sig dog ikke gennemføre for metavariabler i Logiweb, så konkrete variabler vil blive brugt, hvor det er nødvendigt.

Nogle af axiomerne i Peano-aritmetik stiller krav om, at der ved substitution af termer for en variabel ikke fejlagtigt bliver bundet variabler af kvantorer (det såkaldte “T er fri for x i S”-begreb i Mendelson). Eftersom Logiweb ikke har nogen ide om, hvilke regler vores Peano-variabler skal adlyde, må disse regler defineres eksplicit. Dette gøres herunder ^{15}:

Der introduceres en operator [x^{P}]^{16}, der er sand netop hvis [x] er en Peanovariabel.

12[˙1 =^{pyk} “peano one”]

13[˙2 =^{pyk} “peano two”]

14[ẋ =^{pyk} “∗ peano var”]

15Disse definitioner er taget uændret fra [4].

16[x^{P} =^{pyk} “∗ is peano var”]

[x^{P} ˙= x =^{r} ⌈ẋ⌉]

[ṅonfree(x, y)]^{17} er sand netop hvis Peano-variablen [x] ikke forekommer frit i [y]. [ṅonfree^{∗}(x, y)]^{18} er sand netop hvis Peano-variablen [x] ikke forekommer frit i en liste [y] af termer og/eller formler.

[ṅonfree(x, y) ˙= if y^{P} then ¬x =^{t} y else if ¬y =^{r} ⌈ ˙∀x: y⌉ then ṅonfree^{∗}(x, y^{t}) else if x =^{t} y^{1} then T else ṅonfree(x, y^{2})]

[ṅonfree^{∗}(x, y) ˙= x!If(y, T, ṅonfree(x, y^{h}) ¨∧ ṅonfree^{∗}(x, y^{t}))]

[ḟree⟨a|x := b⟩]^{19} er sand når substitutionen [⟨a |x:= b⟩] er fri. [ḟree^{∗}⟨a|x := b⟩]^{20} har samme betydning for en liste af termer [a].

[ḟree⟨a|x := b⟩ ˙= x!b! if a^{P} then T else if ¬a =^{r} ⌈ ˙∀u: v⌉ then ḟree^{∗}⟨a^{t}|x := b⟩ else if a^{1} =^{t} x then T else if ṅonfree(x, a^{2}) then T else if ¬ṅonfree(a^{1}, b) then F else ḟree⟨a^{2}|x := b⟩]

[ḟree^{∗}⟨a|x := b⟩ ˙= x!b!If(a, T, ḟree⟨a^{h}|x := b⟩ ¨∧ ḟree^{∗}⟨a^{t}|x := b⟩)]

[a≡⟨b|x := c⟩]^{21} er sand når [a] er [⟨b |x:= c⟩]. [a≡⟨^{∗}b|x := c⟩]^{22} har samme betydning for lister [a] og [b].

[a≡⟨b|x := c⟩ ˙= a!x!c! if b =^{r} ⌈ ˙∀u: v⌉ ¨∧ b^{1} =^{t} x then a =^{t} b else if b^{P} ∧ b =^{t} x then a =^{t} c else a =^{r} b ¨∧ a^{t}≡⟨^{∗}b^{t}|x := c⟩]

17[ṅonfree(x, y) =^{pyk} “peano nonfree ∗ in ∗ end nonfree”] 18[ṅonfree^{∗}(x, y) =^{pyk} “peano nonfree star ∗ in ∗ end nonfree”] 19[ḟree⟨a|x := b⟩ =^{pyk} “peano free ∗ set ∗ to ∗ end free”] 20[ḟree^{∗}⟨a|x := b⟩ =^{pyk} “peano free star ∗ set ∗ to ∗ end free”] 21[a≡⟨b|x := c⟩ =^{pyk} “peano sub ∗ is ∗ where ∗ is ∗ end sub”] 22[a≡⟨^{∗}b|x := c⟩ =^{pyk} “peano sub star ∗ is ∗ where ∗ is ∗ end sub”]

[a≡⟨^{∗}b|x := c⟩ ˙= b!x!c!If(a, T, a^{h}≡⟨b^{h}|x := c⟩ ¨∧ a^{t}≡⟨^{∗}b^{t}|x := c⟩)]

3.3 Teorien S’

Den formelle teori, som vil danne grundlag for denne rapport, vil blive betegnet [S′]^{23}, og er næsten identisk med teorien S, som defineres i Mendelson. Teorien indeholder de 5 axiomer^{24} fra førsteordens prædikatkalkulen [A1′]^{25}, [A2′]^{26}, [A3′]^{27}, [A4′]^{28}, og [A5′]^{29}, samt de 2 inferensregler [MP′]^{30} og [Gen′]^{31}:

[Theory S′]

[S′ rule A1′: ∀A: ∀B: A ˙⇒ B ˙⇒ A]

[S′ rule A2′: ∀A: ∀B: ∀C: (A ˙⇒ B ˙⇒ C) ˙⇒ (A ˙⇒ B) ˙⇒ A ˙⇒ C]

[S′ rule A3′: ∀A: ∀B: ( ˙¬ B ˙⇒ ˙¬ A) ˙⇒ ( ˙¬ B ˙⇒ A) ˙⇒ B]

[S′ rule A4′: ∀C: ∀A: ∀X: ∀B: ⌈A⌉≡⟨⌈B⌉|⌈X ⌉ := ⌈C⌉⟩ ⊢⊢ ˙∀X: B ˙⇒ A]

[S′ rule A5′: ∀X: ∀A: ∀B: ṅonfree(⌈X ⌉, ⌈A⌉) ⊢⊢ ˙∀X: (A ˙⇒ B) ˙⇒ A ˙⇒ ˙∀X: B]

[S′ rule MP′: ∀A: ∀B: A ˙⇒ B ⊢ A ⊢ B]

[S′ rule Gen′: ∀X: ∀A: A ⊢ ˙∀X: A] Derudover er der også de egentlige axiomer fra Peano-aritmetik [S1′]^{32}, [S2′]^{33}, [S3′]^{34}, [S4′]^{35}, [S5′]^{36}, [S6′]^{37}, [S7′]^{38}, [S8′]^{39}, og [S9′]^{40}:

23[S′ =^{pyk} “system prime s”] 24Strengt taget er der tale om axiomsskemaer, men denne forskel er ikke væsentlig i denne sammenhæng.

25[A1′ =^{pyk} “axiom prime a one”] 26[A2′ =^{pyk} “axiom prime a two”] 27[A3′ =^{pyk} “axiom prime a three”] 28[A4′ =^{pyk} “axiom prime a four”] 29[A5′ =^{pyk} “axiom prime a five”] 30[MP′ =^{pyk} “rule prime mp”] 31[Gen′ =^{pyk} “rule prime gen”]

[S′ rule S1′: ∀A: ∀B: ∀C: A =^{p} B ˙⇒ A =^{p} C ˙⇒ B =^{p} C]

[S′ rule S2′: ∀A: ∀B: A =^{p} B ˙⇒ A′ =^{p} B′]

[S′ rule S3′: ∀A: ¬˙0 =^{p} A′]

[S′ rule S4′: ∀A: ∀B: A′ =^{p} B′ ˙⇒ A =^{p} B]

[S′ rule S5′: ∀A: A ˙+ ˙0 =^{p} A]

[S′ rule S6′: ∀A: ∀B: A ˙+ B′ =^{p} (A ˙+ B)′]

[S′ rule S7′: ∀A: A ˙· ˙0 =^{p} ˙0]

[S′ rule S8′: ∀A: ∀B: A ˙·(B′) =^{p} (A ˙· B) ˙+ A]

[S′ rule S9′: ∀A: ∀B: ∀C: ∀X:

B≡⟨A|X := ˙0⟩ ⊢⊢ C≡⟨A|X := X′⟩ ⊢⊢

B ˙⇒ ˙∀X: (A ˙⇒ C) ˙⇒ ˙∀X: A]

Bortset fra de Logiweb-specifikke tilføjelser, adskiller teorien [S′] sig fra teorien S i Mendelson ved, at axiomerne [S1′]-[S9′] primært er angivet med metavariabler i stedet for konkrete variabler, og dermed svarer axiomerne til lemma 3.2(1-9) i Mendelson. Teorien kunne sagtens være formuleret på samme måde som i Mendelson, men dette havde blot gjort beviser meget længere pga. omfattende brug af [A4′] og generaliseringer. Den præsenterede formulering viser sig meget mere anvendelig i praksis, og vil derfor blive benyttet.

32[S1′ =^{pyk} “axiom prime s one”]

33[S2′ =^{pyk} “axiom prime s two”]

34[S3′ =^{pyk} “axiom prime s three”]

35[S4′ =^{pyk} “axiom prime s four”]

36[S5′ =^{pyk} “axiom prime s five”]

37[S6′ =^{pyk} “axiom prime s six”]

38[S7′ =^{pyk} “axiom prime s seven”]

39[S8′ =^{pyk} “axiom prime s eight”]

40[S9′ =^{pyk} “axiom prime s nine”]

4 Den kommutative lov for addition

Nu da grundlaget er på plads, er det tid til at løse den stillede opgave. Der skal leveres et bevis for, at den den kommutative lov gælder for addition i Peanoaritmetik, dvs. at t+r = r+t for to vilkårlige ikke-negative heltal t og r. Skrevet i Logiweb’s notation skal ˙∀ṫ: ˙∀ṙ: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ bevises^{41}.

Mendelson leverer et bevis for denne sætning, men for at kunne komme så langt skal der bevises en del forskellige hjælpesætninger. Ser man i Mendelson indser man hurtigt, at beviset for kommutativitet [L3.2(h)′]^{42} afhænger af de foregående lemmaer [L3.2(a)′]^{43}, [L3.2(b)′]^{44}, [L3.2(c)′]^{45}, [L3.2(d)′]^{46}, [L3.2(f)′]^{47} og [L3.2(g)′]^{48}. Derudover vil det være praktisk at bevise at antal tautologier, som vil kunne spare en del gentagelser af bevislinier. Der vil som udgangspunkt ikke blive bevist flere sætninger end strengt nødvendigt for at kunne gennemføre beviset for L3.2(h)′.

4.1 Hjælpesætninger

Der vil nu blive fremsat og bevist en række forskellige tautologier, der er meget nyttige at have ved hånden. Disse hjælpesætninger bruger kun begreber fra den rene prædikatkalkule, og vil derfor kunne bevises i mange andre teorier end Peano-aritmetik.

4.1.1 MPTwice

I beviser har man af og til linier af formen [A ˙⇒ B ˙⇒ C], og man ønsker at konkludere [C] ud fra [A] og [B]. Dette kan naturligvis let klares med to anvendelser af modus ponens, men der kan i disse situationer spares en bevislinie ved at benytte det enkle lemma [MPTwice]^{49}:

41I denne sammenhæng spiller kvantorene ingen rolle, da de kan tilføjes eller fjernes efter behag.

42[L3.2(h)′ =^{pyk} “lemma prime three two h”]

43[L3.2(a)′ =^{pyk} “lemma prime three two a”]

44[L3.2(b)′ =^{pyk} “lemma prime three two b”]

45[L3.2(c)′ =^{pyk} “lemma prime three two c”]

46[L3.2(d)′ =^{pyk} “lemma prime three two d”]

47[L3.2(f)′ =^{pyk} “lemma prime three two f”]

48[L3.2(g)′ =^{pyk} “lemma prime three two g”]

49[MPTwice =^{pyk} “lemma mp twice”]

[S′ lemma MPTwice: ∀A: ∀B: ∀C: A ˙⇒ B ˙⇒ C ⊢ A ⊢ B ⊢ C]

Beviset for lemmaet er naturligvis blot at benytte modus ponens to gange, men man vil bemærke at der alligevel kræves 8 bevislinier pga. nogle Logiwebteknikaliteter. Det skulle dog være rimeligt enkelt at forstå meningen med disse liner, idet de simpethen blot remser lemmaets præmisser op igen.

S′ proof of MPTwice:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A ˙⇒ B ˙⇒ C  ;
L05: Premise ≫  A  ;
L06: Premise ≫  B  ;
L07: MP′ ⊳ L04 ⊳ L05 ≫  B ˙⇒ C  ;
L08: MP′ ⊳ L07 ⊳ L06 ≫  C  □

4.1.2 Lemma M1.7

Fra Mendelson tages lemma 1.7 [M1.7]^{50}:

[S′ lemma M1.7: ∀B: B ˙⇒ B]

S′ proof of M1.7:

L01: Arbitrary ≫  B  ;
L02: A1′ ≫  B ˙⇒ (B ˙⇒ B) ˙⇒ B  ;
L03: A2′ ≫  {(B ˙⇒ (B ˙⇒ B) ˙⇒ B) ˙⇒ \atop (B ˙⇒ B ˙⇒ B) ˙⇒ B ˙⇒ B  ;}
L04: MP′ ⊳ L03 ⊳ L02 ≫  (B ˙⇒ B ˙⇒ B) ˙⇒ B ˙⇒ B  ;
L05: A1′ ≫  B ˙⇒ B ˙⇒ B  ;
L06: MP′ ⊳ L04 ⊳ L05 ≫  B ˙⇒ B  □

4.1.3 Lemma Weaken

Det vil blive nødvendigt at gøre et udsagn “svagere”, dvs. gøre det betinget af et nyt udsagn, hvilket naturligvis altid er tilladt. Dette udtrykkes i lemmaet [Weaken]^{51}:

50[M1.7 =^{pyk} “mendelson one seven”]

51[Weaken =^{pyk} “lemma weaken”]

[S′ lemma Weaken: ∀A: ∀B: A ⊢ B ˙⇒ A]

Beviset er helt enkelt:

S′ proof of Weaken:

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

4.1.4 Tautologi 1

[Taut1]^{52} er det første af fire tautologier, der er en smule mere komplicerede end de hidtil sete. Disse tautologier har ikke nogle oplagte navne, hvorfor de blot vil blive nummereret. Dette føste lemma tillader, om man ombytter rækkefølgen af visse præmisser i en implikation:

[S′ lemma Taut1: ∀A: ∀B: ∀C: A ˙⇒ B ˙⇒ C ⊢ B ˙⇒ A ˙⇒ C]

Beviset er ikke langt, men demonstrerer alligvel, at man naturligvis kan referere tilbage til tidligere beviste lemmaer. Logiweb checker, at alle refererede lemmaer også er beviste, og at der ikke er cykliske afhængigheder mellem beviser.

S′ proof of Taut1:

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

L09: A1′ ≫  B ˙⇒ A ˙⇒ B  ;
L10: MPTwice ⊳ L08 ⊳ L07 ⊳ L09 ≫ B ˙⇒ A ˙⇒ C  □

52[Taut1 =^{pyk} “lemma tautology one”]

4.1.5 Tautologi 2 Lemma [Taut2]^{53} udtrykker en form for transitivitet af implikationsoperatoren. [S′ lemma Taut2: ∀D: ∀E: ∀F: (D ˙⇒ E) ⊢ (E ˙⇒ F) ⊢ (D ˙⇒ F)] S′ proof of Taut2:

L01: Arbitrary ≫  D  ;
L02: Arbitrary ≫  E  ;
L03: Arbitrary ≫  F  ;
L04: Premise ≫  D ˙⇒ E  ;
L05: Premise ≫  E ˙⇒ F  ;
L06: A1′ ≫  (E ˙⇒ F) ˙⇒ D ˙⇒ (E ˙⇒ F)  ;
L07: MP′ ⊳ L06 ⊳ L05 ≫  D ˙⇒ E ˙⇒ F  ;
L08: A2′ ≫  {(D ˙⇒ E ˙⇒ F) ˙⇒ ((D ˙⇒ E) ˙⇒ \atop (D ˙⇒ F))  ;}
L09: MPTwice ⊳ L08 ⊳ L07 ⊳ L04 ≫ D ˙⇒ F  □

4.1.6 Tautologi 3 Med lemma [Taut3]^{54} kan man eliminere en betingelse fra en dobbeltimplikation, såfremt det kan bevises, at betingelsen altid er opfyldt. [S′ lemma Taut3: ∀A: ∀B: ∀C: A ˙⇒ B ⊢ A ˙⇒ B ˙⇒ C ⊢ A ˙⇒ C] S′ proof of Taut3:

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

4.1.7 Tautologi 4 Tautologi [Taut4]^{55} er en svagere variant af forrige tautologi.

53[Taut2 =^{pyk} “lemma tautology two”]

54[Taut3 =^{pyk} “lemma tautology three”]

55[Taut4 =^{pyk} “lemma tautology four”]

[S′ lemma Taut4: ∀A: ∀B: ∀C: A ⊢ B ˙⇒ A ˙⇒ C ⊢ B ˙⇒ C] S′ proof of Taut4:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A  ;
L05: Premise ≫  B ˙⇒ A ˙⇒ C  ;
L06: Taut1 ⊳ L05 ≫  A ˙⇒ B ˙⇒ C  ;
L07: MP′ ⊳ L06 ⊳ L04 ≫  B ˙⇒ C  □

4.2 Lemmaer fra Peanoaritmetik

4.2.1 Lemma 3.2 (a) Det første lemma fra Mendelson udtrykker at lighedstegnet er refleksivt: [S′ lemma L3.2(a)′: ∀T : T =^{p} T ] Beviset er kort, og benytter addition med nul som “trick”: S′ proof of L3.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: MPTwice ⊳ L03 ⊳ L02 ⊳ L02 ≫ T =^{p} T  □

4.2.2 Lemma 3.2 (b) Lemma [L3.2(b)′] siger, at lighedstegnet er symmetrisk: [S′ lemma L3.2(b)′: ∀T : ∀R: T =^{p} R ˙⇒ R =^{p} T ] S′ proof of L3.2(b)′:

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: S1′ ≫  T =^{p} R ˙⇒ (T =^{p} T ˙⇒ R =^{p} T )  ;
L04: Taut1 ⊳ L03 ≫  T =^{p} T ˙⇒ (T =^{p} R ˙⇒ R =^{p} T )  ;

L05: L3.2(a)′ ≫  T =^{p} T  ;
L06: MP′ ⊳ L04 ⊳ L05 ≫  T =^{p} R ˙⇒ R =^{p} T  □

4.2.3 Lemma 3.2 (c) Dette lemma siger, at lighedstegnet er transitivt. Med dette lemma er det nu bevist, at lighedstegnet er en ækvivalensrelation. [S′ lemma L3.2(c)′: ∀T : ∀R: ∀S: T =^{p} R ˙⇒ (R =^{p} S ˙⇒ T =^{p} S)] Med de allerede beviste lemmaer er dette bevis helt enkelt: S′ proof of L3.2(c)′:

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

4.2.4 Lemma 3.2 (d) Dette lemma er lidt besværligt at beskrive med ord, men dets mening skulle være klar og det vil vise sig særdeles nyttigt i flere af de kommende beviser [S′ lemma L3.2(d)′: ∀T : ∀R: ∀S: R =^{p} T ˙⇒ (S =^{p} T ˙⇒ R =^{p} S)] S′ proof of L3.2(d)′:

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

4.2.5 Lemma 3.2 (f)

Lemma L3.2(f)′ er det første lemma, der kræver et induktivt bevis. Dette bevirker, at lemmaet må formuleres med konkrete variabler i stedet for metavariabler som de tidligere lemmaer har benyttet. Der bevises en version, hvor den frie variabel er kvantoriseret, da denne denne form er nemmere at arbejde med i senere beviser.

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

Som ved enhver induktion skal der både bevises et basistilfælde og et induktionsskridt for at axiom S9′ kan bruges til at konkludere det ønskede. Beviset er dog ikke længere, end at begge dele uden problemer kan bevises i samme lemma. Var beviset blevet langt, ville det nok have været mere overskueligt, at dele lemmaet op i flere dele.

S′ proof of L3.2(f)′:

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

L05: A1′ ≫ ˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒

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

L06: MP′ ⊳ L05 ⊳ L04 ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′  ;
L07: M1.7 ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ  ;
L08: S2′ ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} (˙0 ˙+ ṫ)′  ;
L09: Taut2 ⊳ L07 ⊳ L08 ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} (˙0 ˙+ ṫ)′  ;

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

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

L11: Taut2 ⊳ L08 ⊳ L10 ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ (˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′ ˙⇒

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

L12: Taut3 ⊳ L06 ⊳ L11 ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′  ;
L13: Gen′ ⊳ L12 ≫  ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′)  ;

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

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

L15: MPTwice ⊳ L14 ⊳ L03 ⊳ L13 ≫ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ  □

4.2.6 Lemma 3.2 (g)

Dette sidste lemma inden L3.2(h)′ er i sig selv ikke specielt interessant, men er nødvendigt for at det endelige induktive argument kan gives.

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

Beviset er længere og mere komplekst end nogen af de tidligere beviser. Igen er det et bevis ved induktion, og fremgangsmåden er i vid udstrækning den samme som i Mendelson. Beviset er gjort en anelse kortere ved at anvende en makro H.

S′ proof of L3.2(g)′:

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

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

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

L06: MPTwice ⊳ L05 ⊳ L01 ⊳ L04 ≫ ṫ′ ˙+ ˙0 =^{p} (ṫ ˙+ ˙0)′  ;
L07: Local ≫  H = ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′  ;
L08: S6′ ≫  ṫ′ ˙+ ṙ′ =^{p} (ṫ′ ˙+ ṙ)′  ;
L09: Weaken ⊳ L08 ≫  H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} (ṫ′ ˙+ ṙ)′  ;

L10: S2′ ≫

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

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

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

L12: MP′ ⊳ L11 ⊳ L08 ≫

(ṫ′ ˙+ ṙ)′ =^{p} (ṫ ˙+ ṙ)′′ ˙⇒ ṫ′ ˙+ ṙ′ =^{p}
(ṫ ˙+ ṙ)′′ ;
L13: Taut2 ⊳ L10 ⊳ L12 ≫  H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′′  ;
L14: S6′ ≫  ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′  ;

L15: S2′ ≫

ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′ ˙⇒ (ṫ ˙+ ṙ′)′ =^{p}
(ṫ ˙+ ṙ)′′ ;
L16: MP′ ⊳ L15 ⊳ L14 ≫ (ṫ ˙+ ṙ′)′ =^{p} (ṫ ˙+ ṙ)′′ ;

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

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

L18: Taut2 ⊳ L13 ⊳ L17 ≫ H ˙⇒ (ṫ ˙+ ṙ′)′ =^{p} (ṫ ˙+ ṙ)′′ ˙⇒

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

L19: Taut1 ⊳ L18 ≫ (ṫ ˙+ ṙ′)′ =^{p} (ṫ ˙+ ṙ)′′ ˙⇒ H ˙⇒

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

L20: MP′ ⊳ L19 ⊳ L16 ≫  H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′  ;
L21: Gen′ ⊳ L20 ≫  ˙∀ṙ: (H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′)  ;

L22: S9′ ≫ ṫ′ ˙+ ˙0 =^{p} (ṫ ˙+ ˙0)′ ˙⇒ ( ˙∀ṙ: (H ˙⇒

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

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

L23: MPTwice ⊳ L22 ⊳ L06 ⊳ L21 ≫ ˙∀ṙ: ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′  ;
L24: Gen′ ⊳ L23 ≫  ˙∀ṫ: ˙∀ṙ: ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′  □

4.2.7 Lemma 3.2 (g) II

I beviset for L3.2(h)′ skal L3.2(g)′ benyttes, men netop fordi der skal bevises kommutativitet, skal variablerne ṫ og ṙ benyttes i omvendt rækkefølge. At denne ombytning er tilladt er intuitivt oplagt for en menneskelig læser, men Logiweb kræver dette bevist i pinagtig detalje. For at gøre beviset for L3.2(h)′ kortere, er her en udgave af L3.2(g)′ kaldet [L3.2(g)′II]^{56}, der passer perfekt til senere brug.

Hjælpesætningen har tre umiddelbart meget komplicerede sidebetingelser. Disse betingelser siger tilsammen, at det er tilladt at udskifte ṫ med ṙ og omvendt. Fordi disse udskiftninger ikke kan foretages samtidigt, er det nødvendigt at benytte en midlertidig tredie variabel ṡ. Det endelige lemma er ikke kvantoriseret, hvilket er godt, da det netop er skrevet med samme konkrete variabler, som skal bruges senere.

[S′ lemma L3.2(g)′II: ⌈ ˙∀ṙ: ṡ′ ˙+ ṙ =^{p} (ṡ ˙+ ṙ)′⌉≡⟨⌈ ˙∀ṙ: ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′⌉|⌈ṫ⌉ := ⌈ṡ⌉⟩ ⊢⊢

⌈ṡ′ ˙+ ṫ =^{p} (ṡ ˙+ ṫ)′⌉≡⟨⌈ṡ′ ˙+ ṙ =^{p} (ṡ ˙+ ṙ)′⌉|⌈ṙ⌉ := ⌈ṫ⌉⟩ ⊢⊢ ⌈ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′⌉≡⟨⌈ṡ′ ˙+ ṫ =^{p}

(ṡ ˙+ ṫ)′⌉|⌈ṡ⌉ := ⌈ṙ⌉⟩ ⊢⊢ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′]

Beviset udskifter først ṫ med ṡ, derefter ṙ med ṫ og til sidst ṡ med ṙ ved hjælp af axiom A4′. Sidebetingelserne skal explicit angives, fot at Logiweb kan kontrollere, at substitutionerne er legale.

S′ proof of L3.2(g)′II:

L01: L3.2(g)′ ≫  ˙∀ṫ: ˙∀ṙ: ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′  ;
L02: Side-condition ≫  ⌈ ˙∀ṙ: ṡ′ ˙+ ṙ  =^{p}
(ṡ ˙+ ṙ)′⌉≡⟨⌈ ˙∀ṙ: ṫ′ ˙+ ṙ  =^{p}
(ṫ ˙+ ṙ)′⌉|⌈ṫ⌉ := ⌈ṡ⌉⟩ ;

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

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

56[L3.2(g)′II =^{pyk} “lemma prime three two g rev”]

L04: MP′ ⊳ L03 ⊳ L01 ≫  ˙∀ṙ: ṡ′ ˙+ ṙ =^{p} (ṡ ˙+ ṙ)′  ;

L05: Side-condition ≫ ⌈ṡ′ ˙+ ṫ =^{p} (ṡ ˙+ ṫ)′⌉≡⟨⌈ṡ′ ˙+ ṙ =^{p}

(ṡ ˙+ ṙ)′⌉|⌈ṙ⌉ := ⌈ṫ⌉⟩ ;

L06: A4′ ⊳ ⊳ L05 ≫ ( ˙∀ṙ: ṡ′ ˙+ ṙ =^{p} (ṡ ˙+ ṙ)′) ˙⇒

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

L07: MP′ ⊳ L06 ⊳ L04 ≫  ṡ′ ˙+ ṫ =^{p} (ṡ ˙+ ṫ)′  ;
L08: Gen′ ⊳ L07 ≫  ˙∀ṡ: ṡ′ ˙+ ṫ =^{p} (ṡ ˙+ ṫ)′  ;

L09: Side-condition ≫ ⌈ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′⌉≡⟨⌈ṡ′ ˙+ ṫ =^{p}

(ṡ ˙+ ṫ)′⌉|⌈ṡ⌉ := ⌈ṙ⌉⟩ ;

L10: A4′ ⊳ ⊳ L09 ≫ ( ˙∀ṡ: ṡ′ ˙+ ṫ =^{p} (ṡ ˙+ ṫ)′) ˙⇒

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

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

4.2.8 Lemma 3.2 (h) basis

Beviset for [L3.2(h)′] er tilpas langt til, at det bør deles op i flere bidder. Derudover anvendes i beviset en instans af axiom A4′ som kræver at en (triviel) sidebetingelse er opfyldt. Denne sidebetingelse skal så også angives i selve lemmaet, og ser dels ikke pænt ud og kunne dels forlede læseren til at tro, at kun en svagere variant af lemma 3.2 var blevet bevist, så derfor pakkes denne sidebetingelse væk i den første halvdel af beviset for [L3.2(h)′]. Derfor bevises først en del af [L3.2(h)′] kaldet [L3.2(h)′basis]^{57}.

Denne første del tager sig også af selve induktionsargumentet, og beviser basistilfældet. [L3.2(h)′] vil så være bevist ud fra dette lemma [L3.2(h)′basis], hvis selve induktionsskridtet kan bevises.

[S′ lemma L3.2(h)′basis: ⌈ṫ =^{p} ˙0 ˙+ ṫ⌉≡⟨⌈ṫ =^{p} ˙0 ˙+ ṫ⌉|⌈ṫ⌉ := ⌈ṫ⌉⟩ ⊢⊢ ( ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ) ˙⇒ ˙∀ṙ: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ)]

S′ proof of L3.2(h)′basis:

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

L03: Side-condition ≫ ⌈ṫ =^{p} ˙0 ˙+ ṫ⌉≡⟨⌈ṫ =^{p} ˙0 ˙+ ṫ⌉|⌈ṫ⌉ :=

⌈ṫ⌉⟩ ;

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

L06: L3.2(c)′ ≫

ṫ ˙+ ˙0 =^{p} ṫ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒
ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ  ;
L07: MPTwice ⊳ L06 ⊳ L01 ⊳ L05 ≫ ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ  ;

57[L3.2(h)′basis =^{pyk} “lemma prime three two h base”]

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

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

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

L09: MP′ ⊳ L08 ⊳ L07 ≫

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

4.3 Kommutativitet - Lemma 3.2 (h)

Med alt det gjorte forarbejde er beviset for [L3.2(h)′] nu ret enkelt. [S′ lemma L3.2(h)′: ˙∀ṫ: ˙∀ṙ: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ] Beviset er naturligvis et induktionsbevis, men eftersom selve induktionsargumentet er pakket væk i [L3.2(h)′basis], har dette bevis mest til opgave at samle trådene fra forgående lemmaer. S′ proof of L3.2(h)′:

L01: S6′ ≫  ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′  ;
L02: L3.2(g)′II ≫  ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′  ;
L03: Local ≫  H = ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ  ;

L04: S2′ ≫

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

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

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

L06: MP′ ⊳ L05 ⊳ L01 ≫

(ṫ ˙+ ṙ)′ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ ṫ ˙+ ṙ′ =^{p}
(ṙ ˙+ ṫ)′ ;
L07: Taut2 ⊳ L04 ⊳ L06 ≫ H ˙⇒ ṫ ˙+ ṙ′ =^{p} (ṙ ˙+ ṫ)′ ;

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

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

L09: Taut2 ⊳ L07 ⊳ L08 ≫

H ˙⇒ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒
ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ  ;
L10: Taut4 ⊳ L02 ⊳ L09 ≫  H ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ  ;
L11: Gen′ ⊳ L10 ≫  ˙∀ṙ: (H ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ)  ;

L12: L3.2(h)′basis ≫ ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ) ˙⇒ ˙∀ṙ: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ;

L13: MP′ ⊳ L12 ⊳ L11 ≫  ˙∀ṙ: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ  ;
L14: Gen′ ⊳ L13 ≫  ˙∀ṫ: ˙∀ṙ: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ  □

5 Konklusion

Det er lykkedes at bevise den kommutative lov for addition formelt i systemet Logiweb, der både kan verificere beviser i logiske systemer, og samtidigt kan præsentere disse på en pæn måde for læseren. Brug af konkrete variabler gjorde flere af beviserne overraskende komplekse, men ellers var Logiweb et fornuftigt system at udarbejde beviser i.

A Definitioner

A.1 Denne sides navn

Denne rapport er også en Logiweb-side, og skal derfor have et navn. Dette defineres til:

[peanorapport =^{pyk} “peanorapport”]

A.2 Variabler i Peano-aritmetik

Følgende kan være konkrete variabler i Peano-aritmetik [ȧ]^{58}, [ḃ]^{59}, [ċ]^{60}, [ḋ]^{61}, [ė]^{62}, [ḟ]^{63}, [ġ]^{64}, [ḣ]^{65}, [i̇]^{66}, [j̇]^{67}, [k̇]^{68}, [l̇]^{69}, [ṁ]^{70}, [ṅ]^{71}, [ȯ]^{72}, [ṗ]^{73}, [q̇]^{74},

58[ȧ =^{pyk} “peano a”] 59[ḃ =^{pyk} “peano b”] 60[ċ =^{pyk} “peano c”] 61[ḋ =^{pyk} “peano d”] 62[ė =^{pyk} “peano e”] 63[ḟ =^{pyk} “peano f”] 64[ġ =^{pyk} “peano g”] 65[ḣ =^{pyk} “peano h”] 66[i̇ =^{pyk} “peano i”] 67[j̇ =^{pyk} “peano j”] 68[k̇ =^{pyk} “peano k”] 69[l̇ =^{pyk} “peano l”] 70[ṁ =^{pyk} “peano m”] 71[ṅ =^{pyk} “peano n”] 72[ȯ =^{pyk} “peano o”] 73[ṗ =^{pyk} “peano p”] 74[q̇ =^{pyk} “peano q”]

[ṙ]^{75}, [ṡ]^{76}, [ṫ]^{77}, [u̇]^{78}, [v̇]^{79}, [ẇ]^{80}, [ẋ]^{81}, [ẏ]^{82}, and [ż]^{83}.

Disse variabler makrodefineres som [ȧ ¨= ȧ], [ḃ ¨= ḃ], [ċ ¨= ċ], [ḋ ¨= ḋ], [ė ¨= ė], [ḟ ¨= ḟ], [ġ ¨= ġ], [ḣ ¨= ḣ], [i̇ ¨= i̇], [j̇ ¨= j̇], [k̇ ¨= k̇], [l̇ ¨= l̇], [ṁ ¨= ṁ], [ṅ ¨= ṅ], [ȯ ¨= ȯ], [ṗ ¨= ṗ], [q̇ ¨= q̇], [ṙ ¨= ṙ], [ṡ ¨= ṡ], [ṫ ¨= ṫ], [u̇ ¨= u̇], [v̇ ¨= v̇], [ẇ ¨= ẇ], [ẋ ¨= ẋ], [ẏ ¨= ẏ], og [ż ¨= ż].

B Litteraturliste

[1] Formelt bevis for den kommutative lov for addition i peano-aritmetik.

   http://www.diku.dk/~grue/logiweb/20050502/home/hyldahl/
   peanorapport/fixed/.
[2] Logiweb. http://yoa.dk.
[3] Logiweb base page. http://www.diku.dk/~grue/logiweb/20050502/
   home/grue/base/latest/.
[4] Peano.  http://www.diku.dk/~grue/logiweb/20050502/home/grue/
   peano/latest/.

[5] E. Mendelson. Introduction to Mathematical Logic, fourth edition. Chapman & Hall, 1997.

75[ṙ =^{pyk} “peano r”]

76[ṡ =^{pyk} “peano s”]

77[ṫ =^{pyk} “peano t”]

78[u̇ =^{pyk} “peano u”]

79[v̇ =^{pyk} “peano v”]

80[ẇ =^{pyk} “peano w”]

81[ẋ =^{pyk} “peano x”]

82[ẏ =^{pyk} “peano y”]

83[ż =^{pyk} “peano z”]