Logik

Allan Hvam Petersen (220282-2137)

4. juli 2005

Indhold

1 Forord 3 2 Sammenfatning 3 3 Introduktion 4 3.1 Opgaveformulering . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.2 Logiweb og Pyk . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 4 Propositions teorien 6 4.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 4.2 Standarder . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 4.3 Simple beviser . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 4.3.1 Bevis MP′_{d} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 4.3.2 Bevis A1′_{i} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.3.3 Bevis A2′_{i} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.3.4 Bevis A2′_{ii} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.3.5 Bevis A2′_{iid} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 4.3.6 Bevis 1.8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4.3.7 Bevis 1.8_{i} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4.3.8 Bevis 1.47 b . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4.3.9 Bevis 1.47 c . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 4.3.10 Bevis 1.47 e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 5 Deduktion 13 5.1 Definitioner . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 5.2 Oversættelse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 5.2.1 Brug af hypotese . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 5.2.2 Instanciering af aksiom/lemma . . . . . . . . . . . . . . . . . . . . 14 5.2.3 Brug af lemma med modus ponens . . . . . . . . . . . . . . . . . . 14 5.2.4 Brug af modus ponens . . . . . . . . . . . . . . . . . . . . . . . . . 14 5.3 Eksempel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 5.4 Optimering af eksempel . . . . . . . . . . . . . . . . . . . . . . . . . 16 5.5 Nye beviskonstruktioner . . . . . . . . . . . . . . . . . . . . . . . . . 16 5.5.1 Brug af regler . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 5.5.2 Brug af MP lokalt . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 5.5.3 Brug af MP eksternt . . . . . . . . . . . . . . . . . . . . . . . . . . 18 5.6 Eksempel med nye konstruktioner . . . . . . . . . . . . . . . . . . . 18 5.7 Hypotetiske beviser . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 5.7.1 Bevis A1′_{ih} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 5.7.2 Bevis A2′_{ih} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 5.7.3 Bevis A2′_{iih} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 5.7.4 Bevis 1.47 b_{h} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 5.7.5 Bevis 1.47 c_{h} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 5.8 Flere niveauer af deduktion . . . . . . . . . . . . . . . . . . . . . . . 21 5.8.1 Konjunktion af hypoteser . . . . . . . . . . . . . . . . . . . . . . . 22 5.9 Beviser med brug af deduktion . . . . . . . . . . . . . . . . . . . . . 23 5.9.1 Bevis 1.10 a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 5.9.2 Bevis 1.10 b . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 6 Peano Aritmetik 24 6.1 Introduktion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 6.2 Simple beviser i peano aritmetik . . . . . . . . . . . . . . . . . . . . 25 6.2.1 Bevis S1′_{i} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 6.2.2 Bevis S1′_{ii} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 6.2.3 Bevis S2′_{i} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 6.2.4 Bevis S2′_{ih} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 6.2.5 Bevis S9′_{ii} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 6.2.6 Bevis Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 6.3 Beviser i proposition 3.2 . . . . . . . . . . . . . . . . . . . . . . . . . 28 6.3.1 Bevis 3.2 a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 6.3.2 Bevis 3.2 b . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 6.3.3 Bevis 3.2 b_{i} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 6.3.4 Bevis 3.2 c . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 6.3.5 Bevis 3.2 c_{ii} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 6.3.6 Bevis 3.2 c_{iih} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 6.3.7 Bevis 3.2 d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 6.3.8 Bevis 3.2 d_{ii} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 6.3.9 Bevis 3.2 d_{iih} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 6.3.10 Bevis 3.2 f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 6.3.11 Bevis 3.2 g . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 6.3.12 Bevis 3.2 h . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 A Diverse 34 B TEX Definitioner 34 C Prioritets Tabel 39 D Litteratur 42

1 Forord

Denne rapport er resultatet af et projektarbejde i kurset Logik på Københavns Universitet, udarbejdet i perioden 2. juni til 4. juli af Allan Hvam Petersen. Formålet med opgaven er at skrive et maskinchecket bevis i systemet Logiweb, som dermed danner grundlag for den resulterende karakter i kurset. Læseren af denne rapport bør være bekendt med dele af Logiweb-systemet samt, L^{A}TEX og have en matematisk grundforståelse. Hvis man fra andre Logiweb-sider ønsker at referer til denne, kan følgende kana-reference eller URL benyttes:

nani

suta suka tine nese neka tasu sine tusa seke siku kiku kata kutu kise sisa tuke tenu saku kene nite kene kusi kise sisa kake saka sika nasa natu

http://www.diku.dk/ grue/logiweb/20050502/home/ahvam/logic/latest/vector/page.lgw

Rapporten er inddelt i følgende afsnit:

Sammenfatning Beskrivelse af projektforløbet, samt vurdering af løsningen.

Introduktion Introduktion af opgaven og teknologi.

Propositions teorien Opbygning af simple beviser.

Deduktion Beskriver oversættelse af beviser på Mendelson-form med hypoteser til beviser på Logiweb-form, desuden definere afsnittet egne konstruktioner til beviser med hypoteser.

Peano Aritmetik Beviser indenfor peano aritmetik.

Bilag er inddelt som følger:

Diverse Samling af diverse definitioner.

TEX Definitioner TEX definitioner for alle konstruktioner i dokumentet.

Prioritets Tabel Prioritets tabel med nye konstruktioner.

Litteratur Litteratur liste.

2 Sammenfatning

Opgaven er løst, og bevist af sætning Mendelson 3.2 h fra [3] er udført indenfor Logiweb-systemet. Endvidere er beviset korrekt, forudsat bevis-checkeren på basis-siden er korrekt. Det endelige bevis kan ses i afsnit 6.3.12. Beviset af Mendelson 3.2 h har ikke koncentreret sig så meget om kreativitet og finde på selve beviset, snarer at få kendskab til detaljerne i Logiweb. Logiweb og de referede Logiweb-sider har til tider båret lidt præg af at systemet/siderne ikke har været helt gennemtestet, men det har dog også haft sin charme og givet en ekstra uventede udfordringer. Denne logiweb-side referer til den seneste version af Klaus Grues basis-side, samt en modificeret version af hans seneste peano-side. Den modificerede version kan findes under mine logiweb publikationer på adressen http://www.diku.dk/

~grue/logiweb/20050502/home/ahvam/. Fra den originale peano-side, er alle

beviserne samt nogle konstruktioner blevet fjernet og et par TEX fejl er blevet udbedret. Ændringerne er foretaget for at undgå tvetydigheder på denne side. Enkelte af beviserne i denne rapport er ikke bevist i [3], udarbejdelsen af disse beviser har til tider været særdeles tidskrævende. Endvidere er beviserne holdt så enkelte og korte som muligt, men der er sikkert nogle få der kan udformes endnu mere enkelt. I afsnit 5.5 bliver der introduceret en række makrodefinitioner, man med fordel kan udnytte til hypotetiske beviser. Konstruktionerne har næppe sparet mig for tid, da opbygningen af disse har været en tidskrævende opgave. Dog har konstruktionerne vist sig yderst anvendelige, da beviserne er blevet nemmere at skrive efter indførelsen af de nye konstruktioner. Mange af beviserne i rapporten er skrevet om adskillige gange, i første omgang blev beviserne frem til Mendelson 3.2 g skrevet. Men da dette bevis fyldte over en hel side, var det på tide at indføre de navngivnings-standarder og abstraktioner beskrevet i afsnit 4.2 (Eksempelvis opdeling af induktionsbeviser). Beviserne var herefter stadig længere og mere komplekse end de tilsvarende i [3], derfor besluttede jeg mig for at lave de før beskrevne makrodefinitioner. Løbende var der blevet udformet såkaldte omdøbnings-beviser, der tog højde for variabelfangst (sammenfald af metavariabler) som bevis-checkeren ikke tog højde for på det tidspunkt. Efter en del forvirring på logiweb-maillinglisten omkring variabelfangst, besluttede Klaus sig for at implementere en løsning på basis-siden. Herefter skulle mange af beviserne endnu engang omskrives/omdøbes. Tilsammen har disse ændringer været med til at højne kvaliteten af beviserne.

3 Introduktion

3.1 Opgaveformulering

Målet med denne rapport, er i sin enkelthed at bevise formelt at naturlige tal (ℕ) under kompositionen addition er kommutativ:

x + y = y + x

Beviset for dette findes allerede i Mendelson [3], men skal derpå bevises i Logiweb-systemet. Beviset skal udtrykkes i sproget pyk, hvortil der findes en pykoversætter som kan oversætte pyk-kildetekst til Logiweb-sider. pyk-oversætteren og Logiweb vil være til rådighed på DIKU’s førstedel-system på hosten bach-0. For ikke at starte på hel bar bund i Logiweb, er det tilladt at referer til Klaus Grues basis- samt peano-side. Disse sider kan findes på DIKU’s Logiweb in-

stallation på adressen http://www.diku.dk/~grue/logiweb/20050502/home/
grue/.

3.2 Logiweb og Pyk

Logiweb er et system til distribution af formel matematik, en side i Logiweb har flere forskellige synsvinkler/ansigter:

vector Et binært format af siden.

biblopgraphy En liste af referencer en side referer til.

body Selve teksten på siden.

expansion Siden efter makroekspansion.

diagnose Eventuelle fejlbeskeder fra siden.

osv.

En Logiweb-side uden reference til andre kaldes en basis-side. På basis-sider er der på forhånd kun prædefineret et minimal antal af konstruktioner. Det er herefter op til sidens skribent, at definere og indføre betydninger og udseende af nye konstruktioner. En basis-side har desuden enkelte privilegier som andre sider ikke har, med hensyn til erklæring af nye symboler og bootstrapping. Opbygningen af en basis-side kan være et større arbejde, som Klaus Grue heldigvis har gjort for os. Hans basis-side definerer bl.a. tal, lister, makroekspansion, bevis-checker og et utal af andre konstruktioner samt operationer. Hvis man refererer til andre sider kan man ’arve’ de konstruktioner, der er beskrevet på den refererede side. Genereringen af en Logiweb-side sker via oversættelse af en pyk-kildetekst. Et eksempel på skelettet for en sådan tekst kan ses i pyk-eksempel 1. I eksemplet er nøgleord skrevet med stort, og navne med lille.

pyk-eksempel 1: body.pyk

1 PAGE  name

2

3 BIBLIOGRAPHY
4 base: refference

5

6 PREASSOCIATIVE   * fac
7 POSTASSOCIATIVE * apply *

8

9 BODY
10 ''files  and  content

11

12 commands''

Eksemplet viser at man først skal give sin side et navn, derefter erklære man referencer til andre sider. Efter referencerne kommer konstruktionerne, som henholdsvis defineres post- (venstre) eller præ-associative (højre). Rækkefølgen af konstruktionerne angiver prioritet, og stjerner angiver pladser til operanter. En prioritets tabel for alle konstruktioner i dette dokument kan ses i bilag C. BODYordet angiver at selve sidens start, siden kan inddeles i flere filer som man tekstuelt påbegynder og afslutter med andre bestemte nøgleord. Indholdet af en side skrives i TEX, iblandt selve teksten kan der laves en bestemt pyk ’omgivelse’, der giver instruktioner til pyk-oversætteren om at den skal oversætte indholdet af omgivelsen. Til sidst i pyk-filen angiver man kommandoer til oversættelse af .tex-filerne. For at give et eksempel på hvad der kan stå i en pyk ’omgivelse’, er pyk-eksempel 2 der har tre definitioner, inkluderet:

pyk-eksempel 2: fac.pyk

1 math  pyk  define  var x fac as  ''* fac'' end  define  end  math   ; Definition 1

2

3 math  tex  define  var x fac as  ''#1.!'' end  define  end  math   ; Definition 2

4

5 math
6  value  define
7  var x fac
8  as
9  tagged  if var x tagged  equal  zero  then
10  one
11  else
12  var x times  parenthesis  var x minus  one  end  parenthesis  fac  end if
13  end  define
14 end  math   ; Definition 3

Eksempel 2 koncentrerer sig omkring definition af en fakultetsfunktion (n!). Desuden belyser eksemplet også, at konstruktioner kan have flere forskellige aspekter. Alle konstruktioner bør have defineret hvorledes de udtrykkes i sproget pyk selv (Definition 1). tex-aspektet beskriver hvordan en konstruktion skal vises i TEX (Definition 2), og value-aspektet definere hvordan ’værdien’ af et udtryk skal udregnes (Definition 3). Alle TEX definitioner introduceret i dette dokument kan ses i bilag B. Konstruktioner kan have adskillige aspekter, men de tre fra eksemplet er de mest centrale. For en komplet gennemgang af Logiweb, pyk, basis-siden og bevissystemet, kan [1] ses.

4 Propositions teorien

4.1 Definition

Propositions teorien som introduceret i [3], har en række grundelementer der skal være på plads før peano aritmetik kan påbegyndes. Det anvendte sprog i teorien er yderst simpelt:

T → V ; ¬T ; T ⇒ T V → x_{1} ; x_{2} ; ...

