Et bevis i Peano aritmetik

Frederik Eriksen (eriksen@diku.dk)

29. juni 2005

Indhold

1 Indledning 3

2 Lidt om Logiweb 3 2.1 Formelle konstruktioner . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Særlige definitioner . . . . . . . . . . . . . . . . . . . . . . . . . . 4

3 Peano aritmetik 4

3.1 Syntaks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.1.1 Termer . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.1.2 Formler . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3.2 Aksiomatisk system . . . . . . . . . . . . . . . . . . . . . . . . . 5

4 Lemmaer, afledte lemmaer og makroer 7 4.1 Lemmaer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 4.2 Afledte lemmaer . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

4.2.1 Regellemmaer . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.2.2 Betingede regellemmaer . . . . . . . . . . . . . . . . . . . 9 4.2.3 Navneafledte lemmaer . . . . . . . . . . . . . . . . . . . . 10

4.3 Makroer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

5 Beviser for makroerne 13 5.1 Bevis for Weakening . . . . . . . . . . . . . . . . . . . . . . . . . 13 5.2 Bevis for DoubleMP′ . . . . . . . . . . . . . . . . . . . . . . . . . 14 5.3 Bevis for ConditionedMP′ . . . . . . . . . . . . . . . . . . . . . 15 5.4 Bevis for DoubleConditionedMP′ . . . . . . . . . . . . . . . . . . 15 5.5 Bevis for ImplyTransitivity . . . . . . . . . . . . . . . . . . . . . 16 5.6 Bevis for PermuteAntecedents . . . . . . . . . . . . . . . . . . . 17 5.7 Bevis for AddOne . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 5.8 Bevis for SubstitutionMacro . . . . . . . . . . . . . . . . . . . . . 18 5.9 Bevis for InductionMacro . . . . . . . . . . . . . . . . . . . . . . 19

6 Beviser for lemmaerne 20 6.1 Bevis for EqualReflexivity . . . . . . . . . . . . . . . . . . . . . . 22 6.2 Bevis for EqualSymmetry og heraf afledt lemma . . . . . . . . . 22 6.3 Bevis for EqualTransitivity og heraf afledte lemmaer . . . . . . . 23 6.4 Bevis for Mendelson3.2(d) og heraf afledte lemmaer . . . . . . . . 25 6.5 Bevis for Mendelson3.2(f) . . . . . . . . . . . . . . . . . . . . . . 26 6.6 Bevis for Mendelson3.2(g) og heraf afledt lemma . . . . . . . . . 28 6.7 Bevis for PlusCommutativity . . . . . . . . . . . . . . . . . . . . 30

A Navnet på dette dokument 32

B TEX definitioner 32

C Litteratur 33

Figurer

1 Den overordnede struktur af beviset for PlusCommutativity … 20

Tabeller

1 Makroer der beviser makroer . . . . . . . . . . . . . . . . . . . . 13 2 Makroer der beviser lemmaer . . . . . . . . . . . . . . . . . . . . 21

1 Indledning

Her er en matematisk sætning: Ligheden

n + m = m + n  (1)

gælder for alle naturlige tal n og m. (Ved et “naturligt tal” forstår jeg et ikkenegativt heltal).

Denne rapport indeholder et formelt bevis for sætning (1). Beviset gennemføres inden for rammerne af et formelt system kaldet “Peano aritmetik”. Rapporten er udarbejdet ved hjælp af Logiweb, som er et system til verifikation og publikation af tekster, der indeholder formel matematik. Logiweb har vericeret, at rapportens bevis for sætning (1) er korrekt — så jeg kan tillade mig at påstå, at rapporten ikke indeholder nogen formelle fejl. Jeg har også brugt Logiweb til at publicere rapporten på internettet; adressen er:

http://www.diku.dk/~grue/logiweb/20050502/home/eriksen/peano-commutativity.

Rapportens bevis for (1) findes allerede i litteraturen — se [3], sætning 3.2(h). Det er altså mere rimeligt at betragte rapporten som en formel øvelse i at bruge Logiweb, end som et selvstændigt stykke matematisk arbejde; men formelle øvelser har jo også deres berettigelse.

Rapporten er struktueret som følger: Afsnit 2 handler om Logiweb. Det er ikke en detaljeret beskrivelse af systemet, men giver forhåbentlig oplysninger nok til, at man kan forstå rapportens formelle indhold uden yderligere viden om Logiweb. Afsnit 3 beskriver syntaksen for Peano aritmetik samt det aksiomsystem, der bliver brugt i rapporten. Afsnit 4 præsenterer de 28 hjælpesætninger, som jeg vil bruge til at bevise ligning (1). For overskuelighedens skyld har jeg inddelt hjælpesætningerne i 3 undergrupper: Lemmaer, afledte lemmaer og makroer. Makroerne bliver bevist i afsnit 5; og de resterende hjælpesætninger bliver bevist i afsnit 6.

2 Lidt om Logiweb

Som nævnt i indledningen er denne rapport skrevet ved hjælp af Logiweb. Dette betyder dels, at rapportens formelle indhold er defineret ud fra nogle andre Logiweb-dokumenter, og dels at rapporten har nogle stilistiske særtræk. Disse to facetter ved Logiweb vil jeg kort forklare i afsnit 2.1 og 2.2. For en detaljeret beskrivelse af hele Logiweb systemet vil jeg henvise til [1]; her kan man bla. læse om den bevischecker, der har verificeret rapportens beviser.

2.1 Formelle konstruktioner

Det formelle indhold af et Logiweb-dokument er sammensat af en række formelle konstruktioner. En formel konstruktion kan repræsentere alt, hvad der har med formel matematik at gøre: Variable, funktioner, lemmaer, beviser, osv. Der er to kilder til konstruktionerne i et Logiweb-dokument: Dels kan man indføre sine egne konstruktioner, og dels kan man importere konstruktioner fra andre Logiiweb-dokumenter. I denne rapport er alle konstruktioner importerede fra de to Logiweb-dokumenter [1] og [2] — med undtagelse af de konstruktioner, der repræsenterer rapportens 28 hjælpesætninger; dem definerer jeg selv.

2.2 Særlige definitioner

Den formelle del af et Logiweb-dokument skrives i et formateringssprog ved navn “pyk”. Hver formel konstruktion, man arbejder med i dokumentet, har tilknyttet en såkaldt “pyk definition”. Dette er en angivelse af, hvad man skal skrive, hvis man i et andet Logiweb-dokument ønsker at benytte den pågældende konstruktion. Hvis man indfører en ny konstruktion i sit Logiweb-dokument, er det et krav, at man gør den tilsvarende pyk definition tilgængelig i dokumentet. Dette krav vil jeg imødekomme ved at nævne pyk definitionen i en fodnote, hver gang jeg præsenterer en ny hjælpesætning.

Logiweb genererer det færdige dokument ved hjælp af det kendte formateringssprog L^{A}TEX. Derfor har hver formel konstruktion også tilknyttet en såkaldt “TEX definition”, som angiver, hvordan konstruktionen skal skrives i L^{A}TEX. Ligesom pyk definitioner skal også TEX definitioner være tilgængelige i dokumentet. TEX definitionerne for denne rapports lemmaer er vedlagt i bilag B.

Endelig skal det nævnes, at Logiweb opfatter selve navnet på et Logiwebdokument som en formel konstruktion. Derfor skal ethvert Logiweb-dokument indeholde mindst én pyk definition — nemlig pyk definitionen af dokumentets eget navn. Denne definition har jeg vedlagt i bilag A.

3 Peano aritmetik

Peano aritmetik er et formelt sprog, der bruges til at repræsentere de naturlige tal. Jeg vil bruge nøjagtig den samme version af Peano aritmetik som dén, der præsenteres i [2]. Dette gælder både mht. syntaksen (som jeg gennemgår i afsnit 3.1), og mht. det anvendte aksiomsystem (som jeg gennemgår i afsnit 3.2).

3.1 Syntaks

Peano aritmetik er opbygget af termer og formler; jeg gennemgår hver af disse begreber i de følgende to underafsnit.

3.1.1 Termer

Syntaksen for en term T kan beskrives ved den følgende BNF-grammatik:

T ::= ˙0 | T′ | T ˙+ T | T ˙· T | Pvar  (2)

Efterfølgeren m til et naturligt tal n er det mindste naturlige tal, der er større end n. Efterfølgeroperatoren er den funktion, der fører n over i m. Ideen med den syntaktiske konstruktion′ er, at den skal repræsentere efterfølgeroperatoren.

På denne måde kan vi repræsentere alle naturlige tal med de to konstruktioner ˙0 og ′ — 1 kan repræsenteres som ˙0′, 2 som (˙0′)′, ^{1} osv.

Ideen med konstruktionerne ˙+ og ˙· er, at de skal repræsentere regningsarterne addition og multiplikation. Da denne rapport kun omhandler addition, kommer vi ikke til at se mere til tegnet ˙·.

Den sidste konstruktion i (2) er Pvar, som er en forkortelse for “Peano variabel” . En Peano variabel er en variabel, der varierer over konstante termer (hvor en konstant term er en term, der ikke indeholder Peano variable). Artiklen [2] bruger små bogstaver med en prik over til at benævne Peano variable — altså f.eks. ȧ og ḃ. Jeg vil gøre det samme, idet jeg dog kun vil bruge bogstaverne ṫ, ṙ og ṡ.

3.1.2 Formler

Syntaksen for en formel F kan beskrives ved den følgende BNF-grammatik:

F ::= T =^{p} T | ˙¬F | F ˙⇒ F | ˙∀Pvar : F

Med en formel kan vi altså påstå, at to termer er lig hinanden. Herudover kan vi negere formler, sætte formler sammen med implikationstegnet ˙⇒ samt sætte alkvantoren ˙∀ foran formler. Bemærk at ˙⇒ er højreassociativ; et udtryk som f.eks. ṙ ˙⇒ ṡ ˙⇒ ṫ skal læses som ṙ ˙⇒ (ṡ ˙⇒ ṫ).

3.2 Aksiomatisk system

Beviserne i denne rapport baserer sig på det aksiomatiske system S′ fra [2]. Dette system består af 14 aksiomskemaer (kaldet A1′— A5′ og S1′—S9′) og 2 slutningsregler (kaldet MP′ og Gen′). For overblikkets skyld genoptrykker jeg dem her:

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

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