Hvor T angiver termer og V angiver en mængde variabler. Teorien har følgende aksiomer, hvor prikkerne over operatorerne bør ignoreres af læseren idet det bliver forklaret i afsnit 6:

A1′ : ∀A: ∀B: A ˙⇒ B ˙⇒ A
A2′ : ∀A: ∀B: ∀C: (A ˙⇒ B ˙⇒ C) ˙⇒ (A ˙⇒ B) ˙⇒ A ˙⇒ C
A3′ : ∀A: ∀B: ( ˙¬ B ˙⇒ ˙¬ A) ˙⇒ ( ˙¬ B ˙⇒ A) ˙⇒ B

Samt en enkelt inferens regel:

MP′ : ∀A: ∀B: A ˙⇒ B ⊢ A ⊢ B

4.2 Standarder

Da der igennem rapporten vil blive introduceret et forholdsvis stort antal sætninger, er der indført følgende standarder til navngivning:

navn _{d} Sætningen har fået tilføjet et ekstra ’argument’, men har stadig den samme ’virkning’. Effekten heraf er ofte at sætning virker som ’dobbelt’ navn (heraf d for dobbelt).

navn _{i} En af de øverste implikations-operatorer i navn’s parse-træ er erstattet af en inferens-operator (heraf i for inferens). Anvendes når navn ønskes anvendt på tværs af linjer, eller til at spare et antal bevislinjer med modus ponens.

navn _{h} Hypotetisk version af navn (heraf h for hypotetisk). Alle undertræer til en inferens-operator (på nær de undertræer hvor den principale operator selv er en inferens-operator) i navn’s parse-træ har fået tilføjet H ⇒ øverst.

navn er her sætningens oprindelige navn, endvidere kan disse endelser kombineres for dermed at danne mere komplekse sætninger. Hvis der eksempelvis tages udgangspunkt i A1′, kan aksiomets parse-træ ses på figur 1.

\begin{matrix}⇒ & A & ⇒ & B & A & [figure] & [figure] & [figure] & [figure] \\ Figur 1: A1′ \end{matrix}

A1′_{i} kan ses på figur 2, det bemærkes at en implikations-operator er blevet udskiftet. Desuden kan A1′_{ih} ses på figur 3, hvor H ⇒ er tilføjet de enkelte undertræer til ⊢ . Af specielle metavariabler kan H nævnes, som bruges til hypotetiske sætninger. Y bruges i induktionsbeviser, hvor der laves induktion over Y. Induktionsbeviser bevises i tre skridt, ’navn i’ beviser basis, ’navn ii’ beviser induktionsskridtet og endelig ’navn’ beviser selve sætningen.

4.3 Simple beviser

I dette afsnit vil der være beviser for et antal lemmaer i propositions teorien, som danner grundlag for efterfølgende afsnit. Alle beviserne bliver bevist indenfor teorien S′, der er defineret på [2] som indeholder alle aksiomerne fra afsnit 4.1.

\begin{matrix}⊢ & A & ⇒ & B & A & [figure] & [figure] & [figure] & [figure] \\ Figur 2: A1′_{i} \end{matrix}

[figure: ⊢; ⇒; ⇒; H; A; H; ⇒; B; A]

Figur 3: A1′_{ih}

For at øge læsbarheden introduceres [x⊵y]^{1} , som bliver makrodefinert til [x⊵y ¨= MP′ ⊳ x ⊳ y].

4.3.1 Bevis MP′_{d}

Det første bevis er [MP′_{d}]^{2} som blot er en dobbelt anvendelse af MP′. Denne sætning reducerer typisk andre beviser med en linje. Sætningen er:

[S′ lemma MP′_{d}: ∀A: ∀B: ∀C: A ˙⇒ B ˙⇒ C ⊢ A ⊢ B ⊢ C]

S′ proof of MP′_{d}:

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

Idet MP′_{d} er bevist, følges eksemplet fra før og [x ⊵ y ⊵ z]^{3} introduceres, der på samme måde er makrodefineret til den dobbelte anvendelse [x ⊵ y ⊵ z ¨= MP′_{d} ⊳ x ⊳ y ⊳ z] .

1[x ⊵ y =^{pyk} “∗ macro modus ponens ∗”]

2[MP′_{d} =^{pyk} “double rule prime mp”]

3[x ⊵ y ⊵ z =^{pyk} “∗ macro first modus ponens ∗ macro second modus ponens ∗”]

4.3.2 Bevis A1′_{i}

Lemmaet [A1′_{i}]^{4} er en inferens version af A1′, som det ses i sætningen er en implikations-operator blevet udskiftet med en inferens-operator:

[S′ lemma A1′_{i}: ∀A: ∀B: A ⊢ B ˙⇒ A]

Beviset føleger:

S′ proof of A1′_{i}:

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

Da denne sætning er essentiel i nogle af de følgende afsnit, gives den navnet [Hypothesize]^{5} , der er makrodefineret til sætningen selv [Hypothesize ¨= A1′_{i}]

4.3.3 Bevis A2′_{i}

[A2′_{i}]^{6} er endnu en inferens version af et aksiom. Lemmaet og beviset er som nedenstående:

[S′ lemma A2′_{i}: ∀A: ∀B: ∀C: A ˙⇒ B ˙⇒ C ⊢ (A ˙⇒ B) ˙⇒ A ˙⇒ C]

S′ proof of A2′_{i}:

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: L05 ⊵ L04 ≫  (A ˙⇒ B) ˙⇒ A ˙⇒ C  □

4.3.4 Bevis A2′_{ii}

[A2′_{ii}]^{7} er den første dobbelte inferens version af et lemma, som det ses i

[S′ lemma A2′_{ii}: ∀A: ∀B: ∀C: A ˙⇒ B ˙⇒ C ⊢ A ˙⇒ B ⊢ A ˙⇒ C]

udskiftes to implikations-operatorer - heraf de to ier. I beviset kan den foregående sætning udnyttes:

4[A1′_{i} =^{pyk} “inference axiom prime a one”]

5[Hypothesize =^{pyk} “rule hypothesize”]

6[A2′_{i} =^{pyk} “inference axiom prime a two”]

7[A2′_{ii} =^{pyk} “inference inference axiom prime a two”]

S′ proof of A2′_{ii}:

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

Anskues A2′_{ii}, ses det at lighederne med MP′ er mange. Reelt er det en hypotetisk version af MP′, derfor bliver [MP′_{h}]^{8} defineret til [MP′_{h} ¨= A2′_{ii}] . Modus ponens blev før defineret med ⊵, herefter vil den hypotetiske version af denne ( [x⊵_{h} y]^{9} ) blive defineret til [x ⊵_{h} y ¨= MP′_{h} ⊳ x ⊳ y] .

4.3.5 Bevis A2′_{iid}

Den første brug af dobbelt-navnet ses af [A2′_{iid}]^{10} . Sætningen

[S′ lemma A2′_{iid}: ∀A: ∀B: ∀C: ∀D: A ˙⇒ B ˙⇒ C ˙⇒ D ⊢ A ˙⇒ B ⊢ A ˙⇒ C ⊢

A ˙⇒ D]

giver perfekt mening i forhold til det sænkede iid. I beviset ses desuden også at det centrale er den dobbelte brug af A2′_{ii}:

S′ proof of A2′_{iid}:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Arbitrary ≫  D  ;
L05: Premise ≫  A ˙⇒ B ˙⇒ C ˙⇒ D  ;
L06: Premise ≫  A ˙⇒ B  ;
L07: Premise ≫  A ˙⇒ C  ;
L08: A2′_{ii} ⊳ L05 ⊳ L06 ≫  A ˙⇒ C ˙⇒ D  ;
L09: A2′_{ii} ⊳ L08 ⊳ L07 ≫  A ˙⇒ D  □

Forholdes lemmaet til MP′_{hd}, ses det at dette er en dobbelt hypotetisk modus ponens. [MP′_{hd}]^{11} bliver derfor makrodefineret til [MP′_{hd} ¨= A2′_{iid}] . På samme måde som før bliver [x ⊵_{h} y ⊵_{h} z]^{12} defineret [x ⊵_{h} y ⊵_{h} z ¨= MP′_{hd} ⊳ x ⊳ y ⊳ z] .

8[MP′_{h} =^{pyk} “hypothetical rule prime mp”]

9[x ⊵_{h} y =^{pyk} “∗ hypothetical macro modus ponens ∗”]

10[A2′_{iid} =^{pyk} “double inference inference axiom prime a two”]

11[MP′_{hd} =^{pyk} “double hypothetical rule prime mp”]

12[x ⊵_{h} y ⊵_{h} z =^{pyk} “∗ hypothetical macro first modus ponens ∗ hypothetical macro second modus ponens var ∗”]

4.3.6 Bevis 1.8 [Mendelson 1.8]^{13} er et grundlæggende bevis i [3]. Sætningen -

[S′ lemma Mendelson 1.8: ∀A: A ˙⇒ A]

- siger at noget medfører sig selv. S′ proof of Mendelson 1.8:

L01: Arbitrary ≫  A  ;
L02: A1′ ≫  A ˙⇒ (A ˙⇒ A) ˙⇒ A  ;
L03: A1′ ≫  A ˙⇒ A ˙⇒ A  ;
L04: A2′_{ii} ⊳ L02 ⊳ L03 ≫  A ˙⇒ A  □

Ovenstående bevis af Mendelson 1.8 bevises i [3] på 5 linjer, hvor denne kun 3. Optimeringen er en konsekvens af de foregående inferens-beviser.

4.3.7 Bevis 1.8_{i} At bevise [Mendelson 1.8_{i}]^{14} som siger [S′ lemma Mendelson 1.8_{i}: ∀A: A ⊢ A] , kan virke besynderligt, men efterfølgende vil dette vise sig nyttigt: S′ proof of Mendelson 1.8_{i}:

L01: Arbitrary ≫  A  ;
L02: Premise ≫  A  ;
L03: Mendelson 1.8 ≫  A ˙⇒ A  ;
L04: L03 ⊵ L02 ≫  A  □
Beviet  navngives  [Repetition]^{15}  via  makrodefinitionen

[Repetition ¨= Mendelson 1.8_{i}] .

4.3.8 Bevis 1.47 b [Mendelson 1.47 b]^{16} er en form for transitivets lemma på implikation:

[S′ lemma Mendelson 1.47 b: ∀A: ∀B: ∀C: A ˙⇒ B ⊢ B ˙⇒ C ⊢ A ˙⇒ C] Beviset udnytter flere af de foregående lemmaer: S′ proof of Mendelson 1.47 b:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;

13[Mendelson 1.8 =^{pyk} “mendelson lemma one eight”]

14[Mendelson 1.8_{i} =^{pyk} “inference mendelson lemma one eight”]

15[Repetition =^{pyk} “rule repetition”]

16[Mendelson 1.47 b =^{pyk} “mendelson exercise one fourtyseven b”]

L04: Premise ≫  A ˙⇒ B  ;
L05: Premise ≫  B ˙⇒ C  ;
L06: A1′_{i} ⊳ L05 ≫  A ˙⇒ B ˙⇒ C  ;
L07: A2′_{ii} ⊳ L06 ⊳ L04 ≫  A ˙⇒ C  □

4.3.9 Bevis 1.47 c [Mendelson 1.47 c]^{17} permutere rækkefølgen af bestemte termer:

[S′ lemma Mendelson 1.47 c: ∀A: ∀B: ∀C: A ˙⇒ B ˙⇒ C ⊢ B ˙⇒ A ˙⇒ C] For første gang benyttes den hypotetiske version af modus ponens: S′ proof of Mendelson 1.47 c:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A ˙⇒ B ˙⇒ C  ;
L05: A2′_{i} ⊳ L04 ≫  (A ˙⇒ B) ˙⇒ A ˙⇒ C  ;
L06: A1′_{i} ⊳ L05 ≫  B ˙⇒ (A ˙⇒ B) ˙⇒ A ˙⇒ C  ;
L07: A1′ ≫  B ˙⇒ A ˙⇒ B  ;
L08: L06 ⊵_{h} L07 ≫  B ˙⇒ A ˙⇒ C  □

4.3.10 Bevis 1.47 e Dette bevis er ikke en oprindelig opgave fra [3], men grundt lighederne med de øvrige beviser fra 1.47-samlingen, placeret her. Selve lemmaet [Mendelson 1.47 e]^{18} siger følgende:

[S′ lemma Mendelson 1.47 e: ∀A: ∀B: ∀C: A ˙⇒ B ˙⇒ C ⊢ B ⊢ A ˙⇒ C] Nedenstående beviser Mendelson 1.47 e: S′ proof of Mendelson 1.47 e:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A ˙⇒ B ˙⇒ C  ;
L05: Premise ≫  B  ;
L06: Mendelson 1.47 c ⊳ L04 ≫  B ˙⇒ A ˙⇒ C  ;
L07: L06 ⊵ L05 ≫  A ˙⇒ C  □

17[Mendelson 1.47 c =^{pyk} “mendelson exercise one fourtyseven c”]

18[Mendelson 1.47 e =^{pyk} “mendelson exercise one fourtyseven e”]