[S′ rule A3′: ( ˙¬ 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]

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

1Egentlig bør (˙0′)′ skrives ˙0′′. Imidlertid er der en lille fejl ved TEX definitionen af konstruktionen ′ i [2]. Fejlen betyder, at L^{A}TEX ikke accepterer to anvendelser af ′ i træk — derfor den ekstra parentes.

[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]

For at lette forståelsen af S′ vil jeg slutte dette afsnit med en generel beskrivelse af de to komponenter, som S′ består af: Aksiomskemaer og slutningsregler.

Et aksiom er en formel, som vi kan tage for givet. Et aksiomskema repræsenterer en mængde af aksiomer. F.eks. følger det af aksiom A1′, at formler som ṙ ˙⇒ ṫ ˙⇒ ṙ og ṡ ˙⇒ ˙0 =^{p} ˙0′ ˙⇒ ṡ er aksiomer. Variablene A og B i A1′ kaldes for meta-variable. Meta-variable er ikke en del af Peano aritmetik; de bruges i stedet, når vi taler om Peano aritmetik — hvilket vi jo gør i vores aksiomsystem. (Der er en tilsvarende forskel mellem den alkvantor ˙∀, som vi bruger i Peano aritmetik, og den alkvantor ∀, som vi bruger i S′). Meta-variable kan variere over Peano variable, vilkårlige termer eller formler. I S′ bruges “X ” om den første slags meta-variable, mens “A”, “B” og “C” bruges om de to andre slags meta-variable.

Ud over aksiomskemaerne indeholder S′ som nævnt to slutningsregler. En slutningsregel er en regel for, hvordan vi kan vise formler ud fra andre formler, som allerede er bevist. F.eks. siger MP′, at vi kan vise formlen B, hvis vi i forvejen har vist de to formler A ˙⇒ B og A. Slutningsreglerne definerer således en beviselighedsrelation ⊢ mellem formler.

Tilsammen definerer aksiomskemaerne og slutningsreglerne en mængde af beviselige formler: En beviselig formel er enten et aksiom, eller også kan den bevises ud fra aksiomerne ved hjælp af slutningsreglerne. Jeg vil bruge ordet “systemsætning” som en fællesbetegnelse for aksiomskemaer og slutningsregler.

En systemsætning kan indeholde en eller flere sidebetingelser; dette gælder for tre af aksiomskemaerne i system S′ (A4′, A5′ og S9′). En sidebetingelse i en systemsætning definerer et krav til den korrekte anvendelse af systemsætningen. I S9′ er det f.eks. klart, at implikationen [B ˙⇒ ˙∀X: (A ˙⇒ C) ˙⇒ ˙∀X: A] ikke har generel gyldighed: B skal være et basistilfælde, og formlen A ˙⇒ C skal repræsentere det induktive skridt. Disse ekstra krav er formuleret i de to sidebetingelser i S9′. Rent syntaktisk bruger vi tegnet “⊧” til at adskille en sidebetingelse fra den øvrige del af systemsætningen.

4 Lemmaer, afledte lemmaer og makroer

Som nævnt i indledningen har jeg opdelt beviset for (1) i 28 hjælpesætninger. For overskuelighedens skyld har jeg inddelt disse hjælpesætninger i tre grupper: Lemmaer, afledte lemmaer og makroer. Distinktionen mellem disse grupper er ikke knivskarp, men den gør det lettere at forklare bevisets struktur. I dette afsnit vil jeg gennemgå hver gruppe og præsentere de hjælpesætninger, som grupperne indeholder.

I min definition af de forskellige hjælpesætninger vil jeg bruge de følgende konventioner for variabelnavne:

• Meta-variable, der varierer over formler, betegnes med “A”, “B”, “C”, “D”, “E” og “F”.

• Meta-variable, der varierer over vilkårlige termer, betegnes med “T ”, “R”, “S” og “U”.

• Meta-variable, der varierer over Peano variable, betegnes med “Z”.

• Peano variable betegnes med “ṫ”, “ṙ” og “ṡ”(som allerede nævnt i afsnit 3.1.1).

4.1 Lemmaer

Under kategorien “lemmaer” vil jeg for det første rubricere hovedsætningen (1), formuleret i Peano aritmetik:

[S′ lemma PlusCommutativity: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ] ^{2}

Som det kan ses, benytter PlusCommutativity sig ikke af meta-variable (som f.eks. T og R), men derimod af Peano variablene ṫ og ṙ. Der er en teknisk forklaring herpå: PlusCommutativity skal vises ved induktion, og derfor kommer aksiomskemaet S9′ uundgåeligt til at indgå i beviset. Som nævnt i afsnit 3.2 benytter S9′ sig af sidebetingelser; og Logiwebs bevischecker kan (endnu) ikke evaluere sidebetingelser, der indeholder meta-variable.

I afsnit 3.1 i lærebogen [3] beviser Mendelson PlusCommutativity under navnet “sætning 3.2(h)”. For at nå frem til sætning 3.2(h) viser Mendelson først de følgende seks lemmaer: ^{3}

[S′ lemma EqualReflexivity: ∀T : T =^{p} T ] ^{4}

[S′ lemma EqualSymmetry: ∀T : ∀R: T =^{p} R ˙⇒ R =^{p} T ] ^{5} [S′ lemma EqualTransitivity: ∀T : ∀R: ∀S: T =^{p} R ˙⇒ R =^{p} S ˙⇒ T =^{p} S] ^{6}

2[PlusCommutativity =^{pyk} “plus commutativity”]. Dette er en “pyk definition”, som omtalt i afsnit 2.2.

3Det skal lige nævnes, at Mendelson bruger meta-variable i sin formulering af Mendelson3.2(f) og Mendelson3.2(g). Fordi disse lemmaer skal vises ved induktion, bruger jeg Peano variable i stedet for.

4[EqualReflexivity =^{pyk} “equal reflexivity”]

5[EqualSymmetry =^{pyk} “equal symmetry”]

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

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

Lemmaerne EqualReflexivity, EqualSymmetry og EqualTransitivity udsiger tilsammen, at =^{p} er en ækvivalensrelation — altså en relation, som er refleksiv, symmetrisk og transitiv. Indholdet af de tre lemmaer Mendelson3.2(d), Mendelson3.2(f) og Mendelson3.2(g) kan ikke sammenfattes lige så koncist, så jeg har givet dem de samme navne, som de har i [3].

Ligesom PlusCommutativity skal Mendelson3.2(f) og Mendelson3.2(g) bevises ved induktion. For at begrænse længden af de enkelte beviser har jeg valgt at definere basistilfældene og de induktive skridt som selvstændige lemmaer. På denne måde får vi yderligere seks lemmaer:

[S′ lemma Mendelson3.2(f)Base: ˙0 =^{p} ˙0 ˙+ ˙0] ^{10}

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

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

[S′ lemma Mendelson3.2(g)Indu: ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′ ˙⇒ ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′] ^{13}

[S′ lemma PlusCommutativityBase: ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ] ^{14}

[S′ lemma PlusCommutativityIndu: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ] ^{15}

Bemærk at induktionen i Mendelson3.2(g) og PlusCommutativity forløber efter variablen ṙ (og ikke efter ṫ).

Flere lemmaer er der ikke i denne rapport; en optælling viser, at der i alt er 13 lemmaer.

6[EqualTransitivity =^{pyk} “equal transitivity”]

7[Mendelson3.2(d) =^{pyk} “mendelson three two d”]

8[Mendelson3.2(f) =^{pyk} “mendelson three two f”]

9[Mendelson3.2(g) =^{pyk} “mendelson three two g”]

10[Mendelson3.2(f)Base =^{pyk} “mendelson three two f base”]

11[Mendelson3.2(f)Indu =^{pyk} “mendelson three two f induction”]

12[Mendelson3.2(g)Base =^{pyk} “mendelson three two g base”]

13[Mendelson3.2(g)Indu =^{pyk} “mendelson three two g induction”]

14[PlusCommutativityBase =^{pyk} “plus commutativity base”]

15[PlusCommutativityIndu =^{pyk} “plus commutativity induction”]

4.2 Afledte lemmaer

Som navnet antyder, er de afledte lemmaer afledt fra de lemmaer, som jeg præsenterede i afsnit 4.1. ^{16} Jeg vil i alt definere 6 afledte lemmaer. De kan opdeles i tre undergrupper: Regellemmaer, betingede regellemmaer og navneafledte lemmaer.

4.2.1 Regellemmaer

Som vi senere vil se i afsnit 5.3, kan vi altid bevise

A ⊢ B, hvis vi i forvejen har et bevis for:

A ˙⇒ B. Ved et “regellemma” forstår jeg et lemma af formen A ⊢ B, som er afledt fra et lemma af formen A ˙⇒ B. Når et lemma skal anvendes i beviser, er det som regel lettere at arbejde med regellemmaet end med det tilsvarende moderlemma. Det gælder også for de tre lemmaer EqualSymmetry, EqualTransitivity og Mendelson3.2(d) fra afsnit 4.1. Derfor vil jeg bevise de tilsvarende tre regellemmaer:

[S′ lemma Mendelson3.2(d)Rule:

∀T : ∀R: ∀S: T =^{p} R ⊢ S =^{p} R ⊢ T =^{p} S] ^{17}

[S′ lemma EqualTransitivityRule:

∀T : ∀R: ∀S: T =^{p} R ⊢ R =^{p} S ⊢ T =^{p} S] ^{18}

[S′ lemma EqualSymmetryRule: ∀T : ∀R: T =^{p} R ⊢ R =^{p} T ] ^{19}

Jeg kunne også have bevist regellemmaer svarende til Mendelson3.2(f)Indu, Mendelson3.2(g)Indu og PlusCommutativityIndu. Imidlertid har jeg valgt kun at bevise de tre regellemmaer, som kan bruges i beviset for PlusCommutativity. Regellemmaer har ikke megen værdi i sig selv; de er et middel til at gøre beviser kortere og mere overskuelige.

4.2.2 Betingede regellemmaer

Et yderligere raffinement er at gå fra regellemmaets form:

A ⊢ B til den betingede form:

C ˙⇒ A ⊢ C ˙⇒ B Ved et “betinget regellemma” forstår jeg et afledt lemma, der har denne form. Jeg vil bevise de følgende to betingede regellemmaer:

16Jeg vil bruge ordet “moderlemma” om et lemma, ud fra hvilket man kan aflede andre lemmaer.

17[Mendelson3.2(d)Rule =^{pyk} “mendelson three two d rule”]

18[EqualTransitivityRule =^{pyk} “equal transitivity rule”]

19[EqualSymmetryRule =^{pyk} “equal symmetry rule”]

[S′ lemma EqualTransitivityCondRule:

∀A: ∀T : ∀R: ∀S: A ˙⇒ T =^{p} R ⊢ A ˙⇒ R =^{p} S ⊢ A ˙⇒ T =^{p} S] ^{20}

[S′ lemma Mendelson3.2(d)CondRule:

∀A: ∀T : ∀R: ∀S: A ˙⇒ T =^{p} R ⊢ A ˙⇒ S =^{p} R ⊢ A ˙⇒ T =^{p} S] ^{21}

Jeg beviser netop disse to betingede regellemmaer, fordi de kan bruges i beviset for PlusCommutativity. Ligesom i afsnit 4.2.1 gælder det, at der ikke er nogen selvstændig grund til at bevise betingede regellemmaer.

4.2.3 Navneafledte lemmaer

Den sidste kategori af afledte lemmaer indeholder kun et enkelt lemma. Det er defineret som følger:

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

Som man kan se, er dette lemma helt identisk med lemma Mendelson3.2(g) fra afsnit 4.1 — bortset fra at der er byttet om på de to Peano variable ṙ og ṫ. Derfor kalder jeg Mendelson3.2(g)Switch for et “navneafledt lemma”. Det viser sig, at det er denne form af Mendelson3.2(g), som vi får brug for, når vi skal vise PlusCommutativity. Dette er et eksempel på ulempen ved at arbejde med Peano variable frem for meta-variable: Vi kan ikke abstrahere fra variablenes navne. Man kunne naturligvis løse problemet ved at bevise den brugbare form til at begynde med. Jeg har valgt løsningen med Mendelson3.2(g)Switch for at se, hvor meget ekstra arbejde det kræver at ændre variabelnavnene i et tilfælde som dette.

4.3 Makroer

Ved en makro forstår jeg en generel hjælpesætning, der kan bruges i beviset for mange forskellige slags sætninger. I denne rapport er der i alt 9 makroer. Jeg har alene defineret og bevist disse makroer for at bruge dem i beviset for PlusCommutativity; alligevel er de fleste af makroerne generelle nok til, at man også kan bruge dem i andre sammenhænge.

I det følgende vil jeg for hver enkelt makro præsentere den formelle definition og forklare makroens indhold.

[S′ lemma Weakening: ∀A: ∀B: A ⊢ B ˙⇒ A] ^{23}

Denne makro tillader os at gøre formler betingede. Hvis vi har vist, at formel A gælder ubetinget, så må vi også gerne antage, at A gælder under betingelsen B.

20[EqualTransitivityCondRule =^{pyk} “equal transitivity conditioned rule”]

21[Mendelson3.2(d)CondRule =^{pyk} “mendelson three two d conditioned rule”]

22[Mendelson3.2(g)Switch =^{pyk} “mendelson three two g rt switch”]

23[Weakening =^{pyk} “weakening”]. Bemærk at Logiweb kalder alle hjælpesætninger for for “lemmaer” — også dem, som jeg kalder for “makroer”.

[S′ lemma DoubleMP′: ∀C: ∀D: ∀E: C ˙⇒ D ˙⇒ E ⊢ C ⊢ D ⊢ E] ^{24}

Makroen DoubleMP′ kan spare os for en enkelt bevislinie i de tilfælde, hvor man ellers ville bruge slutningsreglen MP′ to gange i træk.

[S′ lemma ConditionedMP′:

∀A: ∀B: ∀C: A ˙⇒ B ˙⇒ C ⊢ A ˙⇒ B ⊢ A ˙⇒ C] ^{25}

Indholdet af slutningsreglen MP′ er som bekendt, at man kan slutte C ud fra B ˙⇒ C og B. Man kan tænke på makroen ConditionedMP′ som en betinget udgave af MP′: Den siger, at vi har lov til at bruge MP′ under en vilkårlig betingelse A, hvis vi tilføjer A til begge præmisser og til konklusionen.

[S′ lemma DoubleConditionedMP′:

∀A: ∀D: ∀E: ∀F: A ˙⇒ D ˙⇒ E ˙⇒ F ⊢ A ˙⇒ D ⊢ A ˙⇒ E ⊢ A ˙⇒ F] ^{26}

Af og til kan man få brug for at benytte makroen ConditionedMP′ to gange i træk. Her kan DoubleConditionedMP′ spare en bevislinie. Denne makro forholder sig altså til ConditionedMP′ på nøjagtigt samme måde, som DoubleMP′ forholder sig til MP′.

[S′ lemma ImplyTransitivity: ∀D: ∀E: ∀F: D ˙⇒ E ⊢ E ˙⇒ F ⊢ D ˙⇒ F] ^{27}

Som navnet antyder, udsiger ImplyTransitivity, at relationen ˙⇒ er transitiv; ud fra D ˙⇒ E og E ˙⇒ F kan vi slutte D ˙⇒ F.

[S′ lemma PermuteAntecedents:

∀D: ∀E: ∀F: D ˙⇒ E ˙⇒ F ⊢ E ˙⇒ D ˙⇒ F] ^{28}

I en term som D ˙⇒ E ˙⇒ F kaldes D og E for antecedenterne, mens F kaldes for konsekvensen. Indholdet af PermuteAntecedents er, at antecedenternes rækkefølge er ligegyldig; vi kan omskrive D ˙⇒ E ˙⇒ F til E ˙⇒ D ˙⇒ F.

[S′ lemma AddOne: ∀T : ∀R: T =^{p} R ⊢ T′ =^{p} R′] ^{29}

Denne makro er afledt fra aksiomskemaet S2′: Hvis S2′ havde været et lemma, ville jeg have rubriceret AddOne som et regellemma (med S2′ som moderlemma).

24[DoubleMP′ =^{pyk} “double mp prime”]

25[ConditionedMP′ =^{pyk} “conditioned mp prime”]

26[DoubleConditionedMP′ =^{pyk} “double conditioned mp prime”]

27[ImplyTransitivity =^{pyk} “imply transitivity”]

28[PermuteAntecedents =^{pyk} “permute antecedents”]

29[AddOne =^{pyk} “add one”]

[S′ lemma SubstitutionMacro:

∀Z: ∀C: ∀A: ∀D: ⌈A⌉≡⟨⌈D⌉|⌈Z⌉ := ⌈C⌉⟩ ⊢⊢ D ⊢ A] ^{30}

Denne makro siger, at vi kan slutte A ud fra D, hvis vi kan frembringe A ud fra D ved hjælp af en substitution. F.eks. kan vi slutte ˙0 =^{p} ˙0 ud fra ṫ =^{p} ṫ, fordi vi kan få ˙0 =^{p} ˙0 frem ved at erstatte ṫ med ˙0 i ṫ =^{p} ṫ.

[S′ lemma InductionMacro: ∀A: ∀B: ∀C: ∀Z:

⌈A⌉≡⟨⌈A⌉|⌈Z⌉ := ⌈Z⌉⟩ ⊢⊢ B≡⟨A|Z := ˙0⟩ ⊢⊢ C≡⟨A|Z := Z′⟩ ⊢⊢ B ⊢ A ˙⇒ C ⊢ A] ^{31}

I et induktionsbevis ligger det meste af arbejdet som regel i at vise basistilfældet og det induktive skridt. Når dette er gjort, mangler man bare at henvise til princippet om matematisk induktion. Dette arbejde er indkapslet i InductionMacro. Med denne makro kan man færdiggøre et induktionsbevis med en enkelt linie, når man først har vist basistilfældet B og det induktive skridt A ˙⇒ C.

Bemærk iøvrigt den lidt pudsige sidebetingelse ⌈A⌉≡⟨⌈A⌉|⌈Z⌉ := ⌈Z⌉⟩, der siger, at A er lig med A, hvis vi erstatter enhver fri forekomst af Peano variablen Z i A med sig selv. Det er klart, at dette er opfyldt for enhver formel A og enhver Peano variabel Z, så ved første øjekast virker det som en overflødig sidebetingelse. Det er imidlertid nødvendigt eksplicit at fortælle Logiweb, at betingelsen er opfyldt, hvis beviset for InductionMacro skal gå igennem. Dette skyldes, at Logiweb ikke kan evaluere udtryk, der indeholder meta-variable (som allerede omtalt i afsnit 3.2). Ved at formulere meta-udsagnet ⌈A⌉≡⟨⌈A⌉|⌈Z⌉ := ⌈Z⌉⟩ som en sidebetingelse, kan vi bruge det direkte i beviset, uden at Logiweb evaluerer det. ^{32} Når vi skal til at anvende InductionMacro i andre beviser, vil betingelsen altid være opfyldt; så den ekstra sidebetingelse udgør kun et æstetisk problem.

30[SubstitutionMacro =^{pyk} “substitution macro”]

31[InductionMacro =^{pyk} “induction macro”]

32Det omtalte bevis står i afsnit 5.9.

5 Beviser for makroerne

I dette afsnit vil jeg bevise de 9 makroer, som blev præsenteret i afsnit 4.3. Jeg beviser makroerne i den samme rækkefølge, som blev brugt i dette afsnit.

Tre af makroerne er så generelle, at de kan bruges i beviserne for de andre makroer. I tabel 1 kan man se, hvilke makroer der bruges i beviserne for hvilke andre makroer.

Weakening DoubleMP′ ConditionedMP′ DoubleConditionedMP′ ImplyTransitivity PermuteAntecedents AddOne SubstitutionMacro InductionMacro
Weakening  • •
DoubleMP′ • •
ConditionedMP′  • • •

Tabel 1: Makroer der beviser makroer. En “•” i række X , søjle Y betyder, at makro X bliver brugt i beviset for makro Y .

5.1 Bevis for Weakening

Her er beviset for Weakening:

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

S′ proof of Weakening:

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

Da dette er rapportens første bevis, vil jeg bringe nogle ekstra kommentarer. Oven over beviset har jeg gentaget definitionen af det, der skal bevises; dette er kun for overblikkets skyld — det er ikke en formel nødvendighed. Selve beviset for Weakening består af fem linier, nummereret fra 1 til 5. En bevislinie kan have to former. Den første form er:

     Argumentation ≫ Konklusion

hvor Konklusion er det som linien beviser, mens teksten i Argumentation udgør en begrundelse for, at Konklusion gælder. F.eks. siger linie 4, at meta-formlen A ˙⇒ B ˙⇒ A gælder, fordi den kan udledes fra aksiomskemaet A1′ ved substitution. I linie 5 skal argumentationen læses på den måde, at konklusionerne fra linie 4 og 3 bliver brugt som præmisser til slutningsreglen MP′. Den generelle betydning af konstruktionen “x ⊳ y” er, at konklusionen fra y bliver brugt som præmis i forhold til x.

Den anden form, en bevislinie kan have, er:

     Nøgleord ≫ Konklusion

hvor Nøgleord er et af de tre ord “Arbitrary”, “Premise” eller “Side-condition”. Betydningen af ordene “Premise” og “Side-condition” er åbenlys: De angiver, at liniens konklusion indgår som en præmis (hhv. sidebetingelse) i den hjælpesætning, der skal bevises. F.eks. siger bevisets linie 3, at Weakening bruger meta-formlen A som præmis. Når ordet “Arbitrary” bruges, består konklusionen af en meta-variabel (f.eks. A i linie 1 og B i line 2). Meningen med “Arbitrary” er af teknisk karakter: Ideen er at udtrykke, at vi ikke antager noget om den pågældende meta-variabel, og at vi derfor har ret til at binde meta-variablen med en alkvantor i den hjælpesætning, der skal bevises. I det forhåndenværende bevis fungerer de to linier med “Arbitrary” altså som berettigelse for, at Weakening er kvantificeret med “∀A: ∀B:”.

Alt dette har drejet sig om den formelle syntaks for et Logiweb bevis. Der er egentlig ikke så meget at sige om selve beviset for Weakening; det er en ganske enkel anvendelse af A1′ og MP′.

5.2 Bevis for DoubleMP′

[S′ lemma DoubleMP′: ∀C: ∀D: ∀E: C ˙⇒ D ˙⇒ E ⊢ C ⊢ D ⊢ E]

S′ proof of DoubleMP′:

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

Som nævnt i afsnit 4.3 er ideen med DoubleMP′ at indkapsle to anvendelser af MP′ i en enkelt bevislinie. Det er derfor ganske naturligt, at kernen i beviset for DoubleMP′ netop består af to anvendelser af MP′.

5.3 Bevis for ConditionedMP′

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

S′ proof of ConditionedMP′:

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

I afsnit 4.3 nævnte jeg, at ConditionedMP′ kunne opfattes som en betinget udgave af MP′. Vi kan også opfatte ConditionedMP′ som et regellemma i forhold til aksiomskemaet A2′: A2′ har formen A ˙⇒ B ˙⇒ C, mens ConditionedMP′ har formen A ⊢ B ⊢ C. Dermed kan vi bruge en meget enkel teknik til at bevise ConditionedMP′: Først opskriver vi præmisserne og moderlemmaet, og så bruger vi MP′ én gang for hver præmis. (I dette tilfælde er “moderlemmaet” et aksiomskema, men det gør ingen forskel). Jeg vil også bruge denne teknik, når vi senere hen skal bevise de egentlige regellemmaer.

5.4 Bevis for DoubleConditionedMP′

[S′ lemma DoubleConditionedMP′:

∀A: ∀D: ∀E: ∀F: A ˙⇒ D ˙⇒ E ˙⇒ F ⊢ A ˙⇒ D ⊢ A ˙⇒ E ⊢ A ˙⇒ F]

S′ proof of DoubleConditionedMP′:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  D  ;
L03: Arbitrary ≫  E  ;
L04: Arbitrary ≫  F  ;
L05: Premise ≫  A ˙⇒ D ˙⇒ E ˙⇒ F  ;
L06: Premise ≫  A ˙⇒ D  ;
L07: Premise ≫  A ˙⇒ E  ;
L08: ConditionedMP′⊳L05⊳L06 ≫ A ˙⇒ E ˙⇒ F  ;
L09: ConditionedMP′⊳L08⊳L07 ≫ A ˙⇒ F  □

Makroen DoubleConditionedMP′ indkapsler to anvendelser af ConditionedMP′, så beviset er enkelt: Vi anvender ConditionedMP′ to gange.

5.5 Bevis for ImplyTransitivity

[S′ lemma ImplyTransitivity: ∀D: ∀E: ∀F: D ˙⇒ E ⊢ E ˙⇒ F ⊢ D ˙⇒ F]

S′ proof of ImplyTransitivity:

L01: Arbitrary ≫  D  ;
L02: Arbitrary ≫  E  ;
L03: Arbitrary ≫  F  ;
L04: Premise ≫  D ˙⇒ E  ;
L05: Premise ≫  E ˙⇒ F  ;
L06: Weakening ⊳ L05 ≫  D ˙⇒ E ˙⇒ F  ;
L07: ConditionedMP′⊳L06⊳L04 ≫ D ˙⇒ F  □

Hidtil har beviserne været så enkle, at det har været let at forklare deres struktur med et par sætninger. Denne fremgangsmåde er ikke holdbar for de mere komplicerede beviser. I disse tilfælde vil jeg i stedet illustrere bevisernes struktur med træer som dette:

[figure: 7:DF; 4:DE; Premise; 5–6:DEF; Premise-W; ^{CondMP′}]

I et “bevistræ” som dette repræsenterer hver knude en eller to af de centrale bevislinier. Bladene svarer til aksiomer eller præmisser, mens bevisets konklusion står i roden. Kanterne er orienteret fra barneknude til forældreknude; betydningen af en kant er, at barneknuden bruges til at bevise forældreknuden. Hver kant er mærket med den systemsætning eller hjælpesætning, der bruges i argumentationen for forældreknuden. ^{33} Bevislinier, der bruger Weakening i argumentationen, er ikke vist som selvstændige knuder; disse bevislinier er i stedet slået sammen med de linier, som Weakening virker på. Der er altså nogle knuder, som svarer til to bevislinier; disse knuder er mærket med endelsen “-W” (som står for “Weakening”).

For at gøre den ovenstående tegning pæn har jeg forkortet navnet “ConditionedMP′” og udeladt tegnet “ ˙⇒” fra de tre knuder. Den slags friheder vil jeg også tage mig ved de kommende bevistræer; og jeg vil kun gøre opmærksom på den ændrede notation, når jeg skønner det nødvendigt.

Så meget om bevistræer. Jeg vil ikke kommentere selve beviset for ImplyTransitivity, men lade bevistræet tale for sig selv. Jeg vil heller ikke kommentere nogen af de andre beviser, der er illustrerede med bevistræer.

33Hvis to kanter fører op til en knude, er kun den ene kant mærket.

5.6 Bevis for PermuteAntecedents

[S′ lemma PermuteAntecedents: ∀D: ∀E: ∀F: D ˙⇒ E ˙⇒ F ⊢ E ˙⇒ D ˙⇒ F]

S′ proof of PermuteAntecedents:

L01: Arbitrary ≫  D  ;
L02: Arbitrary ≫  E  ;
L03: Arbitrary ≫  F  ;
L04: Premise ≫  D ˙⇒ E ˙⇒ F  ;
L05: Weakening ⊳ L04 ≫  E ˙⇒ D ˙⇒ E ˙⇒ F  ;
L06: A2′ ≫  {(D ˙⇒ E ˙⇒ F) ˙⇒ (D ˙⇒ E) ˙⇒ \atop D ˙⇒ F  ;}
L07: Weakening ⊳ L06 ≫  {E ˙⇒ (D ˙⇒ E ˙⇒ F) ˙⇒ \atop (D ˙⇒ E) ˙⇒ D ˙⇒ F  ;}
L08: ConditionedMP′⊳L07⊳L05 ≫ E ˙⇒ (D ˙⇒ E) ˙⇒ D ˙⇒ F  ;
L09: A1′ ≫ E ˙⇒ D ˙⇒ E ;
L10: ConditionedMP′⊳L08⊳L09 ≫ E ˙⇒ D ˙⇒ F  □
[figure: 10:EDF; 8:E(DE)(DF); _{CondMP_{′}}; 6–7:E(DEF)(DE)(DF); A2′-W; _{CondMP_{′}}; 4–5:EDEF; Premise-W; 9:EDE; A1′]

5.7 Bevis for AddOne

[S′ lemma AddOne: ∀T : ∀R: T =^{p} R ⊢ T′ =^{p} R′]

S′ proof of AddOne:

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: Premise ≫  T =^{p} R  ;
L04: S2′ ≫  T =^{p} R ˙⇒ T′ =^{p} R′  ;
L05: MP′ ⊳ L04 ⊳ L03 ≫  T′ =^{p} R′  □

Som nævnt i afsnit 4.3 kan vi opfatte AddOne som et regellemma i forhold til aksiomskemaet S2′. Derfor kan vi vise AddOne med den samme enkle teknik, som vi så første gang i beviset for ConditionedMP′ (afsnit 5.3): Vi skriver præmissen og moderlemmaet op, og vi anvender MP′ én gang for hver præmis (i dette tilfælde kun en enkelt gang).

5.8 Bevis for SubstitutionMacro

[S′ lemma SubstitutionMacro:

∀Z: ∀C: ∀A: ∀D: ⌈A⌉≡⟨⌈D⌉|⌈Z⌉ := ⌈C⌉⟩ ⊢⊢ D ⊢ A]

S′ proof of SubstitutionMacro:

L01: Arbitrary ≫  Z  ;
L02: Arbitrary ≫  C  ;
L03: Arbitrary ≫  A  ;
L04: Arbitrary ≫  D  ;
L05: Side-condition ≫  ⌈A⌉≡⟨⌈D⌉|⌈Z⌉ := ⌈C⌉⟩  ;
L06: Premise ≫  D  ;
L07: Gen′ ⊳ L06 ≫  ˙∀Z: D  ;
L08: A4′ ⊳ ⊳ L05 ≫  ˙∀Z: D ˙⇒ A  ;
L09: MP′ ⊳ L08 ⊳ L07 ≫  A  □

Kernen i dette bevis er linie 8. Konklusionen [ ˙∀Z: D ˙⇒ A] i denne linie udtrykker, at den generelle formel D medfører den mindre generelle formel A. Da vi har antaget D, er det let at konkludere A i linie 9.

I argumentationen i linie 8 benytter vi A4′, der som nævnt i afsnit 3.2 kræver, at en sidebetingelse skal være opfyldt. Derfor bruger vi konstruktionen “x ⊳ ⊳ y”, som markerer, at konklusionen fra y kan bruges som sidebetingelse for x .

5.9 Bevis for InductionMacro

[S′ lemma InductionMacro: ∀A: ∀B: ∀C: ∀Z:

⌈A⌉≡⟨⌈A⌉|⌈Z⌉ := ⌈Z⌉⟩ ⊢⊢ B≡⟨A|Z := ˙0⟩ ⊢⊢ C≡⟨A|Z := Z′⟩ ⊢⊢ B ⊢ A ˙⇒ C ⊢ A]

S′ proof of InductionMacro:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Arbitrary ≫  Z  ;
L05: Side-condition ≫  ⌈A⌉≡⟨⌈A⌉|⌈Z⌉ := ⌈Z⌉⟩  ;
L06: Side-condition ≫  B≡⟨A|Z := ˙0⟩  ;
L07: Side-condition ≫  C≡⟨A|Z := Z′⟩  ;
L08: Premise ≫  B  ;
L09: Premise ≫  A ˙⇒ C  ;
L10: Gen′ ⊳ L09 ≫  ˙∀Z: (A ˙⇒ C)  ;
L11: S9′ ⊳ ⊳ L06 ⊳ ⊳ L07 ≫  B ˙⇒ ˙∀Z: (A ˙⇒ C) ˙⇒ ˙∀Z: A  ;
L12: DoubleMP′⊳L11⊳L08⊳L10 ≫ ˙∀Z: A  ;
L13: A4′ ⊳ ⊳ L05 ≫  ˙∀Z: A ˙⇒ A  ;
L14: MP′ ⊳ L13 ⊳ L12 ≫  A  □

Beviset for InductionMacro er langt, men det er ikke så kompliceret, at jeg vil illustrere det med et bevistræ. Kernen i beviset er de følgende tre blokke:

• Linie 8, der fortæller os, at vi har vist basistilfældet.

• Linie 9–10, der fortæller os, at også det induktive skridt er vist.

• Linie 11, der formulerer princippet om matematisk induktion.

I linie 12 binder vi disse blokke sammen med en DoubleMP′, hvilket giver os konklusionen ∀Z: A. I de sidste to linier fjerner vi Peano alkvantoren herfra, hvorved vi når frem til målet: A.

6 Beviser for lemmaerne

Jeg beviser lemmaerne i den samme rækkefølge, som bliver brugt i [3]. Figur 1 giver en oversigt over, hvordan lemmaerne bruges til at bevise hinanden.

Figur 1: Den overordnede struktur af beviset for PlusCommutativity. En pil fra lemma A til lemma B betyder, at A bliver brugt i beviset for B. Den øverste graf viser ikke de afledte lemmaer, og heller ikke basistilfældene og de induktive skridt i de 3 induktionsbeviser. Den nederste graf har disse detaljer med. For at gøre tegningen pæn er nogle af lemmaernes navne forkortede. “PC” står for “PlusCommutativity”; de øvrige forkortelser skulle være umiddelbart forståelige.

De nedenstående tabeller illustrerer, hvordan makroerne bruges i beviserne for lemmaerne.

EqualReflexivity EqualSymmetry EqualSymmetryRule EqualTransitivity EqualTransitivityRule EqualTransitivityCondRule Mendelson3.2(d)

Mendelson3.2(d)Rule

Mendelson3.2(d)CondRule

Weakening  •  •  •
DoubleMP′  •  •  •
ConditionedMP′  •
DoubleConditionedMP′ • •
ImplyTransitivity  •
PermuteAntecedents  •  •

Mendelson3.2(f)Base Mendelson3.2(f)Indu Mendelson3.2(f)

Mendelson3.2(g)Base Mendelson3.2(g)Indu Mendelson3.2(g)

Mendelson3.2(g)Switch PlusCommutativityBase PlusCommutativityIndu

PlusCommutativity

Weakening • • •
AddOne  • •
SubstitutionMacro •  •
InductionMacro  •  •  •

Tabel 2: Makroer der beviser lemmaer. En “•” i række X , søjle Y betyder, at makro X bliver brugt i beviset for lemma Y . For at gøre tegningen pæn er informationerne fordelt på to tabeller.

6.1 Bevis for EqualReflexivity

[S′ lemma EqualReflexivity: ∀T : T =^{p} T ]

S′ proof of EqualReflexivity:

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

Beviset for EqualReflexivity er så simpelt, at jeg kun vil give en enkelt kommentar: Ideen med aksiomskemaet S5′ er egentlig, at det skal være med til at definere betydningen af addition i Peano aritmetik; men som det kan ses af beviset, kan S5′ også bruges til at bevise lemmaer om =^{p}.

6.2 Bevis for EqualSymmetry og heraf afledt lemma

[S′ lemma EqualSymmetry: ∀T : ∀R: T =^{p} R ˙⇒ R =^{p} T ]

S′ proof of EqualSymmetry:

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: S1′ ≫  T =^{p} R ˙⇒ T =^{p} T ˙⇒ R =^{p} T  ;
L04: PermuteAntecedents ⊳ L03 ≫ T =^{p} T ˙⇒ T =^{p} R ˙⇒ R =^{p} T  ;
L05: EqualReflexivity ≫  T =^{p} T  ;
L06: MP′ ⊳ L04 ⊳ L05 ≫  T =^{p} R ˙⇒ R =^{p} T  □

[figure: 6:T R ˙⇒ RT; ^{MP′}; 4:T T ˙⇒ T R ˙⇒ RT; PermuteAnts; 3:T R ˙⇒ T T ˙⇒ RT; ^{S1′}; 5:T T; EqualReflexivity]

I det ovenstående bevistræ er alle forekomster af tegnet “ ˙⇒” taget med; til gengæld er “=^{p}” underforstået — f.eks. skal “T R” læses som “T =^{p} R”. Jeg vil bruge den samme notation i afsnit 6.3 og 6.4.

[S′ lemma EqualSymmetryRule: ∀T : ∀R: T =^{p} R ⊢ R =^{p} T ]

S′ proof of EqualSymmetryRule:

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: Premise ≫  T =^{p} R  ;
L04: EqualSymmetry ≫  T =^{p} R ˙⇒ R =^{p} T  ;
L05: MP′ ⊳ L04 ⊳ L03 ≫  R =^{p} T  □

Beviset for dette regellemma bruger den samme teknik, som vi så første gang i afsnit 5.3.

6.3 Bevis for EqualTransitivity og heraf afledte lemmaer

[S′ lemma EqualTransitivity: ∀T : ∀R: ∀S: T =^{p} R ˙⇒ R =^{p} S ˙⇒ T =^{p} S]

S′ proof of EqualTransitivity:

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: Arbitrary ≫  S  ;
L04: S1′ ≫  R =^{p} T ˙⇒ R =^{p} S ˙⇒ T =^{p} S  ;
L05: Weakening ⊳ L04 ≫  {T =^{p} R ˙⇒ \atop R =^{p} T ˙⇒ R =^{p} S ˙⇒ T =^{p} S  ;}
L06: EqualSymmetry ≫  T =^{p} R ˙⇒ R =^{p} T  ;
L07: ConditionedMP′⊳L05⊳L06 ≫ T =^{p} R ˙⇒ R =^{p} S ˙⇒ T =^{p} S  □

[figure: 7:T R ˙⇒ RS ˙⇒ T S; ^{CondMP′}; 4–5:T R ˙⇒ RT ˙⇒ RS ˙⇒ T S; S1′-W; 6:T R ˙⇒ RT; EqualSymmetry]

[S′ lemma EqualTransitivityRule: ∀T : ∀R: ∀S: T =^{p} R ⊢ R =^{p} S ⊢ T =^{p} S]

S′ proof of EqualTransitivityRule:

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: Arbitrary ≫  S  ;
L04: Premise ≫  T =^{p} R  ;
L05: Premise ≫  R =^{p} S  ;
L06: EqualTransitivity ≫  T =^{p} R ˙⇒ R =^{p} S ˙⇒ T =^{p} S  ;
L07: DoubleMP′⊳L06⊳L04⊳L05 ≫ T =^{p} S  □

Beviset for dette regellemma bruger den samme teknik, som vi så første gang i afsnit 5.3.

[S′ lemma EqualTransitivityCondRule: ∀A: ∀T : ∀R: ∀S:

A ˙⇒ T =^{p} R ⊢ A ˙⇒ R =^{p} S ⊢ A ˙⇒ T =^{p} S]

S′ proof of EqualTransitivityCondRule:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  T  ;
L03: Arbitrary ≫  R  ;
L04: Arbitrary ≫  S  ;
L05: Premise ≫  A ˙⇒ T =^{p} R  ;
L06: Premise ≫  A ˙⇒ R =^{p} S  ;
L07: EqualTransitivity ≫  T =^{p} R ˙⇒ R =^{p} S ˙⇒ T =^{p} S  ;
L08: Weakening ⊳ L07 ≫  {A ˙⇒ \atop T =^{p} R ˙⇒ R =^{p} S ˙⇒ T =^{p} S  ;}

L09: DoubleConditionedMP′ ⊳

L08 ⊳ L05 ⊳ L06 ≫ A ˙⇒ T =^{p} S □

Vi viser et betinget regellemma som EqualTransitivityCondRule på næsten samme måde, som vi viser et ubetinget regellemma. Først skriver vi præmisserne og moderlemmaet op. Derefter gør vi moderlemmaet betinget ved at bruge Weakening. Til slut bruger vi ConditionedMP′ én gang for hver præmis; dette giver os den ønskede konklusion.

6.4 Bevis for Mendelson3.2(d) og heraf afledte lemmaer

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

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  U  ;
L03: Arbitrary ≫  S  ;
L04: EqualTransitivity ≫  T =^{p} U ˙⇒ U =^{p} S ˙⇒ T =^{p} S  ;
L05: PermuteAntecedents ⊳ L04 ≫ U =^{p} S ˙⇒ T =^{p} U ˙⇒ T =^{p} S  ;
L06: EqualSymmetry ≫ S =^{p} U ˙⇒ U =^{p} S ;
L07: ImplyTransitivity⊳L06⊳L05 ≫ S =^{p} U ˙⇒ T =^{p} U ˙⇒ T =^{p} S  ;
L08: PermuteAntecedents ⊳ L07 ≫ T =^{p} U ˙⇒ S =^{p} U ˙⇒ T =^{p} S  □

[figure: 8:T U ˙⇒ SU ˙⇒ T S; PermuteAnts; 7:SU ˙⇒ T U ˙⇒ T S; ImplyTransitivity; 6:SU ˙⇒ US; EqualSymmetry; 5:US ˙⇒ T U ˙⇒ T S; PermuteAnts; 4:T U ˙⇒ US ˙⇒ T S; EqualTransitivity]

[S′ lemma Mendelson3.2(d)Rule: ∀T : ∀R: ∀S: T =^{p} R ⊢ S =^{p} R ⊢ T =^{p} S]

S′ proof of Mendelson3.2(d)Rule:

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: Arbitrary ≫  S  ;
L04: Premise ≫  T =^{p} R  ;
L05: Premise ≫  S =^{p} R  ;
L06: Mendelson3.2(d) ≫  T =^{p} R ˙⇒ S =^{p} R ˙⇒ T =^{p} S  ;
L07: DoubleMP′⊳L06⊳L04⊳L05 ≫ T =^{p} S  □

Beviset for dette regellemma bruger den samme teknik, som vi så første gang i afsnit 5.3.

[S′ lemma Mendelson3.2(d)CondRule: ∀A: ∀T : ∀R: ∀S:

A ˙⇒ T =^{p} R ⊢ A ˙⇒ S =^{p} R ⊢ A ˙⇒ T =^{p} S]

S′ proof of Mendelson3.2(d)CondRule:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  T  ;
L03: Arbitrary ≫  R  ;
L04: Arbitrary ≫  S  ;
L05: Premise ≫  A ˙⇒ T =^{p} R  ;
L06: Premise ≫  A ˙⇒ S =^{p} R  ;
L07: Mendelson3.2(d) ≫  T =^{p} R ˙⇒ S =^{p} R ˙⇒ T =^{p} S  ;
L08: Weakening ⊳ L07 ≫  {A ˙⇒ \atop T =^{p} R ˙⇒ S =^{p} R ˙⇒ T =^{p} S  ;}

L09: DoubleConditionedMP′ ⊳

L08 ⊳ L05 ⊳ L06 ≫ A ˙⇒ T =^{p} S □

Beviset for dette betingede regellemma bruger den samme teknik, som vi brugte til at vise EqualTransitivityCondRule i afsnit 6.3.

6.5 Bevis for Mendelson3.2(f)

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

S′ proof of Mendelson3.2(f)Base:

L01: S5′ ≫ ṫ ˙+ ˙0 =^{p} ṫ ;
L02: EqualSymmetryRule ⊳ L01 ≫ ṫ =^{p} ṫ ˙+ ˙0  ;

L03: SubstitutionMacro @ ṫ @ ˙0 ⊳

L02 ≫ ˙0 =^{p} ˙0 ˙+ ˙0 □

Dette bevis illustrerer nytten af makroen SubstitutionMacro. Bemærk i øvrigt de to snabel-a’er i linie 3; deres formål er at fortælle Logiwebs bevischecker, at de to meta-variable Z og C i SubstitutionMacro skal instantieres til hhv. ṫ og ˙0.

I skrivende stund kan Logiwebs bevischecker ikke selv nå frem til, hvordan Z og C skal instantieres (fordi disse meta-variable kun optræder i sidebetingelsen i SubstitutionMacro).

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

S′ proof of Mendelson3.2(f)Indu:

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

L04: Mendelson3.2(d)CondRule ⊳ L01 ⊳ L03 ≫

ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ □

Jeg vil ikke illustrere dette bevis med et bevistræ; hele arbejdet gøres med en anvendelse af Mendelson3.2(d)CondRule på to aksiomer (hvoraf det ene er gjort betinget med Weakening).

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

S′ proof of Mendelson3.2(f):

L01: Mendelson3.2(f)Base ≫  ˙0 =^{p} ˙0 ˙+ ˙0  ;
L02: Mendelson3.2(f)Indu ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′  ;
L03: InductionMacro⊳L01⊳L02 ≫ ṫ =^{p} ˙0 ˙+ ṫ  □

Som det kan ses, gør InductionMacro det meget enkelt at færdiggøre et induktionsbevis.

6.6 Bevis for Mendelson3.2(g) og heraf afledt lemma

[S′ lemma Mendelson3.2(g)Base: ṫ′ ˙+ ˙0 =^{p} (ṫ ˙+ ˙0)′]

S′ proof of Mendelson3.2(g)Base:

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

L04: Mendelson3.2(d)Rule ⊳

L01 ⊳ L03 ≫ ṫ′ ˙+ ˙0 =^{p} (ṫ ˙+ ˙0)′ □

[figure: 4:t′ + 0 = (t + 0)′; Drule; 1:t′ + 0 = t′; _{S5_{′}}; 3:(t + 0)′ = t′; AddOne; 2:t + 0 = t; _{S5_{′}}]

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

S′ proof of Mendelson3.2(g)Indu:

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

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

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

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

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

L04: EqualTransitivityCondRule ⊳

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

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

L05: S6′ ≫  ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′  ;
L06: AddOne ⊳ L05 ≫  (ṫ ˙+ ṙ′)′ =^{p} ((ṫ ˙+ ṙ)′)′  ;

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

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

L08: Mendelson3.2(d)CondRule ⊳

L04 ⊳ L07 ≫ ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′ ˙⇒

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

8:t′ + r =(t + r)′ ˙⇒ t′ + r′ =(t + r′)′

DCondRule

4:t′ + r =(t + r)′ ˙⇒ t′ + r′ =(t + r)′′

EqualTransitivityCondRule

1:t′ + r =(t + r)′ ˙⇒ (t′ + r)′ =(t + r)′′

S2_{′}

2–3:t′ + r =(t + r)′ ˙⇒ t′ + r′ =(t′ + r)′ S6′-W

6–7:t′ + r =(t + r)′ ˙⇒ (t + r′)′ =(t + r)′′

AddOne-W

5:t + r′ =(t + r)′

S6_{′}

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

S′ proof of Mendelson3.2(g):

L01: Mendelson3.2(g)Base ≫ ṫ′ ˙+ ˙0 =^{p} (ṫ ˙+ ˙0)′ ;

L02: Mendelson3.2(g)Indu ≫ ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′ ˙⇒

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

L03: InductionMacro⊳L01⊳L02 ≫ ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′  □

Ligesom i afsnit 6.5 har vi her færdiggjort induktionsbeviset ved hjælp af InductionMacro.

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

S′ proof of Mendelson3.2(g)Switch:

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

L02: SubstitutionMacro @ ṫ @ ṡ ⊳

L01 ≫ ṡ′ ˙+ ṙ =^{p} (ṡ ˙+ ṙ)′ ;

L03: SubstitutionMacro @ ṙ @ ṫ ⊳

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

L04: SubstitutionMacro @ ṡ @ ṙ ⊳

L03 ≫ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ □

Som det kan ses, er det ganske enkelt at bytte om på variabelnavnene i et lemma som Mendelson3.2(g), når vi først har makroen SubstitutionMacro til rådighed. Det eneste raffinement er, at vi må introducere en hjælpevariabel ṡ: Hvis vi f.eks. havde konkluderet ṙ′ ˙+ ṙ =^{p} (ṙ ˙+ ṙ)′ i linie 2, ville vi ikke længere kunne udtrykke, at lemmaet gælder for to forskellige variable.

6.7 Bevis for PlusCommutativity

[S′ lemma PlusCommutativityBase: ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ]

S′ proof of PlusCommutativityBase:

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

L03: EqualTransitivityRule ⊳

L01 ⊳ L02 ≫ ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ □

Vi har udelukkende vist Mendelson3.2(f) for at kunne bruge det i dette bevis; men som det ses, har vi heller ikke brug for meget mere for at vise PlusCommutativityBase.

[S′ lemma PlusCommutativityIndu: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ] S′ proof of PlusCommutativityIndu:

L01: S2′ ≫ ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒

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

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

L03: Weakening ⊳ L02 ≫

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

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

L04: EqualTransitivityCondRule ⊳

L03 ⊳ L01 ≫ ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒

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

L05: Mendelson3.2(g)Switch ≫ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ;

L06: Weakening ⊳ L05 ≫

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

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

L07: Mendelson3.2(d)CondRule ⊳ L04 ⊳ L06 ≫

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

7:t + r = r + t ˙⇒ t + r′ = r′ + t

DCondRule

4:t + r = r + t ˙⇒ t + r′ =(r + t)′

EqualTransitivityCondRule

2-3:t + r = r + t ˙⇒ t + r′ =(t + r)′ S6′-W 1:t + r = r + t ˙⇒ (t + r)′ =(r + t)′

S2_{′}

5-6:t + r = r + t ˙⇒ r′ + t =(r + t)′ Gswitch-W

[S′ lemma PlusCommutativity: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ] S′ proof of PlusCommutativity:

L01: PlusCommutativityBase ≫  ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ  ;
L02: PlusCommutativityIndu ≫  ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ ;
L03: InductionMacro⊳L01⊳L02 ≫ ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ  □

Den sidste af de 28 hjælpesætninger vises altså ved en simpel anvendelse af InductionMacro. Hermed er det lovede bevis for sætning (1) færdiggjort.

A Navnet på dette dokument

Den følgende definition fastlægger dette dokuments Logiweb-navn:

[peano commutativity =^{pyk} “peano commutativity”]

B TEX definitioner

[Weakening =^{tex} “Weakening”] [DoubleMP′ =^{tex} “DoubleMP’”] [ConditionedMP′ =^{tex} “ConditionedMP’”] [DoubleConditionedMP′ =^{tex} “DoubleConditionedMP’”] [ImplyTransitivity =^{tex} “ImplyTransitivity”] [PermuteAntecedents =^{tex} “PermuteAntecedents”] [AddOne =^{tex} “AddOne”] [SubstitutionMacro =^{tex} “SubstitutionMacro”] [InductionMacro =^{tex} “InductionMacro”] [EqualReflexivity =^{tex} “EqualReflexivity”] [EqualSymmetry =^{tex} “EqualSymmetry”] [EqualSymmetryRule =^{tex} “EqualSymmetryRule”] [EqualTransitivity =^{tex} “EqualTransitivity”] [EqualTransitivityRule =^{tex} “EqualTransitivityRule”] [EqualTransitivityCondRule =^{tex} “EqualTransitivityCondRule”] [Mendelson3.2(d) =^{tex} “Mendelson3.2(d)”] [Mendelson3.2(d)Rule =^{tex} “Mendelson3.2(d)Rule”] [Mendelson3.2(d)CondRule =^{tex} “Mendelson3.2(d)CondRule”] [Mendelson3.2(f)Base =^{tex} “Mendelson3.2(f)Base”] [Mendelson3.2(f)Indu =^{tex} “Mendelson3.2(f)Indu”] [Mendelson3.2(f) =^{tex} “Mendelson3.2(f)”] [Mendelson3.2(g)Base =^{tex} “Mendelson3.2(g)Base”] [Mendelson3.2(g)Indu =^{tex} “Mendelson3.2(g)Indu”] [Mendelson3.2(g) =^{tex} “Mendelson3.2(g)”] [Mendelson3.2(g)Switch =^{tex} “Mendelson3.2(g)Switch”] [PlusCommutativityBase =^{tex} “PlusCommutativityBase”] [PlusCommutativityIndu =^{tex} “PlusCommutativityIndu”] [PlusCommutativity =^{tex} “PlusCommutativity”]

C Litteratur

[1] Klaus Grue. A logiweb base page. Logiweb-dokument tilgængelig

på hjemmesiden: http://www.diku.dk/~grue/logiweb/20050502/home/
grue/base/GRD-2005-06-03-UTC-15-49-33-495567.

[2] Klaus Grue.  Peano arithmetic.  Logiweb-dokument tilgængelig

på hjemmesiden: http://www.diku.dk/~grue/logiweb/20050502/home/
grue/peano-axioms/GRD-2005-06-03-UTC-15-58-02-061312.

[3] Elliott Mendelson. Introduction to Mathematical Logic. Chapman & Hall, fourth edition, 1997.