5 Deduktion

5.1 Definitioner

Proposition 1.9 i [3] beviser, at man fra A ⊢ B kan bevise A ⇒ B. Beviskonstruktionerne på basis-siden giver ikke mulighed for at flytte på ⊢ -tegnet, når det først er sat med en præmisse (Premise). Beviset skal derfor udføres således at det korrekte resultat fremkommer direkte. Mendelson [3] bruger i flæng ordet hyp eller hypothesis om hypoteser, men for nærværende skælnes mellem dem som præmisser og hypoteser på følgende måde:

præmisse ⊢ hypotese ⇒ konklusion

Ovenstående ⊢ står længst til højre i en sætning - og da ⊢ er højre associativ kan der være flere præmisser i en sætning. Desuden kaldes en ’hypotese’ kun for en endelig hypotese, hvis det er noget der bliver hypotetisk antaget. Eksempelvis bliver Corollary 1.10 a fra [3]:

B ⇒ C, C ⇒ D ⊢ B ⇒ D

skrevet på følgende måde i Logiweb:

B ˙⇒ C ⊢ C ˙⇒ D ⊢ B ˙⇒ D

Hvor B ˙⇒ C er den første præmisse, C ˙⇒ D den anden, B er hypotesen og D er konklusionen. Nedenstående bevis på mendelson-form af Lemma 1.11 d vil være gennemgående for dette afsnit (i modsætning til [3] er implikation her høje-associativ):

1. ¬A ⇒ ¬B  Hyp
2. (¬A ⇒ ¬B) ⇒ (¬A ⇒ B) ⇒ A  Axiom (A3)
3. B ⇒ ¬A ⇒ B  Axiom (A1)
4. (¬A ⇒ B) ⇒ A  1, 2, MP
5. B ⇒ A  3, 4, Exercise 1.47 b
6. (¬A ⇒ ¬B) ⇒ B ⇒ A  1-5, deduction theorem

I linje 5 bruger [3] dog Corollary 1.10 a, men da dette bevis ikke er lavet endnu, bliver Exercise 1.47 b udnyttet hvor effekten er den samme.

5.2 Oversættelse

Dette afsnit fremfører en algoritme, der tager et bevis på mendelson-form der benytter proposition 1.9 som input. Som output gives et bevis der kan bevises med beviskonstruktionerne fra basis-siden. I det følgende vil [hyp]^{19} være en pladsholder for en given hypotese, [instance]^{20} for en instanciering af et aksiom eller lemma og [conclusion]^{21} for en konklusion.

19[hyp =^{pyk} “hypothesis”]

20[instance =^{pyk} “instance”]

21[conclusion =^{pyk} “conclusion”]

Algoritmen tager en linje ad gangen, fortløbende fra linje 1. Linjen klassificeres herefter til en af følgende typer og foretager oversættelsen:

• Brug af hypotese

• Instanciering af aksiom/lemma

• Brug af lemma med modus ponens

• Brug af modus ponens Oversættelsen af de enkelte typer ses i de følgende afsnit. Selve oversættelsen sørger for, at der altid kommer til at så det ønskede hyp ˙⇒ instance - altså en form for automatisk brug af Proposition 1.9.

5.2.1 Brug af hypotese Mendelson-form:

X. hyp  Hyp

Logiweb-form:

LX.1: Mendelson 1.8 ≫  hyp ˙⇒ hyp  ;

5.2.2 Instanciering af aksiom/lemma Mendelson-form:

X. instance  Axiom/Lemma

Logiweb-form:

LX.1: Axiom/Lemma ≫  instance  ;
LX.2: A1′ ≫  instance ˙⇒ hyp ˙⇒ instance  ;
LX:  LX.2 ⊵ LX.1 ≫  hyp ˙⇒ instance  ;

5.2.3 Brug af lemma med modus ponens Mendelson-form:

X. conclusion  Y, ..., Lemma

Logiweb-form:

LX:  Lemma_{h} ⊳ Y ⊳ ... ≫  hyp ˙⇒ conclusion  ;

5.2.4 Brug af modus ponens Bemærk at [3] for det meste skriver argumenterne omvendt til MP end i S′. Mendelson-form:

X. conclusion  Y, Z, MP

Logiweb-form:

LX.1: A2′ ≫  Z ˙⇒ Y ˙⇒ hyp ˙⇒ conclusion  ;
LX.2: LX.1 ⊵ Z ≫  Y ˙⇒ hyp ˙⇒ conclusion  ;
LX:  LX.2 ⊵ Y ≫  hyp ˙⇒ conclusion  ;

5.3 Eksempel

Med udgangspunkt i eksemplet fra tidligere, anvendes oversættelses-algoritmen. Algoritmen kræver dog at Mendelson 1.47 b_{h} er bevist først - hvilket er foretaget i afsnit 5.7.4. [Mendelson 1.11 d]^{22} vil herefter være navnet på eksemplet, hvor sætningen siger:

[S′ lemma Mendelson 1.11 d: ∀A: ∀B: ( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ B ˙⇒ A]

Idet udførelsen af beviset gennemgås linje for linje, opnås en enkelt anskuelse:

S′ proof of Mendelson 1.11 d:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Mendelson 1.8 ≫  ( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ˙¬ A ˙⇒ ˙¬ B  ;
L04: A3′ ≫  {( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ B) ˙⇒ \atop A  ;}
L05: A1′ ≫  (( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ B) ˙⇒ ; A) ˙⇒ ( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ ; ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ B) ˙⇒ A  ;

L06: L05 ⊵ L04 ≫  {( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ \atop ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ B) ˙⇒ A  ;}
L07: A1′ ≫  B ˙⇒ ˙¬ A ˙⇒ B  ;
L08: A1′ ≫  {(B ˙⇒ ˙¬ A ˙⇒ B) ˙⇒ ( ˙¬ A ˙⇒ \atop ˙¬ B) ˙⇒ B ˙⇒ ˙¬ A ˙⇒ B  ;}
L09: L08 ⊵ L07 ≫  ( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ B ˙⇒ ˙¬ A ˙⇒ B ;
L10: A2′ ≫  (( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ ; ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ B) ˙⇒ A) ˙⇒ ; (( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ˙¬ A ˙⇒ ; ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ; ( ˙¬ A ˙⇒ B) ˙⇒ A  ;

L11: L10 ⊵ L06 ≫  (( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ˙¬ A ˙⇒ ; ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ; ( ˙¬ A ˙⇒ B) ˙⇒ A  ;

L12: L11 ⊵ L03 ≫  {( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ B) ˙⇒ \atop A  ;}

L13: Mendelson 1.47 b_{h} ⊳ L09 ⊳

L12 ≫ ( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ B ˙⇒ A □

22[Mendelson 1.11 d =^{pyk} “mendelson lemma one eleven d”]

5.4 Optimering af eksempel

Da kun aksiomer blev anvendt til definition af basisoversættelsen af beviser på mendelson-form til logiweb-form, blev eksemplet i afsnit 5.3 langt. Beviset reduceres betydeligt såfremt der drages nytte af tidligere beviste sætninger:

S′ proof of Mendelson 1.11 d:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Mendelson 1.8 ≫  ( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ˙¬ A ˙⇒ ˙¬ B  ;
L04: A3′ ≫  {( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ B) ˙⇒ \atop A  ;}
L05: Hypothesize ⊳ L04 ≫  {( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ \atop ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ B) ˙⇒ A  ;}
L06: A1′ ≫  B ˙⇒ ˙¬ A ˙⇒ B  ;
L07: Hypothesize ⊳ L06 ≫  ( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ B ˙⇒ ˙¬ A ˙⇒ B ;
L08: L05 ⊵_{h} L03 ≫  {( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ B) ˙⇒ \atop A  ;}

L09: Mendelson 1.47 b_{h} ⊳ L07 ⊳

L08 ≫ ( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ B ˙⇒ A □

På samme måde som oversættelse fra bevis på mendelson-form til bevis på logiweb-form, kan man også lave en oversættelse til optimeret logiweb-form. Denne oversættelse er dog ikke beskrevet i detaljer her, da den er forholdsvis enkel og fremgår af eksemplet.

5.5 Nye beviskonstruktioner

Selvom beviser kan laves på optimeret logiweb-form, bliver beviserne stadig længere og mere komplekse end de tilsvarende i [3]. En svaghed ved logiwebformen er den eksplicitte angivelse af hypotesen hver gang, hvilket tager meget ’plads’ i beviserne. Endvidere skal der anvendes en Hypothesize hver gang man instancierer et aksiom eller lemma. Formålet med dette afsnit er at afhjælpe disse problemer, for dermed at lave beviser på samme størrelse som i [3]. En måde dette kunne implementeres, er ved at skrive deduktionsalgoritmen ind i selv bevischeckeren på basis-siden. Dette vil dog være at skyde over målet med denne opgave. Istedet bygges løsningsmodellen på makrodefinitioner, der ekspandere ud til konstruktioner som bevischeckeren allerede kender. Den første nye konstruktion til hypotetiske beviser er [Line l : • Hypothesis ≫ i; p]^{23} , som gør det ud for introduktion af en hypotese - svarende til afsnit 5.2.1. Selve konstruktionen er makrodefineret:

[Line l : • Hypothesis ≫ i; p ¨= (Mendelson 1.8 ≫ i ˙⇒ i; let hyp ¨= i in let l ¨= i ˙⇒ i in p)] Konstruktionen har linjenummeret l, konkludere i og har en ’pointer’ p til den næste bevislinje. Ideen er at konstruktionen skal virke på samme måde som en Hyp i [3]. Først konkluderer makroen ud fra Mendelson 1.8 at i ⇒ i, herefter gemmer den hypotesen i i den lokale makrodefinition hyp. Til sidst gemmer den konklusionen fra Mendelson 1.8 i l, så andre linjer kan referer til denne. Det vigtigste ved linjen er at den ’husker’ hypotesen, så man dermed kan undgå at skrive den eksplicit på efterfølgende linjer - den sorte prik efter linjenummeret angiver at linjen læses med hypotesen stående foran. En lille teknisk detalje ved den nye konstruktion, er at den har pointeren til den næste bevislinje. Dermed kan konstruktionen ikke stå sidst i beviset. En mulig måde at løse dette problem på, kunne være at have to versioner af den nye konstruktion - en almindelig og en til den sidste linje. Denne løsning vil dog ikke være at foretrække, da den fordobler antallet af nye beviskonstruktioner. En nem løsning, og den valgte, på problemet er at bruge lemmaet Repetition til at ’udfylde’ den sidste linje.

23[Line l : • Hypothesis ≫ i; p =^{pyk} “line ∗ hypothesis indeed ∗ end line ∗”]

5.5.1 Brug af regler

Brug af aksiomer og lemmaer bliver igen delt op i kategorier - den ene hvor reglen instancieres direkte og den anden hvor reglen instancieres med brug af en eller flere modus ponens. Som vist i afsnit 5.4, anvendes altid en Hypothesize når man instancere en regel som ikke brugere modus ponens. Alternativt skal der være hypotetiske versioner af alle regler - eksempelvis A1′_{h}, A2′_{h} osv. Konstruktionen [Line l : • a ≫ i; p]^{24} laver automatisk en Hypothesize på en instancering af en regel.

[Line l : • a ≫ i; p ¨= (a ≫ i; Hypothesize ⊳ i ≫ hyp ˙⇒ i; let l ¨= hyp ˙⇒ i in p)]

Ovenstående makrodefinition har igen l, i og p i lighed med tidligere. Endvidere har den a som angiver argumentationen linjen er skrevet med. Makroen konkluderer først i ud fra a, hvorefter den laver den hypotetiske version af i med en Hypothesize - bemærk brugen af hyp, der opretholder proposition 1.9. Til instanciering af en regel med brug af modus ponens, kan konstruktionen [Line l : • a ≫ i; p]^{25} bruges. Selve makrodefinitionen:

[Line l : • a ≫ i; p ¨= (a ≫ hyp ˙⇒ i; let l ¨= hyp ˙⇒ i in p)]

er næsten identisk med en af linje konstruktionerne på basis-siden, på nær at hypotesen er skrevet foran hver konklusion. Når denne konstruktion bruges skal man derfor huske kun at bruge hypotetiske versioner af regler, ellers gives en fejlmeddelelse.

24[Line l : • a ≫ i; p =^{pyk} “line ∗ hypothesis because ∗ indeed ∗ end line ∗”]

25[Line l : • a ≫ i; p =^{pyk} “line ∗ hypothesis raw because ∗ indeed ∗ end line ∗”]

5.5.2 Brug af MP lokalt

Endelig kunne man godt nøjes med de tre foregående definitioner, men for at gøre løsningen mere komplet vil der også blive indført nye konstruktioner til brug af modus ponens i hypotetiske beviser. [Line l : • u ⊵ v ≫ i; p]^{26} er blot en hypotetisk brug af modus ponens:

[Line l : • u ⊵ v ≫ i; p ¨= (u ⊵_{h} v ≫ hyp ˙⇒ i; let l ¨= hyp ˙⇒ i in p)]

[Line l : • u ⊵ v ⊵ z ≫ i; p]^{27} definere den dobbelte brug af modus ponens:

[Line l : • u ⊵ v ⊵ z ≫ i; p ¨= (u ⊵_{h} v ⊵_{h} z ≫ hyp ˙⇒ i; let l ¨= hyp ˙⇒ i in p)]

5.5.3 Brug af MP eksternt

Når modus ponens anvendes med et argument der referer ud af en hypotetisk ’blok’, vil man få problemer med at benytte de nye modus ponens konstruktioner fra det foregående afsnit. Der er derfor igen lavet specielle konstruktioner til dette. Referere en modus ponens ekstern i 1. argument, kan [Line l : • u ∘ ⊵ v ≫ i; p]^{28} benyttes - cirklen angiver hvilket argument der er eksternt.

[Line l : • u ∘ ⊵ v ≫ i; p ¨= (Mendelson 1.47 b ⊳ v ⊳ u ≫ hyp ˙⇒ i; let l ¨= hyp ˙⇒ i in p)]

Makrodefinitionen er meget lig de foregående, men tager blot højde for at det ene argument står uden for blokken. Ved modus ponens med reference eksternt i 2. argument, kan [Line l : • u⊵v∘ ≫ i; p]^{29} udnyttes. Makrodefinitionen er igen simpel:

[Line l : • u ⊵ v ∘ ≫ i; p ¨= (Mendelson 1.47 e ⊳ u ⊳ v ≫ hyp ˙⇒ i; let l ¨= hyp ˙⇒ i in p)]

5.6 Eksempel med nye konstruktioner

Da der er blevet lavet en mængede nye konstruktioner, er det oplagt at lave et eksempel med disse:

S′ proof of Mendelson 1.11 d:

L01: Arbitrary ≫  A  ;

26[Line l : • u ⊵ v ≫ i; p =^{pyk} “line ∗ hypothesis modus ponens ∗ modus ponens ∗ indeed ∗ end line ∗”]

27[Line l : • u ⊵ v ⊵ z ≫ i; p =^{pyk} “line ∗ hypothesis double modus ponens ∗ modus ponens ∗ modus ponens ∗ indeed ∗ end line ∗”]

28[Line l : • u ∘ ⊵ v ≫ i; p =^{pyk} “line ∗ hypothesis first modus ponens ∗ modus ponens ∗ indeed ∗ end line ∗”]

29[Line l : • u ⊵ v ∘ ≫ i; p =^{pyk} “line ∗ hypothesis second modus ponens ∗ modus ponens ∗ indeed ∗ end line ∗”]

L02: Arbitrary ≫  B  ;
L03:• Hypothesis ≫  ˙¬ A ˙⇒ ˙¬ B  ;
L04:• A3′ ≫  {( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ ( ˙¬ A ˙⇒ B) ˙⇒ \atop A  ;}
L05:• A1′ ≫  B ˙⇒ ˙¬ A ˙⇒ B  ;
L06:• L04 ⊵ L03 ≫  ( ˙¬ A ˙⇒ B) ˙⇒ A  ;

L07:• Mendelson 1.47 b_{h} ⊳ L05 ⊳

L06 ≫ B ˙⇒ A ;

L08: Repetition ⊳ L07 ≫  ( ˙¬ A ˙⇒ ˙¬ B) ˙⇒ B ˙⇒ A  □

Som det ses antager beviset samme størrelse som i [3]. Dog kan beviset reduceres lidt ved at indføre brug af A3_{ih} - men beviset holdes på samme måde som i [3] for dermed at have et bedre sammenligningsgrundlag.

5.7 Hypotetiske beviser

Dette afsnit indeholder beviser for et antal hypotetiske sætninger som anvendes senere. Beviserne udnytter de nye konstruktioner.

5.7.1 Bevis A1′_{ih}

[A1′_{ih}]^{30}

[S′ lemma A1′_{ih}: ∀H: ∀A: ∀B: H ˙⇒ A ⊢ H ˙⇒ B ˙⇒ A]

S′ proof of A1′_{ih}:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  A  ;
L03: Arbitrary ≫  B  ;
L04: Premise ≫  H ˙⇒ A  ;
L05:• Hypothesis ≫  H  ;
L06:• A1′ ≫  A ˙⇒ B ˙⇒ A  ;
L07:• L06 ⊵ L04 ≫  B ˙⇒ A  ;
L08: Repetition ⊳ L07 ≫  H ˙⇒ B ˙⇒ A  □

5.7.2 Bevis A2′_{ih}

[A2′_{ih}]^{31}

[S′ lemma A2′_{ih}: ∀H: ∀A: ∀B: ∀C: H ˙⇒ A ˙⇒ B ˙⇒ C ⊢ H ˙⇒ (A ˙⇒ B) ˙⇒

A ˙⇒ C]

S′ proof of A2′_{ih}:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  A  ;

30[A1′_{ih} =^{pyk} “hypothetical inference axiom prime a one”]

31[A2′_{ih} =^{pyk} “hypothetical inference axiom prime a two”]

L03: Arbitrary ≫  B  ;
L04: Arbitrary ≫  C  ;
L05: Premise ≫  H ˙⇒ A ˙⇒ B ˙⇒ C  ;
L06:• Hypothesis ≫  H  ;
L07:• A2′ ≫  {(A ˙⇒ B ˙⇒ C) ˙⇒ (A ˙⇒ B) ˙⇒ \atop A ˙⇒ C  ;}
L08:• L07 ⊵ L05 ≫  (A ˙⇒ B) ˙⇒ A ˙⇒ C  ;
L09: Repetition ⊳ L08 ≫  H ˙⇒ (A ˙⇒ B) ˙⇒ A ˙⇒ C  □

5.7.3 Bevis A2′_{iih} [A2′_{iih}]^{32}

[S′ lemma A2′_{iih}: ∀H: ∀A: ∀B: ∀C: H ˙⇒ A ˙⇒ B ˙⇒ C ⊢ H ˙⇒ A ˙⇒ B ⊢

H ˙⇒ A ˙⇒ C]

S′ proof of A2′_{iih}:

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

5.7.4 Bevis 1.47 b_{h} [Mendelson 1.47 b_{h}]^{33}

[S′ lemma Mendelson 1.47 b_{h}: ∀H: ∀A: ∀B: ∀C: H ˙⇒ A ˙⇒ B ⊢ H ˙⇒ B ˙⇒

C ⊢ H ˙⇒ A ˙⇒ C]

S′ proof of Mendelson 1.47 b_{h}:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  A  ;
L03: Arbitrary ≫  B  ;
L04: Arbitrary ≫  C  ;
L05: Premise ≫  H ˙⇒ A ˙⇒ B  ;
L06: Premise ≫  H ˙⇒ B ˙⇒ C  ;
L07:• Hypothesis ≫  H  ;
L08:• A1′_{ih} ⊳ L06 ≫  A ˙⇒ B ˙⇒ C  ;

32[A2′_{iih} =^{pyk} “hypothetical inference inference axiom prime a two”]

33[Mendelson 1.47 b_{h} =^{pyk} “hypothetical mendelson exercise one fourtyseven b”]

L09:• A2′_{iih} ⊳ L08 ⊳ L05 ≫  A ˙⇒ C  ;
L10: Repetition ⊳ L09 ≫  H ˙⇒ A ˙⇒ C  □

5.7.5 Bevis 1.47 c_{h}

[Mendelson 1.47 c_{h}]^{34}

[S′ lemma Mendelson 1.47 c_{h}: ∀H: ∀A: ∀B: ∀C: H ˙⇒ A ˙⇒ B ˙⇒ C ⊢ H ˙⇒

B ˙⇒ A ˙⇒ C]

S′ proof of Mendelson 1.47 c_{h}:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  A  ;
L03: Arbitrary ≫  B  ;
L04: Arbitrary ≫  C  ;
L05: Premise ≫  H ˙⇒ A ˙⇒ B ˙⇒ C  ;
L06:• Hypothesis ≫  H  ;
L07:• A2′_{ih} ⊳ L05 ≫  (A ˙⇒ B) ˙⇒ A ˙⇒ C  ;
L08:• A1′_{ih} ⊳ L07 ≫  B ˙⇒ (A ˙⇒ B) ˙⇒ A ˙⇒ C  ;
L09:• A1′ ≫  B ˙⇒ A ˙⇒ B  ;
L10:• A2′_{iih} ⊳ L08 ⊳ L09 ≫  B ˙⇒ A ˙⇒ C  ;
L11: Repetition ⊳ L10 ≫  H ˙⇒ B ˙⇒ A ˙⇒ C  □

5.8 Flere niveauer af deduktion

I de foregående afsnit blev deduktion i et niveau beskrevet, men der kan selvfølgelig også laves deduktion i flere niveauer. Selve oversættelsesalgoritmen fra afsnit 5.2, kan igen bruges ved blot at starte fra den inderste hypotese og arbejde sig ud. Men igen vil beviserne blive betydelig større og mere komplekse end i [3]. En anden måde beviserne kunne udformes, er at bruge de nye beviskonstruktioner til det yderste niveau, og så lave det manuelt for de inderste. [Mendelson 1.11 c]^{35} er et eksempel på en sætning der bruger 2 niveauer af deduktion. Sætningen er som følger:

[S′ lemma Mendelson 1.11 c: ∀A: ∀B: ˙¬ A ˙⇒ A ˙⇒ B]

Nedenstående viser beviset af eksemplet:

S′ proof of Mendelson 1.11 c:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03:• Hypothesis ≫  ˙¬ A  ;
L04:• Mendelson 1.8 ≫  A ˙⇒ A  ;
L05:• A1′ ≫  A ˙⇒ ˙¬ B ˙⇒ A  ;

34[Mendelson 1.47 c_{h} =^{pyk} “hypothetical mendelson exercise one fourtyseven c”]

35[Mendelson 1.11 c =^{pyk} “mendelson lemma one eleven c”]

L06:• A1′_{ih} ⊳ L05 ≫  A ˙⇒ A ˙⇒ ˙¬ B ˙⇒ A  ;
L07:• A1′ ≫  ˙¬ A ˙⇒ ˙¬ B ˙⇒ ˙¬ A  ;
L08:• A1′_{ih} ⊳ L07 ≫  A ˙⇒ ˙¬ A ˙⇒ ˙¬ B ˙⇒ ˙¬ A  ;
L09:• A2′_{iih} ⊳ L06 ⊳ L04 ≫  A ˙⇒ ˙¬ B ˙⇒ A  ;
L10:• L07 ⊵ L03 ≫  ˙¬ B ˙⇒ ˙¬ A  ;
L11:• A1′_{ih} ⊳ L10 ≫  A ˙⇒ ˙¬ B ˙⇒ ˙¬ A  ;
L12:• A3′ ≫  {( ˙¬ B ˙⇒ ˙¬ A) ˙⇒ ( ˙¬ B ˙⇒ A) ˙⇒ \atop B  ;}
L13:• A1′_{ih} ⊳ L12 ≫  {A ˙⇒ ( ˙¬ B ˙⇒ ˙¬ A) ˙⇒ ( ˙¬ B ˙⇒ \atop A) ˙⇒ B  ;}
L14:• A2′_{iih} ⊳ L13 ⊳ L11 ≫  A ˙⇒ ( ˙¬ B ˙⇒ A) ˙⇒ B  ;
L15:• A2′_{iih} ⊳ L14 ⊳ L09 ≫  A ˙⇒ B  ;
L16: Repetition ⊳ L15 ≫  ˙¬ A ˙⇒ A ˙⇒ B  □

På samme måde som der blev lavet nye makrodefinitioner for det første niveau af deduktion, kan der også laves definitioner for det andet niveau. Disse definitioner er dog ikke defineret i denne rapport, da det vil gøre rapporten unødvendig længere fordi der kun vil være minimal brug for det i forhold til beviset af Mendelson 3.2 h (kommutativitet for addition).

5.8.1 Konjunktion af hypoteser

Når man arbejder med deduktion i flere niveauer, kan man også samle alle hypoteserne til en:

hyp ˙∧ hyp ˙⇒ conclusion

Da ˙∧ binder stærkere end ˙⇒, vil det overfor systemet blive opfattet som en enkelt hypotese. For at fuldføre disse beviser vil man også få brug for følgende sætninger:

[Mendelson 1.48 d]^{36}

[S′ lemma Mendelson 1.48 d: ∀A: ∀B: A ˙∧ B ˙⇒ A]

[Mendelson 1.48 e]^{37}

[S′ lemma Mendelson 1.48 e: ∀A: ∀B: A ˙∧ B ˙⇒ B]

[Mendelson 1.48 h]^{38}

[S′ lemma Mendelson 1.48 h: ∀A: ∀B: A ˙⇒ B ˙⇒ A ˙∧ B]

Bemærk at disse sætninger ikke er bevist, igen fordi der er minimal brug for deduktion i flere niveauer.

36[Mendelson 1.48 d =^{pyk} “mendelson exercise one fourtyeight d”]

37[Mendelson 1.48 e =^{pyk} “mendelson exercise one fourtyeight e”]

38[Mendelson 1.48 h =^{pyk} “mendelson exercise one fourtyeight h”]

5.9 Beviser med brug af deduktion

Corollary 1.10 i [3] ligger op til anvendelse af Proposition 1.9, til nogle af de samme beviser som fra Exercise 1.47. Dette eksempel følges, og begge sætninger fra 1.10 vil blive bevist med de nye konstruktioner. Fremover vil Corollary 1.10 blive brugt i stedet for Exercise 1.47.

5.9.1 Bevis 1.10 a [Mendelson 1.10 a]^{39}

[S′ lemma Mendelson 1.10 a: ∀A: ∀B: ∀C: A ˙⇒ B ⊢ B ˙⇒ C ⊢ A ˙⇒ C] S′ proof of Mendelson 1.10 a:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A ˙⇒ B  ;
L05: Premise ≫  B ˙⇒ C  ;
L06:• Hypothesis ≫  A  ;
L07:• L04 ∘ ⊵ L06 ≫  B  ;
L08:• L05 ∘ ⊵ L07 ≫  C  ;
L09: Repetition ⊳ L08 ≫  A ˙⇒ C  □

5.9.2 Bevis 1.10 b [Mendelson 1.10 b]^{40}

[S′ lemma Mendelson 1.10 b: ∀A: ∀B: ∀C: A ˙⇒ B ˙⇒ C ⊢ B ⊢ A ˙⇒ C] S′ proof of Mendelson 1.10 b:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A ˙⇒ B ˙⇒ C  ;
L05: Premise ≫  B  ;
L06:• Hypothesis ≫  A  ;
L07:• L04 ∘ ⊵ L06 ≫  B ˙⇒ C  ;
L08:• L07 ⊵ L05 ∘ ≫  C  ;
L09: Repetition ⊳ L08 ≫  A ˙⇒ C  □

39[Mendelson 1.10 a =^{pyk} “mendelson corollary one ten a”]

40[Mendelson 1.10 b =^{pyk} “mendelson corollary one ten b”]

6 Peano Aritmetik

6.1 Introduktion

Peano aritmetik er en 1. ordens teori, det er derfor naturlig at introducere 1. ordens prædikat teorien først. 1. ordens prædikat teorien bygger videre på propositions teorien, beskrevet i afsnit 4. Sproget fra propositions teorien er derfor en delmængde af 1. ordens prædikat teoriens sprog:

F → R ; ¬F ; F ⇒ F ; ∀V: F R → A_{1}(P) ; A_{2}(P) ; ... P → T ; T , P T → V ; C ; T′ T′ → f_{1}(P) ; f_{2}(P) ; ... C → a_{1} ; a_{2} ; ... V → x_{1} ; x_{2} ; ...

Hvor F angiver formler, R relationssymboler, P parameterliste, T termer, T′ funktioner, C konstanter og V variabler. 1. ordens teorien udbygger propositions teorien med yderlige 3 aksiomer:

A4′ : ∀C: ∀A: ∀X: ∀B: ⌈A⌉≡⟨⌈B⌉|⌈X ⌉ := ⌈C⌉⟩ ⊢⊢ ˙∀X: B ˙⇒ A
A5′ : ∀X: ∀A: ∀B: ṅonfree(⌈X ⌉, ⌈A⌉) ⊢⊢ ˙∀X: (A ˙⇒ B) ˙⇒ A ˙⇒ ˙∀X: B
Gen′ : ∀X: ∀A: A ⊢ ˙∀X: A

Tegnet ⊢⊢ angiver sidebetingelser - altså ting der skal være opfyldt før aksiomet må benyttes. Sidebetingelserne i A4′ og A5′ behandler ting som validering af substitution og betingelsen ’ikke fri for’. En ny ting i aksiomerne er ˙∀, som er en objektkvantor der variere over variabler - i modsætning til ∀ der variere over termer/formler. Peano aritmetik har et enkelt relationssymbol, = som herefter vil blive kalde lighed. Desuden har teorien en enkelt konstant 0 (nul) og tre funktioner x′, x+y og x · y. x′ er en efterfølger-funktion der giver det næste tal efter x, x + y er addition og x · y er multiplikation. Peano’s teori har desuden følgende aksiomer:

S1′ : ∀A: ∀B: ∀C: A =^{p} B ˙⇒ A =^{p} C ˙⇒ B =^{p} C

S2′ : ∀A: ∀B: A =^{p} B ˙⇒ A′ =^{p} B′

S3′ : ∀A: ¬˙0 =^{p} A′

S4′ : ∀A: ∀B: A′ =^{p} B′ ˙⇒ A =^{p} B

S5′ : ∀A: A ˙+ ˙0 =^{p} A

S6′ : ∀A: ∀B: A ˙+ B′ =^{p} (A ˙+ B)′

S7′ : ∀A: A ˙· ˙0 =^{p} ˙0

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

S9′ : ∀A: ∀B: ∀C: ∀X:

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

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

Det første der springer en i øjne når man ser aksiomerne er nok de prikker der er sat over alle operatorerne, samt p’et over lighedsoperatoren. Disse tegn har til formål at skelne peano relaterede ting fra lignende ting defineret på basis-side. Eksempelvis at skelne peano addition fra almindelig addition. Ud fra S1′ (og lidt ekstra) kan det bevises at lighed er en ækvivalensrelation. S5′ til S8′ behandler rekursion af addition samt multiplikation og S9′ siger at princippet om matematisk induktion gælder i peano aritmetik.

6.2 Simple beviser i peano aritmetik

Dette afsnit indeholder mest inferens- og hypotetiske-beviser af aksiomerne, men også et par interessante beviser omkring induktion. Beviserne er lavet så der kan spares et par linjer i senere beviser.

6.2.1 Bevis S1′_{i}

[S1′_{i}]^{41}

[S′ lemma S1′_{i}: ∀A: ∀B: ∀C: A =^{p} B ⊢ A =^{p} C ˙⇒ B =^{p} C]

S′ proof of S1′_{i}:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A =^{p} B  ;
L05: S1′ ≫  A =^{p} B ˙⇒ A =^{p} C ˙⇒ B =^{p} C  ;
L06: L05 ⊵ L04 ≫  A =^{p} C ˙⇒ B =^{p} C  □

6.2.2 Bevis S1′_{ii}

[S1′_{ii}]^{42}

[S′ lemma S1′_{ii}: ∀A: ∀B: ∀C: A =^{p} B ⊢ A =^{p} C ⊢ B =^{p} C]

41[S1′_{i} =^{pyk} “inference axiom prime s one”]

42[S1′_{ii} =^{pyk} “inference inference axiom prime s one”]

S′ proof of S1′_{ii}:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A =^{p} B  ;
L05: Premise ≫  A =^{p} C  ;
L06: S1′_{i} ⊳ L04 ≫  A =^{p} C ˙⇒ B =^{p} C  ;
L07: L06 ⊵ L05 ≫  B =^{p} C  □

6.2.3 Bevis S2′_{i} [S2′_{i}]^{43}

[S′ lemma S2′_{i}: ∀A: ∀B: A =^{p} B ⊢ A′ =^{p} B′]

S′ proof of S2′_{i}:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Premise ≫  A =^{p} B  ;
L04: S2′ ≫  A =^{p} B ˙⇒ A′ =^{p} B′  ;
L05: L04 ⊵ L03 ≫  A′ =^{p} B′  □

6.2.4 Bevis S2′_{ih} [S2′_{ih}]^{44}

[S′ lemma S2′_{ih}: ∀H: ∀A: ∀B: H ˙⇒ A =^{p} B ⊢ H ˙⇒ A′ =^{p} B′]

S′ proof of S2′_{ih}:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  A  ;
L03: Arbitrary ≫  B  ;
L04: Premise ≫  H ˙⇒ A =^{p} B  ;
L05:• Hypothesis ≫  H  ;
L06:• S2′ ≫  A =^{p} B ˙⇒ A′ =^{p} B′  ;
L07:• L06 ⊵ L04 ≫  A′ =^{p} B′  ;
L08: Repetition ⊳ L07 ≫  H ˙⇒ A′ =^{p} B′  □

6.2.5 Bevis S9′_{ii} [S9′_{ii}]^{45} er en inferens-version af induktions-aksiomet. I selve sætningen, er to implikationsoperatoere blevet udskiftet:

43[S2′_{i} =^{pyk} “inference axiom prime s two”]

44[S2′_{ih} =^{pyk} “hypothetical inference axiom prime s two”]

45[S9′_{ii} =^{pyk} “inference inference axiom prime s nine”]

[S′ lemma S9′_{ii}: ∀A: ∀B: ∀C: ∀Y: B≡⟨A|Y := ˙0⟩ ⊢⊢ C≡⟨A|Y := Y′⟩ ⊢⊢
B ⊢ ˙∀Y: (A ˙⇒ C) ⊢ ˙∀Y: A]

Selve beviset er ligefrem, det skal dog bemærkes hvordan sidebetingelser kan elimineres:

S′ proof of S9′_{ii}:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Arbitrary ≫  Y  ;
L05: Side-condition ≫  B≡⟨A|Y := ˙0⟩  ;
L06: Side-condition ≫  C≡⟨A|Y := Y′⟩  ;
L07: Premise ≫  B  ;
L08: Premise ≫  ˙∀Y: (A ˙⇒ C)  ;
L09: S9′ ⊳ ⊳ L05 ⊳ ⊳ L06 ≫  B ˙⇒ ˙∀Y: (A ˙⇒ C) ˙⇒ ˙∀Y: A  ;
L10: L09 ⊵ L07 ⊵ L08 ≫  ˙∀Y: A  □

6.2.6 Bevis Induction

For at lette anvendelsen af induktion er sætningen [Induction]^{46} blevet lavet, sætningen siger følgende:

[S′ lemma Induction: ∀A: ∀B: ∀C: ∀Y: B≡⟨A|Y := ˙0⟩ ⊢⊢ C≡⟨A|Y := Y′⟩ ⊢⊢

⌈A⌉≡⟨⌈A⌉|⌈Y⌉ := ⌈Y⌉⟩ ⊢⊢ B ⊢ A ˙⇒ C ⊢ A]

Grundtanken med sætningen er at anvende den direkte på ens basis og induktionsskridt, for direkte at få det ønskede resultat. I sætningen er der tilføjet en ekstra sidebetingelse, så A4′ kan instancieres:

S′ proof of Induction:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Arbitrary ≫  Y  ;
L05: Side-condition ≫  B≡⟨A|Y := ˙0⟩  ;
L06: Side-condition ≫  C≡⟨A|Y := Y′⟩  ;
L07: Side-condition ≫  ⌈A⌉≡⟨⌈A⌉|⌈Y⌉ := ⌈Y⌉⟩  ;
L08: Premise ≫  B  ;
L09: Premise ≫  A ˙⇒ C  ;
L10: Gen′ ⊳ L09 ≫  ˙∀Y: (A ˙⇒ C)  ;

L11: S9′_{ii} ⊳ ⊳ L05 ⊳ ⊳

L06 ⊳ L08 ⊳ L10 ≫ ˙∀Y: A ;

L12: A4′ ⊳ ⊳ L07 ≫  ˙∀Y: A ˙⇒ A  ;
L13: L12 ⊵ L11 ≫  A  □

46[Induction =^{pyk} “rule induction”]

6.3 Beviser i proposition 3.2

Dette afsnit fremføre det endelige bevis, beviserne følger [3] meget tæt. Der bevises desuden en række inferensversioner af sætningerne.

6.3.1 Bevis 3.2 a [Mendelson 3.2 a]^{47}

[S′ lemma Mendelson 3.2 a: ∀A: A =^{p} A] S′ proof of Mendelson 3.2 a:

L01: Arbitrary ≫  A  ;
L02: S5′ ≫  A ˙+ ˙0 =^{p} A  ;
L03: S1′_{ii} ⊳ L02 ⊳ L02 ≫  A =^{p} A  □

6.3.2 Bevis 3.2 b [Mendelson 3.2 b]^{48}

[S′ lemma Mendelson 3.2 b: ∀A: ∀B: A =^{p} B ˙⇒ B =^{p} A] S′ proof of Mendelson 3.2 b:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: S1′ ≫  A =^{p} B ˙⇒ A =^{p} A ˙⇒ B =^{p} A  ;
L04: Mendelson 3.2 a ≫  A =^{p} A  ;
L05: Mendelson 1.10 b⊳L03⊳L04 ≫ A =^{p} B ˙⇒ B =^{p} A  □

6.3.3 Bevis 3.2 b_{i} [Mendelson 3.2 b_{i}]^{49} [S′ lemma Mendelson 3.2 b_{i}: ∀A: ∀B: A =^{p} B ⊢ B =^{p} A] S′ proof of Mendelson 3.2 b_{i}:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Premise ≫  A =^{p} B  ;
L04: Mendelson 3.2 b ≫  A =^{p} B ˙⇒ B =^{p} A  ;
L05: L04 ⊵ L03 ≫  B =^{p} A  □

47[Mendelson 3.2 a =^{pyk} “mendelson proposition three two a”]

48[Mendelson 3.2 b =^{pyk} “mendelson proposition three two b”]

49[Mendelson 3.2 b_{i} =^{pyk} “inference mendelson proposition three two b”]

6.3.4 Bevis 3.2 c [Mendelson 3.2 c]^{50}

[S′ lemma Mendelson 3.2 c: ∀A: ∀B: ∀C: A =^{p} B ˙⇒ B =^{p} C ˙⇒ A =^{p} C] S′ proof of Mendelson 3.2 c:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: S1′ ≫  B =^{p} A ˙⇒ B =^{p} C ˙⇒ A =^{p} C  ;
L05: Mendelson 3.2 b ≫  A =^{p} B ˙⇒ B =^{p} A  ;
L06: Mendelson 1.10 a⊳L05⊳L04 ≫ A =^{p} B ˙⇒ B =^{p} C ˙⇒ A =^{p} C  □

Mendelson 3.2 a (refleksivititet), Mendelson 3.2 b (symmetri) og Mendelson 3.2 c (transitivitet) udgør tilsammen beviset for at lighed i peano aritmetik er en ækvivalensrelation.

6.3.5 Bevis 3.2 c_{ii} [Mendelson 3.2 c_{ii}]^{51}

[S′ lemma Mendelson 3.2 c_{ii}: ∀A: ∀B: ∀C: A =^{p} B ⊢ B =^{p} C ⊢ A =^{p} C] S′ proof of Mendelson 3.2 c_{ii}:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A =^{p} B  ;
L05: Premise ≫  B =^{p} C  ;
L06: Mendelson 3.2 c ≫  A =^{p} B ˙⇒ B =^{p} C ˙⇒ A =^{p} C  ;
L07: L06 ⊵ L04 ⊵ L05 ≫  A =^{p} C  □

6.3.6 Bevis 3.2 c_{iih} [Mendelson 3.2 c_{iih}]^{52}

[S′ lemma Mendelson 3.2 c_{iih}: ∀H: ∀A: ∀B: ∀C: H ˙⇒ A =^{p} B ⊢ H ˙⇒ B =^{p}

C ⊢ H ˙⇒ A =^{p} C]

50[Mendelson 3.2 c =^{pyk} “mendelson proposition three two c”]

51[Mendelson 3.2 c_{ii} =^{pyk} “inference inference mendelson proposition three two c”]

52[Mendelson 3.2 c_{iih} =^{pyk} “hypothetical inference inference mendelson proposition three two c”]

S′ proof of Mendelson 3.2 c_{iih}:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  A  ;
L03: Arbitrary ≫  B  ;
L04: Arbitrary ≫  C  ;
L05: Premise ≫  H ˙⇒ A =^{p} B  ;
L06: Premise ≫  H ˙⇒ B =^{p} C  ;
L07:• Hypothesis ≫  H  ;
L08:• Mendelson 3.2 c ≫  A =^{p} B ˙⇒ B =^{p} C ˙⇒ A =^{p} C  ;
L09:• L08 ⊵ L05 ⊵ L06 ≫  A =^{p} C  ;
L10: Repetition ⊳ L09 ≫  H ˙⇒ A =^{p} C  □

6.3.7 Bevis 3.2 d [Mendelson 3.2 d]^{53}

[S′ lemma Mendelson 3.2 d: ∀A: ∀B: ∀C: A =^{p} B ˙⇒ C =^{p} B ˙⇒ A =^{p} C] S′ proof of Mendelson 3.2 d:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Mendelson 3.2 c ≫  A =^{p} B ˙⇒ B =^{p} C ˙⇒ A =^{p} C  ;
L05: Mendelson 1.47 c ⊳ L04 ≫  B =^{p} C ˙⇒ A =^{p} B ˙⇒ A =^{p} C  ;
L06: Mendelson 3.2 b ≫  C =^{p} B ˙⇒ B =^{p} C  ;
L07: Mendelson 1.10 a⊳L06⊳L05 ≫ C =^{p} B ˙⇒ A =^{p} B ˙⇒ A =^{p} C  ;
L08: Mendelson 1.47 c ⊳ L07 ≫  A =^{p} B ˙⇒ C =^{p} B ˙⇒ A =^{p} C  □

6.3.8 Bevis 3.2 d_{ii} [Mendelson 3.2 d_{ii}]^{54}

[S′ lemma Mendelson 3.2 d_{ii}: ∀A: ∀B: ∀C: A =^{p} B ⊢ C =^{p} B ⊢ A =^{p} C] S′ proof of Mendelson 3.2 d_{ii}:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A =^{p} B  ;
L05: Premise ≫  C =^{p} B  ;
L06: Mendelson 3.2 d ≫  A =^{p} B ˙⇒ C =^{p} B ˙⇒ A =^{p} C  ;
L07: L06 ⊵ L04 ⊵ L05 ≫  A =^{p} C  □

53[Mendelson 3.2 d =^{pyk} “mendelson proposition three two d”]

54[Mendelson 3.2 d_{ii} =^{pyk} “inference inference mendelson proposition three two d”]

6.3.9 Bevis 3.2 d_{iih}

[Mendelson 3.2 d_{iih}]^{55}

[S′ lemma Mendelson 3.2 d_{iih}: ∀H: ∀A: ∀B: ∀C: H ˙⇒ A =^{p} B ⊢ H ˙⇒ C =^{p}

B ⊢ H ˙⇒ A =^{p} C]

S′ proof of Mendelson 3.2 d_{iih}:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  A  ;
L03: Arbitrary ≫  B  ;
L04: Arbitrary ≫  C  ;
L05: Premise ≫  H ˙⇒ A =^{p} B  ;
L06: Premise ≫  H ˙⇒ C =^{p} B  ;
L07:• Hypothesis ≫  H  ;
L08:• Mendelson 3.2 d ≫  A =^{p} B ˙⇒ C =^{p} B ˙⇒ A =^{p} C  ;
L09:• L08 ⊵ L05 ⊵ L06 ≫  A =^{p} C  ;
L10: Repetition ⊳ L09 ≫  H ˙⇒ A =^{p} C  □

6.3.10 Bevis 3.2 f

[Mendelson 3.2 f i]^{56}

[S′ lemma Mendelson 3.2 f i: ˙0 =^{p} ˙0 ˙+ ˙0]

S′ proof of Mendelson 3.2 f i:

L01: S5′ ≫  ˙0 ˙+ ˙0 =^{p} ˙0  ;
L02: Mendelson 3.2 b_{i} ⊳ L01 ≫  ˙0 =^{p} ˙0 ˙+ ˙0  □

[Mendelson 3.2 f ii]^{57}

[S′ lemma Mendelson 3.2 f ii: ẋ =^{p} ˙0 ˙+ ẋ ˙⇒ ẋ′ =^{p} ˙0 ˙+ ẋ′]

S′ proof of Mendelson 3.2 f ii:

L01:• Hypothesis ≫  ẋ =^{p} ˙0 ˙+ ẋ  ;
L02:• S6′ ≫  ˙0 ˙+ ẋ′ =^{p} (˙0 ˙+ ẋ)′  ;
L03:• S2′_{ih} ⊳ L01 ≫  ẋ′ =^{p} (˙0 ˙+ ẋ)′  ;

L04:• Mendelson 3.2 d_{iih} ⊳ L03 ⊳

L02 ≫ ẋ′ =^{p} ˙0 ˙+ ẋ′ ;

L05: Repetition ⊳ L04 ≫  ẋ =^{p} ˙0 ˙+ ẋ ˙⇒ ẋ′ =^{p} ˙0 ˙+ ẋ′  □

[Mendelson 3.2 f]^{58}

55[Mendelson 3.2 d_{iih} =^{pyk} “hypothetical inference inference mendelson proposition three two d”]

56[Mendelson 3.2 f i =^{pyk} “mendelson proposition three two f i”]

57[Mendelson 3.2 f ii =^{pyk} “mendelson proposition three two f ii”]

58[Mendelson 3.2 f =^{pyk} “mendelson proposition three two f”]

[S′ lemma Mendelson 3.2 f: ẋ =^{p} ˙0 ˙+ ẋ]

S′ proof of Mendelson 3.2 f:

L01: Mendelson 3.2 f i ≫  ˙0 =^{p} ˙0 ˙+ ˙0  ;
L02: Mendelson 3.2 f ii ≫  ẋ =^{p} ˙0 ˙+ ẋ ˙⇒ ẋ′ =^{p} ˙0 ˙+ ẋ′  ;
L03: Induction ⊳ L01 ⊳ L02 ≫  ẋ =^{p} ˙0 ˙+ ẋ  □

6.3.11 Bevis 3.2 g

I denne sætning er x og y blevet byttet om, ombytningen er gjort så den kommer til at passe i beviset til Mendelson 3.2 h.

[Mendelson 3.2 g i]^{59}

[S′ lemma Mendelson 3.2 g i: ẏ′ ˙+ ˙0 =^{p} (ẏ ˙+ ˙0)′]

S′ proof of Mendelson 3.2 g i:

L01: S5′ ≫  ẏ′ ˙+ ˙0 =^{p} ẏ′  ;
L02: S5′ ≫  ẏ ˙+ ˙0 =^{p} ẏ  ;
L03: S2′_{i} ⊳ L02 ≫  (ẏ ˙+ ˙0)′ =^{p} ẏ′  ;
L04: Mendelson 3.2 d_{ii}⊳L01⊳L03 ≫ ẏ′ ˙+ ˙0 =^{p} (ẏ ˙+ ˙0)′  □

[Mendelson 3.2 g ii]^{60}

[S′ lemma Mendelson 3.2 g ii: ẏ′ ˙+ ẋ =^{p} (ẏ ˙+ ẋ)′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} (ẏ ˙+ ẋ′)′]

S′ proof of Mendelson 3.2 g ii:

L01:• Hypothesis ≫  ẏ′ ˙+ ẋ =^{p} (ẏ ˙+ ẋ)′  ;
L02:• S6′ ≫  ẏ′ ˙+ ẋ′ =^{p} (ẏ′ ˙+ ẋ)′  ;
L03:• S2′_{ih} ⊳ L01 ≫  (ẏ′ ˙+ ẋ)′ =^{p} ((ẏ ˙+ ẋ)′)′  ;

L04:• Mendelson 3.2 c_{iih} ⊳ L02 ⊳

L03 ≫ ẏ′ ˙+ ẋ′ =^{p} ((ẏ ˙+ ẋ)′)′ ;

L05:• S6′ ≫  ẏ ˙+ ẋ′ =^{p} (ẏ ˙+ ẋ)′  ;
L06:• S2′_{ih} ⊳ L05 ≫  (ẏ ˙+ ẋ′)′ =^{p} ((ẏ ˙+ ẋ)′)′  ;

L07:• Mendelson 3.2 d_{iih} ⊳ L04 ⊳

L06 ≫ ẏ′ ˙+ ẋ′ =^{p} (ẏ ˙+ ẋ′)′ ;

L08: Repetition ⊳ L07 ≫

ẏ′ ˙+ ẋ =^{p} (ẏ ˙+ ẋ)′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p}
(ẏ ˙+ ẋ′)′ □

[Mendelson 3.2 g]^{61}

[S′ lemma Mendelson 3.2 g: ẏ′ ˙+ ẋ =^{p} (ẏ ˙+ ẋ)′] S′ proof of Mendelson 3.2 g:

59[Mendelson 3.2 g i =^{pyk} “mendelson proposition three two g i”]

60[Mendelson 3.2 g ii =^{pyk} “mendelson proposition three two g ii”]

61[Mendelson 3.2 g =^{pyk} “mendelson proposition three two g”]

L01: Mendelson 3.2 g i ≫ ẏ′ ˙+ ˙0 =^{p} (ẏ ˙+ ˙0)′ ;

L02: Mendelson 3.2 g ii ≫

ẏ′ ˙+ ẋ =^{p} (ẏ ˙+ ẋ)′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p}
(ẏ ˙+ ẋ′)′ ;
L03: Induction ⊳ L01 ⊳ L02 ≫ ẏ′ ˙+ ẋ =^{p} (ẏ ˙+ ẋ)′ □

6.3.12 Bevis 3.2 h [Mendelson 3.2 h i]^{62}

[S′ lemma Mendelson 3.2 h i: ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ] S′ proof of Mendelson 3.2 h i:

L01: S5′ ≫  ẋ ˙+ ˙0 =^{p} ẋ  ;
L02: Mendelson 3.2 f ≫  ẋ =^{p} ˙0 ˙+ ẋ  ;
L03: Mendelson 3.2 c_{ii}⊳L01⊳L02 ≫ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ  □

[Mendelson 3.2 h ii]^{63}

[S′ lemma Mendelson 3.2 h ii: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ] S′ proof of Mendelson 3.2 h ii:

L01:• Hypothesis ≫  ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ  ;
L02:• S6′ ≫  ẋ ˙+ ẏ′ =^{p} (ẋ ˙+ ẏ)′  ;
L03:• Mendelson 3.2 g ≫  ẏ′ ˙+ ẋ =^{p} (ẏ ˙+ ẋ)′  ;
L04:• S2′_{ih} ⊳ L01 ≫  (ẋ ˙+ ẏ)′ =^{p} (ẏ ˙+ ẋ)′  ;

L05:• Mendelson 3.2 c_{iih} ⊳ L02 ⊳

L04 ≫ ẋ ˙+ ẏ′ =^{p} (ẏ ˙+ ẋ)′ ;

L06:• Mendelson 3.2 d_{iih} ⊳ L05 ⊳

L03 ≫ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ ;

L07: Repetition ⊳ L06 ≫

ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p}
ẏ′ ˙+ ẋ  □

[Mendelson 3.2 h]^{64}

[S′ lemma Mendelson 3.2 h: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ] S′ proof of Mendelson 3.2 h:

L01: Mendelson 3.2 h i ≫ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ ;

L02: Mendelson 3.2 h ii ≫

ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p}
ẏ′ ˙+ ẋ  ;
L03: Induction ⊳ L01 ⊳ L02 ≫  ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ  □

62[Mendelson 3.2 h i =^{pyk} “mendelson proposition three two h i”]

63[Mendelson 3.2 h ii =^{pyk} “mendelson proposition three two h ii”]

64[Mendelson 3.2 h =^{pyk} “mendelson proposition three two h”]

A Diverse

[logic =^{pyk} “logic”]

B TEX Definitioner

[x ⊵ y =^{tex} “#1.

\unrhd #2.”]

[MP′_{d} =^{tex} “MP’ {d}”]

[x ⊵ y ⊵ z =^{tex} “#1.

\unrhd #2.

\unrhd #3.”]

[A1′_{i} =^{tex} “A1’ {i}”]

[Hypothesize =^{tex} “Hypothesize”]

[A2′_{i} =^{tex} “A2’ {i}”]

[A2′_{ii} =^{tex} “A2’ {ii}”] [MP′_{h} =^{tex} “MP’ {h}”]

[x ⊵_{h} y =^{tex} “#1.

\unrhd h #2.”]

[A2′_{iid} =^{tex} “A2’ {iid}”] [MP′_{hd} =^{tex} “MP’ {hd}”] [x ⊵_{h} y ⊵_{h} z =^{tex} “#1.

\unrhd h #2.

\unrhd h #3.”]

[Mendelson 1.8 =^{tex} “Mendelson\ \textbf{1.8}”] [Mendelson 1.8_{i} =^{tex} “Mendelson\ \textbf{1.8} {i}”] [Repetition =^{tex} “Repetition”] [Mendelson 1.47 b =^{tex} “Mendelson\ \textbf{1.47}\ b”] [Mendelson 1.47 c =^{tex} “Mendelson\ \textbf{1.47}\ c”] [Mendelson 1.47 e =^{tex} “Mendelson\ \textbf{1.47}\ e”] [hyp =^{tex} “\mathsf{hyp}”]

[instance =^{tex} “\mathsf{instance}”]

[conclusion =^{tex} “\mathsf{conclusion}”]

[Mendelson 1.11 d =^{tex} “Mendelson\ \textbf{1.11}\ d”]

[Line l : • Hypothesis ≫ i; p =^{tex} “ \newline \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}\makebox [0.4\textwidth ][l]{$Hypothesis{} \gg{}$}\quad \parbox [t]{0.4\textwidth }{$#2. $\hfill \makebox [0mm][l]{\quad ; }}#3.”]

[Line l : • Hypothesis ≫ i; p =^{name} “ Line \, #1. :\bullet{}\ Hypothesis \gg #2. ; #3.”]

[Line l : • a ≫ i; p =^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$#2. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#3. $\hfill \makebox [0mm][l]{\quad ; }}#4.”]

[Line l : • a ≫ i; p =^{name} “ Line \, #1. :\bullet{}\ #2. \gg #3. ; #4.”]

[Line l : • a ≫ i; p =^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$#2. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#3. $\hfill \makebox [0mm][l]{\quad ; }}#4.”] [Line l : • a ≫ i; p =^{name} “

Line \, #1. :\bullet{}\ #2. \gg #3. ; #4.”]

[Line l : • u ⊵ v ≫ i; p =^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$#2. \unrhd{} #3. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#4. $\hfill \makebox [0mm][l]{\quad ; }}#5.”]

[Line l : • u ⊵ v ≫ i; p =^{name} “ Line \, #1. :\bullet{}\ #2. \unrhd{} #3. \gg #4. ; #5.”]

[Line l : • u ⊵ v ⊵ z ≫ i; p =^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$ #2. \unrhd{} #3. \unrhd{} #4. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#5. $\hfill \makebox [0mm][l]{\quad ; }}#6.”]

[Line l : • u ⊵ v ⊵ z ≫ i; p =^{name} “ Line \, #1. :\bullet{}\ #2. \unrhd{} #3. \unrhd{} #4. \gg #5. ; #6.”]

[Line l : • u ∘ ⊵ v ≫ i; p =^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$ #2. \circ{} \unrhd{} #3. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#4. $\hfill \makebox [0mm][l]{\quad ; }}#5.”]

[Line l : • u ∘ ⊵ v ≫ i; p =^{name} “ Line \, #1. :\bullet{}\ #2. \circ{} \unrhd{} #3. \gg #4. ; #5.”]

[Line l : • u ⊵ v ∘ ≫ i; p =^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$ #2. \unrhd{} #3. \circ{} {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#4. $\hfill \makebox [0mm][l]{\quad ; }}#5.”]

[Line l : • u ⊵ v ∘ ≫ i; p =^{name} “ Line \, #1. :\bullet{}\ #2. \unrhd{} #3. \circ{} \gg #4. ; #5.”]

[A1′_{ih} =^{tex} “A1’ {ih}”]

[A2′_{ih} =^{tex} “A2’ {ih}”]

[A2′_{iih} =^{tex} “A2’ {iih}”]

[Mendelson 1.47 b_{h} =^{tex} “Mendelson\ \textbf{1.47}\ b {h}”]

[Mendelson 1.47 c_{h} =^{tex} “Mendelson\ \textbf{1.47}\ c {h}”]

[Mendelson 1.11 c =^{tex} “Mendelson\ \textbf{1.11}\ c”]

[Mendelson 1.48 d =^{tex} “Mendelson\ \textbf{1.48}\ d”]

[Mendelson 1.48 e =^{tex} “Mendelson\ \textbf{1.48}\ e”] [Mendelson 1.48 h =^{tex} “Mendelson\ \textbf{1.48}\ h”] [Mendelson 1.10 a =^{tex} “Mendelson\ \textbf{1.10}\ a”] [Mendelson 1.10 b =^{tex} “Mendelson\ \textbf{1.10}\ b”]

[S1′_{i} =^{tex} “S1’ {i}”]

[S1′_{ii} =^{tex} “S1’ {ii}”]

[S2′_{i} =^{tex} “S2’ {i}”]

[S2′_{ih} =^{tex} “S2’ {ih}”] [S9′_{ii} =^{tex} “S9’ {ii}”] [Induction =^{tex} “Induction”] [Mendelson 3.2 a =^{tex} “Mendelson\ \textbf{3.2}\ a”] [Mendelson 3.2 b =^{tex} “Mendelson\ \textbf{3.2}\ b”] [Mendelson 3.2 b_{i} =^{tex} “Mendelson\ \textbf{3.2}\ b {i}”] [Mendelson 3.2 c =^{tex} “Mendelson\ \textbf{3.2}\ c”] [Mendelson 3.2 c_{ii} =^{tex} “Mendelson\ \textbf{3.2}\ c {ii}”] [Mendelson 3.2 c_{iih} =^{tex} “Mendelson\ \textbf{3.2}\ c {iih}”] [Mendelson 3.2 d =^{tex} “Mendelson\ \textbf{3.2}\ d”] [Mendelson 3.2 d_{ii} =^{tex} “Mendelson\ \textbf{3.2}\ d {ii}”] [Mendelson 3.2 d_{iih} =^{tex} “Mendelson\ \textbf{3.2}\ d {iih}”] [Mendelson 3.2 f i =^{tex} “Mendelson\ \textbf{3.2}\ f\ i”] [Mendelson 3.2 f ii =^{tex} “Mendelson\ \textbf{3.2}\ f\ ii”] [Mendelson 3.2 f =^{tex} “Mendelson\ \textbf{3.2}\ f”] [Mendelson 3.2 g i =^{tex} “Mendelson\ \textbf{3.2}\ g\ i”] [Mendelson 3.2 g ii =^{tex} “Mendelson\ \textbf{3.2}\ g\ ii”] [Mendelson 3.2 g =^{tex} “Mendelson\ \textbf{3.2}\ g”] [Mendelson 3.2 h i =^{tex} “Mendelson\ \textbf{3.2}\ h\ i”] [Mendelson 3.2 h ii =^{tex} “Mendelson\ \textbf{3.2}\ h\ ii”]

[Mendelson 3.2 h =^{tex} “Mendelson\ \textbf{3.2}\ h”]

C Prioritets Tabel

Priority table Preassociative [logic], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [math ∗ end math], [flush left [∗]], [x], [y], [z], [[∗ ▷◁ ∗]], [[∗ →^{∗} ∗]], [pyk], [tex], [name], [prio], [∗], [T], [if(∗, ∗, ∗)], [[∗ ⇒^{∗} ∗]], [val], [claim], [⊥], [f(∗)], [(∗)^{I}], [F], [\underline{0}], [\underline{1}], [\underline{2}], [\underline{3}], [\underline{4}], [\underline{5}], [\underline{6}], [\underline{7}], [\underline{8}], [\underline{9}], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [a], [b], [c], [d], [e], [f], [g], [h], [i], [j], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [(∗)^{M}], [If(∗, ∗, ∗)], [array{∗} ∗ end array], [l], [c], [r], [empty], [⟨∗ | ∗:= ∗⟩], [M(∗)], [Ũ(∗)], [U(∗)], [U^{M}(∗)], [apply(∗, ∗)], [apply_{1}(∗, ∗)], [identifier(∗)], [identifier_{1}(∗, ∗)], [arrayplus(∗, ∗)], [array-remove(∗, ∗, ∗)], [array-put(∗, ∗, ∗, ∗)], [array-add(∗, ∗, ∗, ∗, ∗)], [bit(∗, ∗)], [bit_{1}(∗, ∗)], [rack], ["vector"], ["bibliography"], ["dictionary"], ["body"], ["codex"], ["expansion"], ["code"], ["cache"], ["diagnose"], ["pyk"], ["tex"], ["texname"], ["value"], ["message"], ["macro"], ["definition"], ["unpack"], ["claim"], ["priority"], ["lambda"], ["apply"], ["true"], ["if"], ["quote"], ["proclaim"], ["define"], ["introduce"], ["hide"], ["pre"], ["post"], [E(∗, ∗, ∗)], [E_{2}(∗, ∗, ∗, ∗, ∗)], [E_{3}(∗, ∗, ∗, ∗)], [E_{4}(∗, ∗, ∗, ∗)], [lookup(∗, ∗, ∗)], [abstract(∗, ∗, ∗, ∗)], [⌈∗⌉], [M(∗, ∗, ∗)], [M_{2}(∗, ∗, ∗, ∗)], [M^{∗}(∗, ∗, ∗)], [macro], [s_{0}], [zip(∗, ∗)], [assoc_{1}(∗, ∗, ∗)], [(∗)^{p}], [self], [[∗ ¨= ∗]], [[∗ ˙= ∗]], [[∗ ´= ∗]], [[∗ =^{pyk} ∗]], [[∗ =^{tex} ∗]], [[∗ =^{name} ∗]], [Priority table[∗]], [M̃_{1}], [M̃_{2}(∗)], [M̃_{3}(∗)], [M̃_{4}(∗, ∗, ∗, ∗)], [M̃(∗, ∗, ∗)], [Q̃(∗, ∗, ∗)], [Q̃_{2}(∗, ∗, ∗)], [Q̃_{3}(∗, ∗, ∗, ∗)], [Q̃^{∗}(∗, ∗, ∗)], [(∗)], [aspect(∗, ∗)], [aspect(∗, ∗, ∗)], [⟨∗⟩], [tuple_{1}(∗)], [tuple_{2}(∗)], [let_{2}(∗, ∗)], [let_{1}(∗, ∗)], [[∗ =^{claim} ∗]], [checker], [check(∗, ∗)], [check_{2}(∗, ∗, ∗)], [check_{3}(∗, ∗, ∗)], [check^{∗}(∗, ∗)], [check_{2}^{∗}(∗, ∗, ∗)], [[∗]^{·}], [[∗]^{−}], [[∗]^{∘}], [msg], [[∗ =^{msg} ∗]], [<stmt>], [stmt], [[∗ =^{stmt} ∗]], [HeadNil′], [HeadPair′], [Transitivity′], [⊥ ⊥], [Contra′], [T′_{E}], [L_{1}], [\underline{∗}], [A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [O], [P], [Q], [R], [S], [T ], [U], [V], [W], [X], [Y], [Z], [⟨∗ | ∗:= ∗⟩], [⟨^{∗}∗ | ∗:= ∗⟩], [∅], [Remainder], [(∗)^{v}], [intro(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗)], [error(∗, ∗)], [error_{2}(∗, ∗)], [proof(∗, ∗, ∗)], [proof_{2}(∗, ∗)], [S(∗, ∗)], [S^{I}(∗, ∗)], [S^{⊳} (∗, ∗)], [S_{1}^{⊳} (∗, ∗, ∗)], [S^{E}(∗, ∗)], [S_{1}^{E}(∗, ∗, ∗)], [S^{+}(∗, ∗)], [S_{1}^{+}(∗, ∗, ∗)], [S^{−}(∗, ∗)], [S_{1}^{−}(∗, ∗, ∗)], [S^{∗}(∗, ∗)], [S_{1}^{∗}(∗, ∗, ∗)], [S_{2}^{∗}(∗, ∗, ∗, ∗)], [S^{@}(∗, ∗)], [S_{1}^{@}(∗, ∗, ∗)], [S^{⊢}(∗, ∗)], [S_{1}^{⊢}(∗, ∗, ∗, ∗)], [S⊢ ⊢(∗, ∗)],

[S⊢ ⊢ ; 1(∗, ∗, ∗, ∗)], [S^{i.e.}(∗, ∗)], [S_{1}^{i.e.}(∗, ∗, ∗, ∗)], [S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗)], [S^{∀}(∗, ∗)],

[S_{1}^{∀}(∗, ∗, ∗, ∗)], [S^{;}(∗, ∗)], [S_{1}^{;}(∗, ∗, ∗)], [S_{2}^{;}(∗, ∗, ∗, ∗)], [T (∗)], [claims(∗, ∗, ∗)], [claims_{2}(∗, ∗, ∗)], [<proof>], [proof], [[Lemma ∗: ∗]], [[Proof of ∗: ∗]], [[∗ lemma ∗: ∗]], [[∗ antilemma ∗: ∗]], [[∗ rule ∗: ∗]], [[∗ antirule ∗: ∗]], [verifier], [V_{1}(∗)], [V_{2}(∗, ∗)], [V_{3}(∗, ∗, ∗, ∗)], [V_{4}(∗, ∗)], [V_{5}(∗, ∗, ∗, ∗)], [V_{6}(∗, ∗, ∗, ∗)], [V_{7}(∗, ∗, ∗, ∗)], [Cut(∗, ∗)], [Head_{⊕}(∗)], [Tail_{⊕}(∗)], [rule_{1}(∗, ∗)], [rule(∗, ∗)], [Rule tactic], [Plus(∗, ∗)], [[Theory ∗]], [theory_{2}(∗, ∗)], [theory_{3}(∗, ∗)], [theory_{4}(∗, ∗, ∗)], [HeadNil′′], [HeadPair′′], [Transitivity′′], [Contra′′], [HeadNil], [HeadPair], [Transitivity], [Contra], [T_{E}], [ragged right], [ragged right expansion ], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗, ∗)], [occur^{∗}(∗, ∗, ∗)], [unify(∗ = ∗, ∗)], [unify^{∗}(∗ = ∗, ∗)], [unify_{2}(∗ = ∗, ∗)], [L_{a}], [L_{b}], [L_{c}], [L_{d}], [L_{e}], [L_{f}], [L_{g}], [L_{h}], [L_{i}], [L_{j}], [L_{k}], [L_{l}], [L_{m}], [L_{n}], [L_{o}], [L_{p}], [L_{q}], [L_{r}], [L_{s}], [L_{t}], [L_{u}], [L_{v}], [L_{w}], [L_{x}], [L_{y}], [L_{z}], [L_{A}], [L_{B}], [L_{C}], [L_{D}], [L_{E}], [L_{F}], [L_{G}], [L_{H}], [L_{I}], [L_{J}], [L_{K}], [L_{L}], [L_{M}], [L_{N}], [L_{O}], [L_{P}], [L_{Q}], [L_{R}], [L_{S}], [L_{T}], [L_{U}], [L_{V}], [L_{W}], [L_{X}], [L_{Y}], [L_{Z}], [L_{?}], [Reflexivity], [Reflexivity_{1}], [Commutativity], [Commutativity_{1}], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)], [conclude_{4}(∗, ∗)], [peano], [˙0], [˙1], [˙2], [ȧ], [ḃ], [ċ], [ḋ], [ė], [ḟ], [ġ], [ḣ], [i̇], [j̇], [k̇], [l̇], [ṁ], [ṅ], [ȯ], [ṗ], [q̇], [ṙ], [ṡ], [ṫ], [u̇], [v̇], [ẇ], [ẋ], [ẏ], [ż], [ṅonfree(∗, ∗)], [ṅonfree^{∗}(∗, ∗)], [ḟree⟨∗|∗ := ∗⟩], [ḟree^{∗}⟨∗|∗ := ∗⟩], [∗≡⟨∗|∗ := ∗⟩], [∗≡⟨^{∗}∗|∗ := ∗⟩], [S], [A1], [A2], [A3], [A4], [A5], [S1], [S2], [S3], [S4], [S5], [S6], [S7], [S8], [S9], [MP], [Gen], [S′], [A1′], [A2′], [A3′], [A4′], [A5′], [S1′], [S2′], [S3′], [S4′], [S5′], [S6′], [S7′], [S8′], [S9′], [MP′], [Gen′], [MP′_{d}], [A1′_{i}], [Hypothesize], [A2′_{i}], [A2′_{ii}], [MP′_{h}], [A2′_{iid}], [MP′_{hd}], [Mendelson 1.8], [Mendelson 1.8_{i}], [Repetition], [Mendelson 1.47 b], [Mendelson 1.47 c], [Mendelson 1.47 e], [Mendelson 1.11 d], [A1′_{ih}], [A2′_{ih}], [A2′_{iih}], [Mendelson 1.47 b_{h}], [Mendelson 1.47 c_{h}], [Mendelson 1.11 c], [Mendelson 1.48 d], [Mendelson 1.48 e], [Mendelson 1.48 h], [Mendelson 1.10 a], [Mendelson 1.10 b], [S1′_{i}], [S1′_{ii}], [S2′_{i}], [S2′_{ih}], [S9′_{ii}], [Induction], [Mendelson 3.2 a], [Mendelson 3.2 b], [Mendelson 3.2 b_{i}], [Mendelson 3.2 c], [Mendelson 3.2 c_{ii}], [Mendelson 3.2 c_{iih}], [Mendelson 3.2 d], [Mendelson 3.2 d_{ii}], [Mendelson 3.2 d_{iih}], [Mendelson 3.2 f], [Mendelson 3.2 f i], [Mendelson 3.2 f ii], [Mendelson 3.2 g], [Mendelson 3.2 g i], [Mendelson 3.2 g ii], [Mendelson 3.2 h], [Mendelson 3.2 h i], [Mendelson 3.2 h ii], [hyp], [instance], [conclusion]; Preassociative [∗ {∗}], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [˙∗]; Preassociative [“ ∗ ”], [], [(∗)^{t}], [string(∗) + ∗], [string(∗) ++ ∗], [ ∗], [ ∗], [!∗], [”∗], [#∗], [$∗], [%∗], [&∗], [’∗], [(∗], [)∗], [∗∗], [+∗], [, ∗], [-∗], [.∗], [/∗], [0∗], [1∗], [2∗], [3∗], [4∗], [5∗], [6∗], [7∗], [8∗], [9∗], [:∗], [; ∗], [<∗], [=∗], [>∗], [?∗], [@∗], [A∗], [B∗], [C∗], [D∗], [E∗], [F∗], [G∗], [H∗], [I∗], [J∗], [K∗], [L∗], [M∗], [N∗], [O∗], [P∗], [Q∗], [R∗], [S∗], [T∗], [U∗], [V∗], [W∗], [X∗], [Y∗], [Z∗], [[∗], [\∗], []∗], [ˆ ∗], [ ∗], [‘∗], [a∗], [b∗], [c∗], [d∗], [e∗], [f∗], [g∗], [h∗], [i∗], [j∗], [k∗], [l∗], [m∗], [n∗], [o∗], [p∗], [q∗], [r∗], [s∗], [t∗], [u∗], [v∗], [w∗], [x∗], [y∗], [z∗], [{∗], [|∗], [}∗], [˜ ∗], [Preassociative ∗; ∗], [Postassociative ∗; ∗], [[∗], ∗], [priority ∗ end], [newline ∗], [macro newline ∗]; Preassociative [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗^{H}], [∗^{T}], [∗^{U}], [∗^{h}], [∗^{t}], [∗^{s}], [∗^{c}], [∗^{d}], [∗^{a}], [∗^{C}], [∗^{M}], [∗^{B}], [∗^{r}], [∗^{i}], [∗^{d}], [∗^{R}], [∗^{0}], [∗^{1}], [∗^{2}], [∗^{3}], [∗^{4}], [∗^{5}], [∗^{6}], [∗^{7}], [∗^{8}], [∗^{9}], [∗^{E}], [∗^{V}], [∗^{C}], [∗^{C^{∗}}], [∗′]; Preassociative [∗ · ∗], [∗ ·_{0} ∗], [∗ ˙· ∗]; Preassociative [∗ + ∗], [∗ +_{0} ∗], [∗ +_{1} ∗], [∗ − ∗], [∗ −_{0} ∗], [∗ −_{1} ∗], [∗ ˙+ ∗]; Preassociative [∗ ∪ {∗}], [∗ ∪ ∗], [∗\{∗}]; Postassociative [∗ ˙. . ∗], [∗ \underline{˙. .} ∗], [∗ \underline{: :} ∗], [∗ \underline{+2∗} ∗], [∗ : : ∗], [∗ +2∗ ∗]; Postassociative [∗, ∗]; Preassociative

[∗ ≈^{B} ∗], [∗ ≈^{D} ∗], [∗ ≈^{C} ∗], [∗ ≈^{P} ∗], [∗ ≈ ∗], [∗ = ∗], [∗ →^{+} ∗], [∗ =^{t} ∗], [∗ =^{t^{∗}} ∗], [∗ =^{r} ∗],

[∗ ∈_{t} ∗], [∗ ⊆_{T} ∗], [∗ =^{T} ∗], [∗ =^{s} ∗], [∗ free in ∗], [∗ free in^{∗} ∗], [∗ free for ∗ in ∗],

[∗ free for^{∗} ∗ in ∗], [∗ ∈_{c} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ =^{p} ∗], [∗^{P}];

Preassociative [¬∗], [ ˙¬ ∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗], [∗ ˙∧ ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗], [∗ ˙∨ ∗]; Preassociative [ ˙∀∗: ∗], [ ˙∃∗: ∗]; Postassociative [∗ ¨⇒ ∗], [∗ ˙⇒ ∗], [∗ ˙⇔ ∗]; Postassociative [∗ : ∗], [∗!∗]; Preassociative

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} ];

Preassociative [λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗^{I}], [∗^{⊳} ], [∗^{V}], [∗^{+}], [∗^{−}], [∗^{∗}]; Preassociative [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗], [∗ ⊵ ∗], [∗ ⊵ ∗ ⊵ ∗], [∗ ⊵_{h} ∗], [∗ ⊵_{h} ∗ ⊵_{h} ∗]; Postassociative [∗ ⊢ ∗], [∗ ⊢⊢ ∗], [∗ i.e. ∗]; Preassociative [∀∗: ∗]; Postassociative [∗ ⊕ ∗]; Postassociative [∗; ∗]; Preassociative [∗ proves ∗]; Preassociative [∗ proof of ∗ : ∗], [Line ∗ : ∗ ≫ ∗; ∗], [Last line ∗ ≫ ∗ □], [Line ∗ : Premise ≫ ∗; ∗], [Line ∗ : Side-condition ≫ ∗; ∗], [Arbitrary ≫ ∗; ∗], [Local ≫ ∗ = ∗; ∗], [Line ∗ : • ∗ ⊵∗ ≫ ∗; ∗], [Line ∗ : • ∗ ∘ ⊵ ∗ ≫ ∗; ∗], [Line ∗ : • ∗ ⊵ ∗ ∘ ≫ ∗; ∗], [Line ∗ : • ∗ ⊵ ∗ ⊵∗ ≫ ∗; ∗], [Line ∗ : • Hypothesis ≫ ∗; ∗], [Line ∗ : • ∗ ≫ ∗; ∗], [Line ∗ : • ∗ ≫ ∗; ∗]; Postassociative [∗ then ∗], [∗[ ∗]∗]; Preassociative [∗&∗]; Preassociative [∗\\∗]; End table

D Litteratur

[1] Klaus Grue. A Logiweb base page. http://www.diku.dk/ grue/logiweb/ 20050502/home/grue/base/latest/, 2005.

[2] Klaus Grue. Peano arithmetic. http://www.diku.dk/ grue/logiweb/ 20050502/home/grue/peano-axioms/latest/, 2005.

[3] Elliott Mendelson. Introduction to Mathematical Logic. Chapman and Hall/CRC, 4. edition, 1997.