Ækvivalensrelationer i Logiweb

Frederik Eriksen (eriksen@diku.dk)

22. juni 2006

Indhold

1 Indledning 4

2 Lidt om Logiweb 4 2.1 Formelle konstruktioner . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Særlige definitioner og tabeller . . . . . . . . . . . . . . . . . . . 5 2.3 L-kode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 Syntaks for ZFsub 6 3.1 Termer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.2 Formler . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.3 Objektvariable vs. metavariable . . . . . . . . . . . . . . . . . . . 6

4 Aksiomatisk system 7

4.1 1. ordens prædikatkalkyle . . . . . . . . . . . . . . . . . . . . . . 7

4.1.1 Håndtering af eksistenskvantorer . . . . . . . . . . . . . . 8 4.2 Selve mængdelæren . . . . . . . . . . . . . . . . . . . . . . . . . . 9

4.2.1 Separation og pladsholdervariable . . . . . . . . . . . . . . 9

5 Makrodefinitioner 11 5.1 Konnektiver . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 5.2 Negerede formler . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 5.3 Delmængde . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 5.4 Singleton-mængde . . . . . . . . . . . . . . . . . . . . . . . . . . 12 5.5 Binær foreningsmængde og fællesmængde . . . . . . . . . . . . . 12 5.6 Relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 5.7 Ækvivalensrelation . . . . . . . . . . . . . . . . . . . . . . . . . . 13 5.8 Mængde-variable . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 5.9 Ækvivalensklasse . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 5.10 Partition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

6 Udsagnslogisk bibliotek 14

6.1 MP-lemmaer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 6.1.1 Det første bevis . . . . . . . . . . . . . . . . . . . . . . . . 16 6.1.2 Beviser for de andre MP-lemmaer . . . . . . . . . . . . . 17

6.2 Implikation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 6.2.1 Refleksivitet; blok-konstruktionen . . . . . . . . . . . . . . 18 6.2.2 Transitivitet . . . . . . . . . . . . . . . . . . . . . . . . . 18 6.2.3 Svækkelse . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 6.2.4 Modsigelse . . . . . . . . . . . . . . . . . . . . . . . . . . 19

6.3 Håndtering af dobbeltnegationer . . . . . . . . . . . . . . . . . . 20 6.4 Modus tollens og beslægtede lemmaer . . . . . . . . . . . . . . . 20 6.5 Konjunktion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

6.5.1 Forening af konjunkter . . . . . . . . . . . . . . . . . . . . 22 6.5.2 Udskilning af anden konjunkt . . . . . . . . . . . . . . . . 22

6.5.3 Udskilning af første konjunkt . . . . . . . . . . . . . . . . 23 6.6 Dobbeltimplikation . . . . . . . . . . . . . . . . . . . . . . . . . . 23

6.6.1 Brug sammen med modus ponens . . . . . . . . . . . . . 23 6.6.2 Kommutativitet . . . . . . . . . . . . . . . . . . . . . . . 24

6.7 Disjunktion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 6.7.1 Svækkelse . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 6.7.2 Slutning ud fra disjunktion . . . . . . . . . . . . . . . . . 25

7 Regellemaer 26 7.1 Par . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 7.2 Foreningsmængde . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 7.3 Potensmængde; sidebetingelser . . . . . . . . . . . . . . . . . . . 27 7.4 Potensmængde, variant . . . . . . . . . . . . . . . . . . . . . . . 29 7.5 Separation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 7.6 Ekstentionalitet . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

7.6.1 Tilstrækkelig betingelse for lighed . . . . . . . . . . . . . 31 7.6.2 Nødvendig betingelse for lighed . . . . . . . . . . . . . . . 32

8 Definitionslemmaer 33 8.1 Refleksiv relation . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 8.2 Symmetrisk relation . . . . . . . . . . . . . . . . . . . . . . . . . 34 8.3 Transitiv relation . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 8.4 Ækvivalensrelation . . . . . . . . . . . . . . . . . . . . . . . . . . 36

9 Basale sætninger i mængdelære 37

9.1 Den tomme mængde . . . . . . . . . . . . . . . . . . . . . . . . . 39 9.1.1 En delmængde af alle mængder . . . . . . . . . . . . . . . 39 9.1.2 Der er kun én tom mængde . . . . . . . . . . . . . . . . . 39 9.1.3 Lemmaet “MemberNotØ” . . . . . . . . . . . . . . . . . . 40

9.2 [x=y] er en ækvivalensrelation . . . . . . . . . . . . . . . . . . . 41 9.3 Negeret lighed . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

10 Lighedslemmaer 44 10.1 Par . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 10.2 Singleton-mængde . . . . . . . . . . . . . . . . . . . . . . . . . . 48 10.3 Foreningsmængde . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 10.4 Binær foreningsmængde . . . . . . . . . . . . . . . . . . . . . . . 50 10.5 Separation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 10.6 Binær fællesmængde . . . . . . . . . . . . . . . . . . . . . . . . . 52

11 Hovedresultatet 54 11.1 Ingen ækvivalensklasser er tomme . . . . . . . . . . . . . . . . . 54 11.2 Alle ækvivalensklasser er disjunkte . . . . . . . . . . . . . . . . . 56

11.2.1 Lemmaet “EqSubset” . . . . . . . . . . . . . . . . . . . . 58 11.2.2 Lemmaet “EqNecessary” . . . . . . . . . . . . . . . . . . 59 11.2.3 Lemmaet “NoneEqNecessary” . . . . . . . . . . . . . . . . 61 11.2.4 To ækvivalensklasser er disjunkte . . . . . . . . . . . . . . 64 11.2.5 Alle ækvivalensklasser er disjunkte . . . . . . . . . . . . . 65 11.2.6 Implikation i stedet for inferens . . . . . . . . . . . . . . . 66

11.3 Ækvivalensklassernes foreningsmængde . . . . . . . . . . . . . . . 67 11.3.1 Den ene halvdel . . . . . . . . . . . . . . . . . . . . . . . 68 11.3.2 Den anden halvdel . . . . . . . . . . . . . . . . . . . . . . 69 11.3.3 De to halvdele sættes sammen . . . . . . . . . . . . . . . 70

11.4 Det sidste bevis . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71

12 Konklusion 72

Litteratur 73

A Oversigt over variabelnavne 73

B Det samlede aksiomsystem 74

C Deduktionsreglen 75 C.1 Motivering . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 C.2 Kode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75

D Pyk definitioner 76

E Prioritetstabel 82

F TEX definitioner 86

Figurer

1 Bevisstrukturen for tautologierne . . . . . . . . . . . . . . . . . . 15 2 Bevisstrukturen for afsnit 9 . . . . . . . . . . . . . . . . . . . . . 38 3 Bevisstrukturen for lighedslemmaerne . . . . . . . . . . . . . . . 45 4 Bevisstrukturen for underafsnit 11.2 . . . . . . . . . . . . . . . . 57

1 Indledning

Denne rapport indeholder et aksiomsystem for en reduceret version af ZF mængdelære, som jeg kalder for “ZFsub”. Ud fra dette aksiomsystem vil jeg vise en række basale sætninger inden for udsagnslogik og mængdelære. Hovedresultatet er, at en ækvivalensrelation på en mængde BS implicit definerer en partition af BS^{1}. Alt det formelle arbejde i rapporten er gennemført med henblik på at bevise dette resultat.

Rapporten er udarbejdet ved hjælp af Logiweb, som er et system til verifikation og publicering af tekster, der indeholder formel matematik. Logiweb har verificeret rapportens beviser og publiceret rapporten på WWW-adressen

http://www.diku.dk/~grue/logiweb/20060417/home/eriksen/equivalence-relations.

Det matematiske indhold af denne rapport er ikke synderligt avanceret; f.eks. fylder materialet om ækvivalensrelationer knap to sider i lærebogen [5] (s. 29– 31). Ideen med rapporten er snarere at afprøve Logiweb end at redegøre for en matematisk teori. Derfor vil jeg ikke gøre alt for meget ud af at forklare de matematiske begreber; fokus vil i højere grad ligge på tekniske forhold omkring formaliseringen.

Rapporten er struktureret som følger: Afsnit 2 er en kort beskrivelse af nogle detaljer ved Logiweb, som er nyttige at kende for en læser af et Logiwebdokument som dette^{2}. Afsnit 3 og 4 omhandler syntaksen og aksiomsystemet for ZFsub, og afsnit 5 indfører de makrodefinitioner, jeg vil gøre brug af. Så kommer vi til lemmaerne og beviserne; vi skal igennem fem afsnit med hjælpesætninger (afsnit 6–10), før vi endelig kan bevise hovedresultatet i afsnit 11. Afsnit 12 slutter af med en konklusion på det hele.

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, dels at et par afsnit indeholder nogle særlige definitioner og tabeller, og endelig at et par andre afsnit indeholder en del programkode. I dette afsnit vil jeg kort beskrive disse fænomener. For en detaljeret beskrivelse af hele Logiweb systemet vil jeg henvise til [3]; 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 Logiweb-dokumenter. De importerede konstruktioner i denne rapport har to kilder: Dels [3], og dels de 3 .pdf filer [4], som tilsammen udgør ét Logiwebdokument.

1Jeg vil referere til denne sætning som “hovedresultatet”. Oprindeligt var det også et mål at bevise det modsatte resultat — at enhver partition implicit definerer en ækvivalensrelation — men det har der ikke været tid til.

2Dette afsnit er en revideret udgave af afsnit 2 i [1].

2.2 Særlige definitioner og tabeller

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. Denne rapports pyk definitioner er vedlagt i bilag D.

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. Denne rapports TEX definitioner er vedlagt i bilag F.

Endelig indeholder bilag E en tabel over alle de formelle konstruktioner i denne rapport — både de importerede og dem, jeg selv har defineret. Denne tabel er først og fremmest med, for at andre Logiweb-dokumenter skal kunne referere til rapporten; uden tabellen kan sådanne referencer ikke finde sted.

2.3 L-kode

Logiweb-dokumentet [3] indeholder et funktionelt programmeringssprog, som jeg vil kalde for “L”. Der er en del forekomster af L-kode i rapporten. For en forklaring af de konstruktioner fra L, som jeg bruger, vil jeg henvise til funktionsbeskrivelserne i appendikset til [4], afsnit 3.2, s. 6. Herudover vil jeg supplere med et par kommentarer undervejs.

3 Syntaks for ZFsub

Som nævnt i indledningen vil jeg arbejde med en reduceret version af ZF mængdelære, som jeg kalder for “ZFsub”. Dette afsnit beskriver syntaksen for ZFsub. Der er to syntaktiske hovedkategorier i ZFsub: Termer og formler. Underafsnit 3.1 beskriver syntaksen for termer, og underafsnit 3.2 beskriver syntaksen for formler.

3.1 Termer

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

           T ::= Værdi | Variabel

Værdi ::= Ø | {T , T } | ∪ T | P(T ) | {ph ∈ T | F}

     Variabel ::= Objekt-var | Ex-var | Ph-var

En Værdi svarer til en konkret mængde — værditermer indeholder ingen variable. Den grundlæggende værdi er den tomme mængde; herudfra kan vi konstruere par, fællesmængder, potensmængder samt delmængder hvis elementer opfylder en bestemt egenskab. Der er således ingen individuelle konstanter i ZFsub; alt er mængder.

En Variabel kan for det første være en objekt-variabel, som varierer over værdier^{3}. De to andre typer af variable — eksistens-variable og pladsholdervariable — vil jeg vente med at forklare til hhv. afsnit 4.1.1 og 4.2.1.

3.2 Formler

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

F ::= T ∈ T | T =T | ˙¬ F | F ⇒ F | ∀Objekt-var: F

Med en formel kan vi altså påstå, at en mængde tilhører en anden mængde, eller at to mængder er lig hinanden. Desuden kan vi negere formler^{4}, lade formler implicere hinanden, samt kvantificere formler med objektvariable.

3.3 Objektvariable vs. metavariable

En metavariabel^{5} er en variabel, der varierer over vilkårlige termer — altså også over objektvariable. Denne rapport er ikke helt fri for objektvariable; men når vi taler om ZFsub i aksiomer^{6}, definitioner og beviser vil jeg så vidt muligt bruge metavariable, da de er mere fleksible end objektvariable. F.eks. kan “s” i formlen [s =X]^{7} kun instantieres til en term; vi kan ikke skifte objektvariabel og konkludere [t = X]. Derimod kan vi sagtens instantiere formlen [S = X] til [t =X]. En liste over de metavariable, jeg vil bruge, kan ses i bilag A.

3Vi repræsenterer objektvariable med symbolerne “a”, “b”, ⋯ “z” samt “OBS”.

4Jeg skriver negationstegnet med en prik over for at undgå forveksling med konstruktionen [¬x] fra [3].

5Vi repræsenterer metavariable med symbolerne “A”, “B”, ⋯ “Z” samt “BS”.

6Strengt taget burde jeg skrive “aksiomskemaer”, da vi bruger metavariable. Da der kun er aksiomskemaer i denne rapport, vil jeg imidlertid bruge ordet “aksiom” for at gøre teksten lidt lettere.

4 Aksiomatisk system

ZFsub er en teori i 1. ordens prædikatkalkyle. Vi kan således opdele aksiomsystemet for ZFsub i to: En prædikatlogisk del og en mængdeteoretisk del. Underafsnit 4.1 gennemgår den prædikatlogiske del, og underafsnit 4.2 gennemgår den mængdeteoretiske del. Bilag B indeholder en kopi af det samlede aksiomsystem.

4.1 1. ordens prædikatkalkyle

Her er de første slutningsregler i ZFsub:

[Theory ZFsub]

[ZFsub rule MP: ΠA, B: A ⇒ B ⊢ A ⊢ B]

[ZFsub rule Gen: ΠX , A: A ⊢ ∀X: A]

[ZFsub rule Repetition: ΠA: A ⊢ A]

[ZFsub rule Neg: ΠA, B: ˙¬ B ⇒ A ⊢ ˙¬ B ⇒ ˙¬ A ⊢ B]

[ZFsub rule Ded: ΠA, B: Dedu(A, B) ⊢⊢ A ⊢ B]

Først et par ord om syntaks: Konstruktionen [x ⊢ y] står for inferens, altså at vi kan bevise y, hvis vi har et bevis for x. Konstruktionen [x ⊢⊢ y] betyder, at y gælder, hvis sidebetingelsen x er sand. Endelig er konstruktionen [Πx: y] en meta-alkvantor; betydningen er, at metavariablen x kan instantieres til hvad som helst — selv andre metavariable.

De viste slutningsregler er næsten identiske med reglerne MP, Gen, Neg og Ded i systemet S fra [4]. Der er dog to ændringer. For det første har jeg tilføjet [ΠA: A ⊢ A] som en slutningsregel. (I [4] vises [ΠA: A ⊢ A] med et lav-niveau bevis). For det andet har jeg lavet en lille ændring i deduktionsreglen Ded, som gør den i stand til at håndtere sidebetingelser bedre. Jeg beskriver ændringen i bilag C.

Som nævnt i [4] kan deduktionsreglen erstatte enhver anvendelse af aksiomskemaerne A4 og A5 fra [6] (se evt. Mendelsons system på s. 69). Derfor har jeg ikke medtaget disse aksiomskemaer. På denne måde får vi også afprøvet deduktionsreglens brugervenlighed; vi skal straks se et eksempel, hvor A4 kunne have gjort nytte.

7En fodnote om stil: Jeg vil ofte indramme matematiske udtryk i firkantede parenteser “[ ]” for at adskille udtrykkene fra den omgivende tekst. De firkantede parenteser har ingen selvstændig betydning.

4.1.1 Håndtering af eksistenskvantorer

Et spørgsmål er nemlig, hvordan man skal håndtere introduktion og elimination af eksistenskvantorer — altså slutninger som f.eks. [Ø = Ø ⊢ ∃x: x = x] og [∃x: x =x ⊢ c =c] (hvor “c” er et ikke tidligere anvendt navn på en konstant).

Det er muligt at håndtere denne slags slutninger alene med reglerne fra afsnit 4.1, men det er omstændigt og tidskrævende (sammenlign f.eks. de to beviser på s. 81 i [6]). Som et minimum kræver det, at man har A4 fra [6] til rådighed — og som nævnt ovenfor har jeg valgt ikke at medtage dette aksiomskema.

Jeg har i stedet implementeret en løsning, der er baseret på begrebet “eksistensvariabel”. Vi indfører en unær operator [x^{Ex}] og definerer, at en term er en ekistens-variabel, hviss den har [x^{Ex}] som principal operator. Funktionen [x^{Ex}] tester, om x er en eksistens-variabel:

[x^{Ex} ˙= x =^{r} ⌈x_{Ex}⌉]^{8}

Vi kan da definere de fire eksistens-variable, som denne rapport vil gøre brug af (jvf. bilag A):

[Ex_{1} ¨= a_{Ex}]^{9}
[Ex_{2} ¨= b_{Ex}]
[Ex_{10} ¨= j_{Ex}]
[Ex_{20} ¨= t_{Ex}]^{10}

Ideen med disse definitioner er at repræsentere en formel som f.eks. [∃x: x =x] ved formlen [X =X], hvor “X ” er en eksistensvariabel. På denne måde kommer eksistensvariablene til at fungere som erstatning for eksistenskvantoren. Dette betyder også, at der ikke er brug for at nogen regel, der eksplicit fjerner eksistenskvantorer — de er allerede væk.

Til gengæld får vi brug for en regel, der kan introducere eksistensvariable. Til den ende definerer vi prædikatet ⟨a≡b|x:=t⟩_{Ex} i L:

[⟨a≡b|x:=t⟩_{Ex} ¨= ⟨⌈a⌉≡^{0}⌈b⌉|⌈x⌉:=⌈t⌉⟩_{Ex}]

[⟨a≡^{0}b|x:=t⟩_{Ex} ˙= λc.x^{Ex} ∧ ⟨a≡^{1}b|x:=t⟩_{Ex}]

[⟨a≡^{1}b|x:=t⟩_{Ex} ˙= a!x!t! if b =^{r} ⌈∀u: v⌉ then F else if b^{Ex} ∧ b =^{t} x then a =^{t} t else a =^{r} b ¨∧ ⟨a^{t}≡^{∗}b^{t}|x:=t⟩_{Ex}] [⟨a≡^{∗}b|x:=t⟩_{Ex} ˙= b!x!t!If(a, T, ⟨a^{h}≡^{1}b^{h}|x:=t⟩_{Ex} ¨∧ ⟨a^{t}≡^{∗}b^{t}|x:=t⟩_{Ex})]

8Konstruktionen [x ˙= y] er en såkaldt “værdidefinition” i L (jvf. afsnit 2.3). Den svarer til en almindelig funktionsdefinition; vi knytter funktionssignaturen x til kroppen y.

9Konstruktionen [x ¨= y] står for “makrodefinition” i L. Vi definerer x som værende en forkortelse for y. Ud fra bevischeckerens synspunkt er der ingen forskel på x og y.

10“j” og “t” er hhv. bogstav nr. 10 og 20 i alfabetet.

Prædikatet ⟨a≡b|x:=t⟩_{Ex} er sandt, hvis x er en eksistens-variabel, og hvis formlen a er identisk med resultatet af at erstatte alle forekomster af x i formlen b med termen t. F.eks. er ⟨(Ø = Ø)≡(Ex_{1} = Ex_{1})|Ex_{1}:=Ø⟩_{Ex} sand. Herudover er det et krav, at hverken a eller b må indeholde objektkvantorer; således er ⟨(∀s: s = Ø)≡(∀s: s = Ex_{1})|Ex_{1}:=Ø⟩_{Ex} falsk. Dette krav er udelukkende indført for at gøre koden for ⟨a≡b|x:=t⟩_{Ex} så simpel som mulig; det har ikke været nødvendigt at sætte ⟨a≡b|x:=t⟩_{Ex} i stand til at håndtere kvantificering.

Vi kan nu definere den slutningsregel, der står for introduktion af eksistensvariable:

[ZFsub rule ExistIntro: ΠX , T , A, B: ⟨A≡B|X:=T ⟩_{Ex} ⊢⊢ A ⊢ B] ^{11}

Med ExistIntro kan vi f.eks. slutte [Ex_{1} =Ex_{1}] ud fra [Ø=Ø]. Vi har nu defineret seks aksiomer, der tilsammen dækker 1. ordens prædikatkalkyle.

4.2 Selve mængdelæren

De aksiomer i ZFsub, der vedrører selve mængdelæren, har jeg hentet fra kapitel 4.3 og 4.4 i [2]. Her er de første fem:

[ZFsub rule Extensionality: ΠX , Y: X =Y ˙⇔ ∀s: (s ∈ X ˙⇔ s ∈ Y)]

[ZFsub rule Ødef: ΠS: ˙¬ S ∈ Ø]

[ZFsub rule PairDef: ΠS, X , Y: S ∈ {X , Y} ˙⇔ S =X ˙∨ S =Y]

[ZFsub rule UnionDef: ΠS, X: S ∈ ∪X ˙⇔ (S ∈ Ex_{10} ˙∧ Ex_{10} ∈ X)]

[ZFsub rule PowerDef: ΠS, X: S ∈ P(X) ˙⇔ ∀s: (s ∈ S ⇒ s ∈ X)]^{12}

Reglen Extensionality siger, at to mængder er ens, hviss de har de samme elementer. De øvrige fire regler definerer begreberne “tom mængde”, “par”, “foreningssmængde” og “potensmængde”. Læg mærke til, at [∪T ] er en unær operator; ideen er, at ∪T er lig med foreningsmængden af alle de mængder, som T indeholder.

Bemærk også at to af aksiomerne indeholder objektvariablen s. Forklaringen herpå er, at aksiomerne indeholder objektkvantoren [∀x: y]; og deduktionsreglen fra [4] er ikke egnet til at håndtere kombinationen “objektkvantor og metavariabel”. Derfor vil x i [∀x: y] altid være en objektvariabel i denne rapport.

4.2.1 Separation og pladsholdervariable

Vi mangler stadigvæk et “separationsaksiom” — dvs. et aksiom, der giver mening til konstruktionen [{ph ∈ T | F}] fra afsnit 3.1. For at implementere separationsaksiomet indfører vi begrebet “pladsholder-variabel”. Fremgangsmåden er den samme som ved eksistens-variable i afsnit 4.1.1. Først indfører vi en unær operator [x_{Ph}] og definerer, at en term er en pladsholder-variabel, hviss den har [x_{Ph}] som primær operator. Funktionen [x^{Ph}] checker, om x er en pladsholdervariabel:

11I denne definition varierer “X ” over eksistens-variable.

12Konstruktionerne [x ˙∧ y], [x ˙∨ y] og [x ˙⇔ y] svarer til de kendte konnektiver; de bliver defineret formelt i afsnit 5.1.

[x^{Ph} ˙= x =^{r} ⌈x_{Ph}⌉]

Vi kan nu definere de pladsholder-variable, vi får brug for, som følger (jvf. bilag A):

[ph_{1} ¨= a_{Ph}]
[ph_{2} ¨= b_{Ph}]
[ph_{3} ¨= c_{Ph}]

Så definerer vi prædikatet ⟨a≡b|x:=t⟩_{Ph} i L:

[⟨a≡b|x:=t⟩_{Ph} ¨= ⟨⌈a⌉≡^{0}⌈b⌉|⌈x⌉:=⌈t⌉⟩_{Ph}]

[⟨a≡^{0}b|x:=t⟩_{Ph} ˙= λc.x^{Ph} ∧ ⟨a≡^{1}b|x:=t⟩_{Ph}]

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

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

Prædikatet ⟨a≡b|x:=t⟩_{Ph} er sandt, hvis x er en pladsholder-variabel, og hvis formlen a er identisk med resultatet af at erstatte alle forekomster af x i formlen b med termen t. Ligesom ved ⟨a≡b|x:=t⟩_{Ex} kræver vi, at hverken a eller b indeholder objektkvantorer. F.eks. er ⟨(Ø ∈ S)≡(ph_{1} ∈ S)|ph_{1}:=Ø⟩_{Ph} sand. Det er i øvrigt tilladt, at a og b indeholder forskellige ekistensvariable; således er ⟨Ex_{1}≡Ex_{2}|ph_{1}:=Ø⟩_{Ph} sand. På denne måde kan vi imødekomme kravet om, at en eksistens-variabel skal være ubrugt, når den introduceres i et bevis.

Vi definerer nu separationsaksiomet SeparationDef ud fra ⟨a≡b|x:=t⟩_{Ph}:

[ZFsub rule SeparationDef: ΠA, B, P, X , Z: P^{Ph} ∧ ⟨B≡A|P:=Z⟩_{Ph} ⊢⊢ Z ∈ {ph ∈ X | A} ˙⇔ Z ∈ X ˙∧ B]

Ved første øjekast virker konjunkten [P^{Ph}] i denne definition overflødig, fordi ⟨B≡A|P:=Z⟩_{Ph} i forvejen kræver, at P er en pladsholder-variabel. Forklaringen er, at “P” kun optræder i definitionens sidebetingelse. Dette betyder, at bevischeckeren har svært ved at finde ud af, hvordan “P” skal instantieres, når vi anvender definitionen. Det ekstra krav [P^{Ph}] hjælper bevischeckeren til at instantiere “P” korrekt.

Med SeparationDef til rådighed kan vi nu f.eks. definere ContainsEmpty(x) som den delmængde af x, hvis elementer indeholder Ø:

[ContainsEmpty(x) ¨= {ph ∈ x | Ø ∈ ph_{1}}],

og vi kan slutte [S ∈ X ˙∧ Ø ∈ S] ud fra [S ∈ ContainsEmpty(X)].

Vi bruger altså en pladsholder-variabel som fri variabel i dén formel F, der definerer delmængden {ph ∈ X | F}. Ideen med at bruge pladsholder-variable (frem for objekt- eller metavariable) til dette formål er, at vi ikke ønsker at kvantificere eller instantiere den frie variabel i F. Det er f.eks. noget sludder at skrive “∀ph_{1}: {ph ∈ X | Ø ∈ ph_{1}}” eller at konkludere “{ph ∈ X | Ø ∈ Ø}” ud fra definitionen af ContainsEmpty(X). Den frie variabel i F skal blot være en pladsholder; derfor pladsholder-variable.

5 Makrodefinitioner

Dette afsnit indeholder dé makrodefinitioner, som vi vil gøre brug af i resten af rapporten. Definitionerne drejer sig for det meste om mængdeteoretiske begreber, f.eks. “ækvivalensklasse” og “partition”. Til sidst i afsnittet formulerer vi hovedresultatet — at der til enhver ækvivalensrelation svarer en partition — som et formelt teorem.

5.1 Konnektiver

Ud fra de to basale konnektiver [ ˙¬ x] og [x ⇒ y] definerer vi konjunktion, disjunktion og dobbeltimplikation:

[x ˙∧ y ¨= ˙¬ (x ⇒ ˙¬ y)]
[x ˙∨ y ¨= ˙¬ x ⇒ y]
[x ˙⇔ y ¨= (x ⇒ y) ˙∧ (y ⇒ x)]

5.2 Negerede formler

Det er ganske enkelt at definere negeret lighed (x ≠ y) og negeret medlemskab (x ∉ y):

[x ≠ y ¨= ˙¬ x=y]
[x ∉ y ¨= ˙¬ x ∈ y]^{13}

5.3 Delmængde

Mængden x er en delmængde af y hviss ethvert medlem af x også tilhører y:

[x ⊆ y ¨= (s ∈ x ⇒ s ∈ y)]

13Højresiderne i disse definitioner skal læses som hhv. [ ˙¬ (x=y)] og [ ˙¬ (x ∈ y)].

Vi kommer ikke til at bruge denne definition ret ofte. Man får tit en bedre føling med, hvad der foregår i beviserne, hvis man skriver definitionen ud. Desuden bruger denne definition af [x ⊆ y] objektvariable og implikation; vi vil ofte foretrække at bruge metavariable og inferens i stedet (som f.eks. i [S ∈ x ⊢ S ∈ y]).

5.4 Singleton-mængde

[{x}] er mængden, der indeholder x som sit eneste element. Vi definerer [{x}] ved at parre x med sig selv:

[{x} ¨= {x, x}]

5.5 Binær foreningsmængde og fællesmængde

Vi definerer foreningsmængden mellem to mængder x og y som følger:

[x ∪ y ¨= ∪{{x}, {y}}]

Fællesmængden mellem to mængder x og y er en delmængde af deres foreningsmængde:

[x ∩ y ¨= {ph ∈ x ∪ y | ph_{3} ∈ x ˙∧ ph_{3} ∈ y}]

5.6 Relation

Det ordnede par ⟨x, y⟩ indeholder x som “førstekomponent” og y som “andenkomponent”. Den følgende definition af ⟨x, y⟩ er den mest udbredte i litteraturen (se f.eks. afsnit 4.3 i [2] og afsnit 2.1 i [5]):

[⟨x, y⟩ ¨= {{x}, {x, y}}]

Vi kan nu definere en “relation” som en mængde af ordnede par. Vi udtrykker denne definition ved at formalisere, hvad det vil sige, at x er relateret til y i kraft af relationen r:

[r(x, y) ¨= ⟨x, y⟩ ∈ r]

Vi kommer faktisk ikke til at bruge disse to definitioner i rapporten; beviserne vil behandle [r(x, y)] som en primitiv konstruktion. Men det er alligevel betryggende at have det formelle grundlag for relationsbegrebet på plads.

5.7 Ækvivalensrelation

At en relation er refleksiv på en mængde x vil sige, at alle elementer i x er relateret til sig selv:

[ReflRel(r, x) ¨= ∀s: (s ∈ x ⇒ r(s, s))]

At en relation er symmetrisk på en mængde x vil sige, at alle elementer i x opfylder den følgende implikation:

[SymRel(r, x) ¨= ∀s, t: (s ∈ x ⇒ t ∈ x ⇒ r(s, t) ⇒ r(t, s))]

At en relation er transitiv på en mængde x vil sige, at alle elementer i x opfylder den følgende implikation:

[TransRel(r, x) ¨=

∀s, t, u: (s ∈ x ⇒ t ∈ x ⇒ u ∈ x ⇒ r(s, t) ⇒ r(t, u) ⇒ r(s, u))]

Endelig er en ækvivalensrelation det samme som en relation, der er refleksiv, symmetrisk og transitiv:

[EqRel(r, x) ¨= ReflRel(r, x) ˙∧ SymRel(r, x) ˙∧ TransRel(r, x)]

5.8 Mængde-variable

Mange af rapportens beviser sker i forhold til en uspecificeret mængde. Vi vil referere til denne mængde med metavariablen BS og objektvariablen OBS:

[BS ¨= \underline{bs}]
[OBS ¨= \overline{bs}]^{14}

Vi vil så vidt muligt bruge metavariablen, men i afsnit 10.6 og senere bliver det nødvendigt at gå over til objektvariablen.

5.9 Ækvivalensklasse

Lad r være en ækvivalensrelation defineret på bs, og lad x være et medlem af bs. Vi definerer ækvivalensklassen [x ∈ bs]_{r} som den delmængde af bs, hvis medlemmer står i forhold til x:

[[x ∈ bs]_{r} ¨= {ph ∈ bs | r(ph_{1}, x)}]

Ækvivalenssystemet bs/r er mængden af alle de ækvivalensklasser, som bs definerer på r. Vi definerer bs/r som en delmængde af potensmængden P(bs):

[bs/r ¨= {ph ∈ P(bs) | Ex_{20} ∈ bs ˙∧ [Ex_{20} ∈ bs]_{r} =ph_{2}}]

14Navnene “BS” og “OBS” står for hhv. for “big set” og “object big set”. Konstruktionerne [\underline{x}] og [\overline{x}] omdanner x til hhv. en meta- og en objektvariabel. Variablen [bs] vil også blive brugt i nogle af de kommende definitioner, men ikke i selve beviserne.

5.10 Partition

En partition af en mængde bs er en mængde p, som opfylder tre krav:

1. Ingen af mængderne i p er tomme.

2. Alle mængderne i p er indbyrdes disjunkte.

3. Foreningsmængden af alle mængderne i p er lig med bs.

Den formelle version af denne definition ser således ud:

[Partition(p, bs) ¨= (∀s: (s ∈ p ⇒ s ≠ Ø)) ˙∧ (∀s, t: (s ∈ p ⇒ t ∈ p ⇒ s ≠ t ⇒ s ∩ t =Ø)) ˙∧ ∪ p=bs]

Vi kan nu formulere hovedresultatet som et formelt lemma (hvor vi bruger objektvariable):

[ZFsub lemma EqSysIsPartition: EqRel(r, OBS) ⊢ Partition(OBS/r, OBS)]

Formålet med resten af rapporten er at bevise EqSysIsPartition.

6 Udsagnslogisk bibliotek

I dette afsnit vil jeg bevise en samling af udsagnslogiske sandheder ( eller “tautologier”), som vil blive brugt i de følgende afsnit. De fleste af disse tautologier har mange andre anvendelser end lige netop mængdelære. Beviserne er fordelt på syv underafsnit; figur 1 giver et overblik over, hvordan beviserne forholder sig til hinanden. Jeg vil kommentere de fleste af beviserne; dog er nogle af dem så tekniske, at jeg har ladet dem stå alene.

Figur 1: Bevisstrukturen for tautologierne. En pil fra lemma x til lemma y betyder, at x bruges i beviset for y. MP-lemmaerne fra afsnit 6.1 er ikke vist. “ImpTrans” står for “ImplyTransitivity”.

6.1 MP-lemmaer

Man får ofte brug for at anvende slutningsreglen MP flere gange i træk. Derfor vil jeg begynde med at vise fire lemmaer, der kan klare mellem 2 og 5 anvendelser af MP^{15}:

[ZFsub lemma MP2: ΠA, B, C: A ⇒ B ⇒ C ⊢ A ⊢ B ⊢ C]

[ZFsub lemma MP3: ΠA, B, C, D: A ⇒ B ⇒ C ⇒ D ⊢ A ⊢ B ⊢ C ⊢ D]

[ZFsub lemma MP4: ΠA, B, C, D, E: A ⇒ B ⇒ C ⇒ D ⇒ E ⊢ A ⊢ B ⊢ C ⊢ D ⊢ E]

[ZFsub lemma MP5: ΠA, B, C, D, E, F: A ⇒ B ⇒ C ⇒ D ⇒ E ⇒ F ⊢ A ⊢ B ⊢ C ⊢ D ⊢ E ⊢ F]

6.1.1 Det første bevis

Vi begynder med at bevise MP2:

[ZFsub lemma MP2: ΠA, B, C: A ⇒ B ⇒ C ⊢ A ⊢ B ⊢ C]

ZFsub proof of MP2:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A ⇒ B ⇒ C  ;
L03: Premise ≫  A  ;
L04: Premise ≫  B  ;
L05: MP ⊳ L02 ⊳ L03 ≫  B ⇒ C  ;
L06: MP ⊳ L05 ⊳ L04 ≫  C  □

Da dette er rapportens første bevis, vil jeg bringe nogle ekstra kommentarer^{16}. 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 MP2 består af seks linier, nummereret fra 1 til 6. 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 5, at meta-formlen [B ⇒ C] gælder, fordi den kan udledes fra slutningsreglen MP ved substitution. Argumentationen skal læses på den måde, at konklusionerne fra linie 2 og 3 bliver brugt som præmisser til MP. Den generelle betydning af konstruktionen [x ⊳ y] er, at konklusionen fra linie y bliver brugt som præmis i forhold til x.

Den anden form, en bevislinie kan have, er:

     Nøgleord ≫ Konklusion

15I afsnit 8.3 får vi faktisk brug for at anvende MP 6 gange i træk; men et eller andet sted skal man jo stoppe.

16Denne beskrivelse er en revideret udgave af afsnit 5.1 i [1].

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 sætning, der skal bevises. F.eks. siger bevisets linie 2, at MP2 bruger meta-formlen [A ⇒ B ⇒ C] som præmis. Når ordet “Arbitrary” bruges, består konklusionen af en liste af meta-variable (f.eks. [A, B, C] i linie 1). Ideen hermed er at udtrykke, at vi ikke antager noget om de pågældende meta-variable, og at vi derfor har ret til at binde dem med en meta-alkvantor i den sætning, der skal bevises. I det forhåndenværende bevis berettiger linien med “Arbitrary” altså, at MP2 er kvantificeret med [ΠA, B, C: (⋯)].

Alt dette har drejet sig om den formelle syntaks for et Logiweb bevis. Der er ikke så meget at sige om selve beviset for MP2; vi indkapsler simpelthen to på hinanden følgende anvendelser af MP.

6.1.2 Beviser for de andre MP-lemmaer

Beviserne for de øvrige MP-lemmaer er lige ud ad landevejen:

[ZFsub lemma MP3: ΠA, B, C, D: A ⇒ B ⇒ C ⇒ D ⊢ A ⊢ B ⊢ C ⊢ D]

ZFsub proof of MP3:

L01: Arbitrary ≫  A, B, C, D  ;
L02: Premise ≫  A ⇒ B ⇒ C ⇒ D  ;
L03: Premise ≫  A  ;
L04: Premise ≫  B  ;
L05: Premise ≫  C  ;
L06: MP2 ⊳ L02 ⊳ L03 ⊳ L04 ≫  C ⇒ D  ;
L07: MP ⊳ L06 ⊳ L05 ≫  D  □

[ZFsub lemma MP4: ΠA, B, C, D, E: A ⇒ B ⇒ C ⇒ D ⇒ E ⊢ A ⊢ B ⊢ C ⊢ D ⊢ E]

ZFsub proof of MP4:

L01: Arbitrary ≫  A, B, C, D, E  ;
L02: Premise ≫  A ⇒ B ⇒ C ⇒ D ⇒ E  ;
L03: Premise ≫  A  ;
L04: Premise ≫  B  ;
L05: Premise ≫  C  ;
L06: Premise ≫  D  ;
L07: MP2 ⊳ L02 ⊳ L03 ⊳ L04 ≫  C ⇒ D ⇒ E  ;
L08: MP2 ⊳ L07 ⊳ L05 ⊳ L06 ≫  E  □

[ZFsub lemma MP5: ΠA, B, C, D, E, F: A ⇒ B ⇒ C ⇒ D ⇒ E ⇒ F ⊢ A ⊢ B ⊢ C ⊢ D ⊢ E ⊢ F]

ZFsub proof of MP5:

L01: Arbitrary ≫  A, B, C, D, E, F  ;
L02: Premise ≫  A ⇒ B ⇒ C ⇒ D ⇒ E ⇒ F  ;
L03: Premise ≫  A  ;

L04: Premise ≫  B  ;
L05: Premise ≫  C  ;
L06: Premise ≫  D  ;
L07: Premise ≫  E  ;
L08: MP3⊳L02⊳L03⊳L04⊳L05 ≫ D ⇒ E ⇒ F  ;
L09: MP2 ⊳ L08 ⊳ L06 ⊳ L07 ≫  F  □

6.2 Implikation

Dette afsnit indeholder en række lemmaer vedr. implikation, grupperet i fire under-underafsnit.

6.2.1 Refleksivitet; blok-konstruktionen

Lemmaet AutoImply udsiger, at implikations-relationen er refleksiv:

[ZFsub lemma AutoImply: ΠA: A ⇒ A]

ZFsub proof of AutoImply:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A  ;
L03: Premise ≫  A  ;
L04: Repetition ⊳ L03 ≫  A  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  A  ;
L07: Ded ⊳ L05 ≫  A ⇒ A  □

Beviset for AutoImply indeholder to nye ting i forhold til de hidtidige beviser: En bevisblok, og en anvendelse af deduktions-reglen. En bevisblok er selvstændig enhed i et bevis; den afhænger ikke af den øvrige del af beviset. Den ovenstående bevisblok indeholder et bevis for lemmaet [ΠA: A ⊢ A]. Pointen er nu, at blokkens sidste linie (linie 5) fungerer som en forkortelse for dette lemma. Vi kan da anvende deduktionsreglen på denne linie til at omdanne inferensen [ΠA: A ⊢ A] til implikationen [A ⇒ A]. Det vigtigste formål med deduktionsreglen er netop, at vi let kan skifte fra inferens til implikation.

6.2.2 Transitivitet

Lemmaet ImplyTransitivity udsiger, at implikations-relationen er transitiv:

[ZFsub lemma ImplyTransitivity: ΠA, B, C: A ⇒ B ⊢ B ⇒ C ⊢ A ⇒ C]

Vi viser ImplyTransitivity ved hjælp af MP og deduktionsreglen:

ZFsub proof of ImplyTransitivity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B, C  ;
L03: Premise ≫  A ⇒ B  ;

L04: Premise ≫  B ⇒ C  ;
L05: Premise ≫  A  ;
L06: MP ⊳ L03 ⊳ L05 ≫  B  ;
L07: MP ⊳ L04 ⊳ L06 ≫  C  ;
L08: Block ≫  End  ;
L09: Arbitrary ≫  A, B, C  ;
L10: Premise ≫  A ⇒ B  ;
L11: Premise ≫  B ⇒ C  ;
L12: Ded ⊳ L08 ≫  (A ⇒ B) ⇒ (B ⇒ C) ⇒ A ⇒ C ;
L13: MP2 ⊳ L12 ⊳ L10 ⊳ L11 ≫  A ⇒ C  □

6.2.3 Svækkelse

Vi får ofte brug for det følgende ræsonnement: Hvis formlen A gælder ubetinget, så gælder den også under antagelse af en vilkårlig anden formel B. Lemmaet Weakening udtrykker dette ræsonnement som følger:

[ZFsub lemma Weakening: ΠA, B: B ⊢ A ⇒ B]

Vi beviser Weakening ved hjælp af deduktionsreglen:

ZFsub proof of Weakening:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  B  ;
L04: Premise ≫  A  ;
L05: Repetition ⊳ L03 ≫  B  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Ded ⊳ L06 ≫  B ⇒ A ⇒ B  ;
L09: Premise ≫  B  ;
L10: MP ⊳ L08 ⊳ L09 ≫  A ⇒ B  □

6.2.4 Modsigelse

Det sidste lemma i dette afsnit vedrører strengt taget ikke implikation, men derimod inferens (x ⊢ y). Lemmaet FromContradiction udsiger, at vi kan bevise hvad som helst, hvis vi har bevist to formler, der modsiger hinanden:

[ZFsub lemma FromContradiction: ΠA, B: A ⊢ ˙¬ A ⊢ B]

Beviset bruger Weakening og slutningsreglen Neg:

ZFsub proof of FromContradiction:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A  ;
L03: Premise ≫  ˙¬ A  ;
L04: Weakening ⊳ L02 ≫  ˙¬ B ⇒ A  ;

L05: Weakening ⊳ L03 ≫  ˙¬ B ⇒ ˙¬ A  ;
L06: Neg ⊳ L04 ⊳ L05 ≫  B  □

6.3 Håndtering af dobbeltnegationer

De to lemmaer RemoveDoubleNeg og AddDoubleNeg tillader os hhv. at fjerne og tilføje dobbeltnegationer. Jeg vil ikke kommentere beviserne: [ZFsub lemma RemoveDoubleNeg: ΠA: ˙¬ ˙¬ A ⊢ A] ZFsub proof of RemoveDoubleNeg:

L01: Arbitrary ≫  A  ;
L02: Premise ≫  ˙¬ ˙¬ A  ;
L03: Weakening ⊳ L02 ≫  ˙¬ A ⇒ ˙¬ ˙¬ A  ;
L04: AutoImply ≫  ˙¬ A ⇒ ˙¬ A  ;
L05: Neg ⊳ L04 ⊳ L03 ≫  A  □

[ZFsub lemma AddDoubleNeg: ΠA: A ⊢ ˙¬ ˙¬ A] ZFsub proof of AddDoubleNeg:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A  ;
L03: Premise ≫  ˙¬ ˙¬ ˙¬ A  ;
L04: RemoveDoubleNeg ⊳ L03 ≫  ˙¬ A  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  A  ;
L07: Ded ⊳ L05 ≫  ˙¬ ˙¬ ˙¬ A ⇒ ˙¬ A  ;
L08: Premise ≫  A  ;
L09: Weakening ⊳ L08 ≫  ˙¬ ˙¬ ˙¬ A ⇒ A  ;
L10: Neg ⊳ L09 ⊳ L07 ≫  ˙¬ ˙¬ A  □

6.4 Modus tollens og beslægtede lemmaer

Hovedresultatet fra dette afsnit er slutningsreglen modus tollens, bevist som et lemma: [ZFsub lemma MT: ΠA, B: A ⇒ B ⊢ ˙¬ B ⊢ ˙¬ A] For at vise MT begynder vi med et teknisk lemma, der ikke har den store værdi i sig selv: [ZFsub lemma Technicality: ΠA, B: A ⇒ B ⊢ ˙¬ ˙¬ A ⇒ B] ZFsub proof of Technicality:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A ⇒ B  ;
L04: Premise ≫  ˙¬ ˙¬ A  ;

L05: RemoveDoubleNeg ⊳ L04 ≫  A  ;
L06: MP ⊳ L03 ⊳ L05 ≫  B  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  A, B  ;
L09: Ded ⊳ L07 ≫  (A ⇒ B) ⇒ ˙¬ ˙¬ A ⇒ B  ;
L10: Premise ≫  A ⇒ B  ;
L11: MP ⊳ L09 ⊳ L10 ≫  ˙¬ ˙¬ A ⇒ B  □

Uafhængigt af Technicality kan vi vise en version af MT, hvor A optræder i negeret form: [ZFsub lemma NegativeMT: ΠA, B: ˙¬ A ⇒ B ⊢ ˙¬ B ⊢ A] ZFsub proof of NegativeMT:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  ˙¬ A ⇒ B  ;
L03: Premise ≫  ˙¬ B  ;
L04: Weakening ⊳ L03 ≫  ˙¬ A ⇒ ˙¬ B  ;
L05: Neg ⊳ L02 ⊳ L04 ≫  A  □

Ud fra Technicality og NegativeMT kan vi nu vise MT: [ZFsub lemma MT: ΠA, B: A ⇒ B ⊢ ˙¬ B ⊢ ˙¬ A] ZFsub proof of MT:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ⇒ B  ;
L03: Premise ≫  ˙¬ B  ;
L04: Technicality ≫  ˙¬ ˙¬ A ⇒ B  ;
L05: NegativeMT ⊳ L04 ⊳ L03 ≫  ˙¬ A  □

Vi slutter dette underafsnit med en variant af MT, som erstatter en inferens med en implikation: [ZFsub lemma Contrapositive: ΠA, B: A ⇒ B ⊢ ˙¬ B ⇒ ˙¬ A] Når en inferens skal erstattes med en implikation, er det altid deduktionsreglen, der skal i spil: ZFsub proof of Contrapositive:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A ⇒ B  ;
L04: Premise ≫  ˙¬ B  ;
L05: MT ⊳ L03 ⊳ L04 ≫  ˙¬ A  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Premise ≫  A ⇒ B  ;

L09: Ded ⊳ L06 ≫  (A ⇒ B) ⇒ ˙¬ B ⇒ ˙¬ A  ;
L10: MP ⊳ L09 ⊳ L08 ≫  ˙¬ B ⇒ ˙¬ A  □

6.5 Konjunktion

Hovedmålet med dette underafsnit er at konvertere mellem formlerne A og B og deres konjunktion [A ˙∧ B].

6.5.1 Forening af konjunkter

Vi begynder med at slå A og B sammen til [A ˙∧ B]:

[ZFsub lemma JoinConjuncts: ΠA, B: A ⊢ B ⊢ A ˙∧ B]

Beviset for JoinConjuncts er af teknisk karakter. Vi viser den makroekspanderede form [ ˙¬ (A ⇒ ˙¬ B)], som vi i bevisets sidste linie konverterer til [A ˙∧ B]. Denne sidste linie er ikke nødvendig for bevischeckeren, men den gør beviset lidt nemmere at læse:

ZFsub proof of JoinConjuncts:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A  ;
L04: Premise ≫  A ⇒ ˙¬ B  ;
L05: MP ⊳ L04 ⊳ L03 ≫  ˙¬ B  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Ded ⊳ L06 ≫  A ⇒ (A ⇒ ˙¬ B) ⇒ ˙¬ B  ;
L09: Premise ≫  A  ;
L10: Premise ≫  B  ;
L11: MP ⊳ L08 ⊳ L09 ≫  (A ⇒ ˙¬ B) ⇒ ˙¬ B  ;
L12: AddDoubleNeg ⊳ L10 ≫  ˙¬ ˙¬ B  ;
L13: MT ⊳ L11 ⊳ L12 ≫  ˙¬ (A ⇒ ˙¬ B)  ;
L14: Repetition ⊳ L13 ≫  A ˙∧ B  □

6.5.2 Udskilning af anden konjunkt

Tautologien SecondConjunct lader os udskille den anden konjunkt fra [A ˙∧ B]. Jeg vil ikke kommentere beviset:

[ZFsub lemma SecondConjunct: ΠA, B: A ˙∧ B ⊢ B]

ZFsub proof of SecondConjunct:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  ˙¬ B  ;
L04: Weakening ⊳ L03 ≫  A ⇒ ˙¬ B  ;
L05: Block ≫  End  ;

L06: Arbitrary ≫  A, B  ;
L07: Ded ⊳ L05 ≫  ˙¬ B ⇒ A ⇒ ˙¬ B  ;
L08: Premise ≫  A ˙∧ B  ;
L09: Repetition ⊳ L08 ≫  ˙¬ (A ⇒ ˙¬ B)  ;
L10: NegativeMT ⊳ L07 ⊳ L09 ≫  B  □

6.5.3 Udskilning af første konjunkt

For at udskille A fra [A ˙∧ B] viser vi først, at [A ˙∧ B] er kommutativ. Jeg vil ikke kommentere beviset:

[ZFsub lemma AndCommutativity: ΠA, B: A ˙∧ B ⊢ B ˙∧ A]

ZFsub proof of AndCommutativity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  B ⇒ ˙¬ A  ;
L04: Premise ≫  A  ;
L05: AddDoubleNeg ⊳ L04 ≫  ˙¬ ˙¬ A  ;
L06: MT ⊳ L03 ⊳ L05 ≫  ˙¬ B  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  A, B  ;
L09: Ded ⊳ L07 ≫  (B ⇒ ˙¬ A) ⇒ A ⇒ ˙¬ B  ;
L10: Premise ≫  A ˙∧ B  ;
L11: Repetition ≫  ˙¬ (A ⇒ ˙¬ B)  ;
L12: MT ⊳ L09 ⊳ L11 ≫  ˙¬ (B ⇒ ˙¬ A)  ;
L13: Repetition ⊳ L12 ≫  B ˙∧ A  □

Nu er det let at udskille den første konjunkt fra [A ˙∧ B]: Først vender vi konjunktionen om til [B ˙∧ A] ved hjælp af AndCommutativity, og så udskiller vi A ved hjælp af SecondConjunct:

[ZFsub lemma FirstConjunct: ΠA, B: A ˙∧ B ⊢ A]

ZFsub proof of FirstConjunct:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙∧ B  ;
L03: AndCommutativity ⊳ L02 ≫  B ˙∧ A  ;
L04: SecondConjunct ⊳ L03 ≫  A  □

6.6 Dobbeltimplikation

I dette underafsnit viser vi tre enkle resultater vedr. dobbeltimplikation.

6.6.1 Brug sammen med modus ponens

De følgende to tautologier gør det let at bruge anvende slutningsreglen MP på dobbeltimplikationer. Beviserne er enkle og kræver ingen kommentarer:

[ZFsub lemma IffFirst: ΠA, B: A ˙⇔ B ⊢ B ⊢ A] ZFsub proof of IffFirst:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙⇔ B  ;
L03: Premise ≫  B  ;
L04: SecondConjunct ⊳ L02 ≫  B ⇒ A  ;
L05: MP ⊳ L04 ⊳ L03 ≫  A  □

[ZFsub lemma IffSecond: ΠA, B: A ˙⇔ B ⊢ A ⊢ B] ZFsub proof of IffSecond:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙⇔ B  ;
L03: Premise ≫  A  ;
L04: FirstConjunct ⊳ L02 ≫  A ⇒ B  ;
L05: MP ⊳ L04 ⊳ L03 ≫  B  □

6.6.2 Kommutativitet Lemmaet IffCommutativity følger direkte af, at operatoren [x ˙∧ y] er kommutativ: [ZFsub lemma IffCommutativity: ΠA, B: A ˙⇔ B ⊢ B ˙⇔ A] ZFsub proof of IffCommutativity:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙⇔ B  ;
L03: Repetition ⊳ L02 ≫  (A ⇒ B) ˙∧ (B ⇒ A)  ;
L04: AndCommutativity ⊳ L03 ≫  (B ⇒ A) ˙∧ (A ⇒ B)  ;
L05: Repetition ⊳ L04 ≫  B ˙⇔ A  □

6.7 Disjunktion

Dette underafsnit indeholder tre lemmaer vedr. disjunktion, som vi fordeler på to under-underafsnit. 6.7.1 Svækkelse Givet en påstand B vil vi gerne udlede de svagere påstande [A ˙∨ B] og [B ˙∨ A]. Den første slutning varetages af lemmaet WeakenOr1: [ZFsub lemma WeakenOr1: ΠA, B: B ⊢ A ˙∨ B] Beviset består af en simpel anvendelse af Weakening: ZFsub proof of WeakenOr1:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  B  ;

L03: Weakening ⊳ L02 ≫  ˙¬ A ⇒ B  ;
L04: Repetition ⊳ L03 ≫  A ˙∨ B  □

Slutningen fra A til [A ˙∨ B] varetages af lemmaet WeakenOr2: [ZFsub lemma WeakenOr2: ΠA, B: A ⊢ A ˙∨ B] Kernen i beviset for WeakenOr2 er en anvendelse af FromContradiction: ZFsub proof of WeakenOr2:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A  ;
L04: Premise ≫  ˙¬ A  ;

L05: FromContradiction ⊳ L03 ⊳

L04 ≫ B ;

L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Ded ⊳ L06 ≫  A ⇒ ˙¬ A ⇒ B  ;
L09: Premise ≫  A  ;
L10: MP ⊳ L08 ⊳ L09 ≫  ˙¬ A ⇒ B  ;
L11: Repetition ⊳ L10 ≫  A ˙∨ B  □

6.7.2 Slutning ud fra disjunktion Lemmaet FromDisjuncts lader os drage slutninger ud fra en disjunktion: [ZFsub lemma FromDisjuncts: ΠA, B, C: A ˙∨ B ⊢ A ⇒ C ⊢ B ⇒ C ⊢ C] Om beviset vil jeg kun sige, at det er en ret elegant øvelse i bevisteknik: ZFsub proof of FromDisjuncts:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A ˙∨ B  ;
L03: Premise ≫  A ⇒ C  ;
L04: Premise ≫  B ⇒ C  ;
L05: Repetition ⊳ L02 ≫  ˙¬ A ⇒ B  ;
L06: Contrapositive ⊳ L05 ≫  ˙¬ B ⇒ ˙¬ ˙¬ A  ;
L07: Technicality ⊳ L03 ≫  ˙¬ ˙¬ A ⇒ C  ;
L08: ImplyTransitivity⊳L06⊳L07 ≫ ˙¬ B ⇒ C  ;
L09: Contrapositive ⊳ L08 ≫  ˙¬ C ⇒ ˙¬ ˙¬ B  ;
L10: Contrapositive ⊳ L04 ≫  ˙¬ C ⇒ ˙¬ B  ;
L11: Neg ⊳ L10 ⊳ L09 ≫  C  □

7 Regellemaer

Alle aksiomerne i afsnit 4.2 er formuleret som dobbeltimplikationer. Dette er gjort for at holde antallet af aksiomer nede på et minimum; men når aksiomerne skal bruges i beviser, er det mere bekvemt at have regler af formen [A ⊢ B] til rådighed. Heldigvis kan vi altid bevise [A ⊢ B], hvis vi i forvejen har et bevis for [A ⇒ B] — der kræves blot en rutinemæssig anvendelse af MP.

I dette afsnit viser vi regellemmaer svarende til aksiomerne SeparationDef, PairDef, UnionDef, PowerDef og Extensionality.

7.1 Par

I tilfældet “PairDef” forløber både definition og bevis af regellemmaerne så enkelt, som det er muligt. Først formulerer vi den ene halvdel af aksiomets dobbelt-implikation som et lemma:

[ZFsub lemma Pair2Formula: ΠS, X , Y: S ∈ {X , Y} ⊢ S =X ˙∨ S =Y]

Derefter beviser vi dette lemma ved at anvende IffSecond på aksiomet og præmissen:

ZFsub proof of Pair2Formula:

L01: Arbitrary ≫  S, X , Y  ;
L02: Premise ≫  S ∈ {X , Y}  ;
L03: PairDef ≫  S ∈ {X , Y} ˙⇔ S =X ˙∨ S =Y  ;
L04: IffSecond ⊳ L03 ⊳ L02 ≫  S =X ˙∨ S =Y  □

Til sidst gentager vi hele processen mht. den anden halvdel af dobbeltimplikationen. Den eneste reelle forskel er, at vi bruger IffFirst i beviset (i stedet for IffSecond):

[ZFsub lemma Formula2Pair: ΠS, X , Y: S =X ˙∨ S =Y ⊢ S ∈ {X , Y}]

ZFsub proof of Formula2Pair:

L01: Arbitrary ≫  S, X , Y  ;
L02: Premise ≫  S =X ˙∨ S =Y  ;
L03: PairDef ≫  S ∈ {X , Y} ˙⇔ S =X ˙∨ S =Y  ;
L04: IffFirst ⊳ L03 ⊳ L02 ≫  S ∈ {X , Y}  □

7.2 Foreningsmængde

I tilfældet “UnionDef” bruger vi stort set den samme fremgangsmåde som i afsnit 7.1. Først håndterer vi den ene halvdel af dobbeltimplikationen:

[ZFsub lemma Union2Formula: ΠS, X: S ∈ ∪X ⊢ S ∈ Ex_{10} ˙∧ Ex_{10} ∈ X]

ZFsub proof of Union2Formula:

L01: Arbitrary ≫  S, X  ;

L02: Premise ≫  S ∈ ∪X  ;
L03: UnionDef ≫  {S ∈ ∪X ˙⇔ \atop (S ∈ Ex_{10} ˙∧ Ex_{10} ∈ X)  ;}
L04: IffSecond ⊳ L03 ⊳ L02 ≫  S ∈ Ex_{10} ˙∧ Ex_{10} ∈ X  □

Så er turen kommet til den anden halvdel af dobbeltimplikationen:

[ZFsub lemma Formula2Union: ΠS, X: S ∈ Ex_{10} ⊢ Ex_{10} ∈ X ⊢ S ∈ ∪X]

Der er det lille raffinement, at vi i formuleringen af Formula2Union har delt formlen [S ∈ Ex_{10} ˙∧ Ex_{10} ∈ X] op i sine konjunkter. Beviset for Formula2Union kræver derfor en ekstra anvendelse af JoinConjuncts:

ZFsub proof of Formula2Union:

L01: Arbitrary ≫  S, X  ;
L02: Premise ≫  S ∈ Ex_{10}  ;
L03: Premise ≫  Ex_{10} ∈ X  ;
L04: JoinConjuncts ⊳ L02 ⊳ L03 ≫ S ∈ Ex_{10} ˙∧ Ex_{10} ∈ X  ;
L05: UnionDef ≫  {S ∈ ∪X ˙⇔ \atop (S ∈ Ex_{10} ˙∧ Ex_{10} ∈ X)  ;}
L06: IffFirst ⊳ L05 ⊳ L04 ≫  S ∈ ∪X  □

7.3 Potensmængde; sidebetingelser

Tilfældet “PowerDef” er mere kompliceret end de hidtidige tilfælde. Det ene af de to regellemmaer er nemt nok:

[ZFsub lemma SubsetInPower: ΠS, X: S ⊆ X ⊢ S ∈ P(X)]

ZFsub proof of SubsetInPower:

L01: Arbitrary ≫  S, X  ;
L02: Premise ≫  s ∈ S ⇒ s ∈ X  ;
L03: Gen ⊳ L02 ≫  ∀s: (s ∈ S ⇒ s ∈ X)  ;
L04: PowerDef ≫  {S ∈ P(X) ˙⇔ \atop ∀s: (s ∈ S ⇒ s ∈ X)  ;}
L05: IffFirst ⊳ L04 ⊳ L03 ≫  S ∈ P(X)  □

Det andet regellemma er også nemt, hvis vi nøjes med at vise:

[ΠS, X: S ∈ P(X) ⊢ ∀s: (s ∈ S ⇒ s ∈ X)]. For at komme videre med konklusionen [∀s: s ∈ S ⇒ s ∈ X] må vi imidlertid slippe af med objektkvantoren; og dette kan vi lige så godt gøre med det samme. Derfor bliver målet i stedet at vise:

[ΠS, X: S ∈ P(X) ⊢ S ⊆ X], hvor S ⊆ X som nævnt i afsnit 5.3 er en forkortelse for [s ∈ S ⇒ s ∈ X].

For at nå dette mål må vi begynde med et hjælpelemma, der ser således ud:

[ZFsub lemma HelperPowerIsSub: ΠS, X , Y: s#X ⊢⊢ s#Y ⊢⊢ ∀s: (s ∈ X ⇒ s ∈ Y) ⇒ S ∈ X ⇒ S ∈ Y] De to sidebetingelser [s#X] og [s#Y] er her nødvendige pga. antecedenten^{17} [∀s: (s ∈ X ⇒ s ∈ Y)]. Hvis vi i denne formel instantierer X eller Y til en term, der indeholder frie forekomster af s, så ændres formlens mening. F.eks. er formlen [∀s: (s ∈ s ⇒ s ∈ y)] nødvendigvis sand, fordi ingen mængder i ZFsub er medlem af sig selv; men den oprindelige formel [∀s: (s ∈ X ⇒ s ∈ Y)] er ikke nødvendigvis sand. Konstruktionen [x#y] (der er defineret i appendikset til [4]) udsiger netop, at objektvariablen x ikke forekommer frit i termen y^{18}. Vi kommer til at se mange flere eksempler på sidebetingelser af formen [x#y]: De er nødvendige, når metavariablen y optræder i en kontekst, der er kvantificeret med objektvariablen x.

Indholdet af selve lemmaet er, at vi kan fjerne objektkvantoren fra [∀s: (s ∈ X ⇒ s ∈ Y)], og endda erstatte objektvariablen s med metavariablen S. Her er beviset:

ZFsub proof of HelperPowerIsSub:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  s ∈ X ⇒ s ∈ Y  ;
L04: Repetition ⊳ L03 ≫  s ∈ X ⇒ s ∈ Y  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  S, X , Y  ;
L07: Ded ⊳ L05 ≫  {s#X ⊢⊢ s#Y ⊢⊢ ∀s: (s ∈ X ⇒ \atop s ∈ Y) ⇒ S ∈ X ⇒ S ∈ Y  □}

Beviset illustrerer styrken af slutningsreglen Ded: I dette tilfælde omdanner den en inferens (nemlig [ΠX , Y: s ∈ X ⇒ s ∈ Y ⊢ s ∈ X ⇒ s ∈ Y]) til en implikation (nemlig [(s ∈ X ⇒ s ∈ Y) ⇒ s ∈ X ⇒ s ∈ Y]), sætter en alkvantor på antecedenten (så vi får [∀s: (s ∈ X ⇒ s ∈ Y) ⇒ s ∈ X ⇒ s ∈ Y]), og erstatter den frie forekomst af “s” med “S” — alt sammen på én gang. Dog skal de to sidebetingelser med, for at reglen kan anvendes.

Formuleringen af det andet regellemma bliver nu som følger:

[ZFsub lemma PowerIsSub: ΠS, X: s#S ⊢⊢ s#X ⊢⊢ S ∈ P(X) ⊢ S ⊆ X]

Da PowerIsSub benytter sig af HelperPowerIsSub, bliver vi nødt til at lade PowerIsSub “arve” de to sidebetingelser fra dette lemma. Vi kan ikke undgå sidebetingelserne ved at instantiere de to metavariable X og Y fra HelperPowerIsSub til nogle andre metavariable; for der er jo ingen garanti for, at disse metavariable vil undgå s, når de engang bliver instantierede. Så længe man arbejder med metavariable, er det altså meget svært at slippe af med denne slags sidebetingelser, når de først er blevet indført i en beviskæde.

Her er beviset for PowerIsSub:

ZFsub proof of PowerIsSub:

L01: Arbitrary ≫  S, X  ;

17Jeg kalder x i [x ⇒ y] for “antecedenten”; og jeg kalder y for “konsekvensen”.

18Vi siger at “x undgår y” (eller at “y undgår x”).

L02: Side-condition ≫  s#S  ;
L03: Side-condition ≫  s#X  ;
L04: Premise ≫  S ∈ P(X)  ;
L05: PowerDef ≫  {S ∈ P(X) ˙⇔ \atop ∀s: (s ∈ S ⇒ s ∈ X)  ;}
L06: IffSecond ⊳ L05 ⊳ L04 ≫  ∀s: (s ∈ S ⇒ s ∈ X)  ;

L07: HelperPowerIsSub ⊳ ⊳ L02 ⊳ ⊳

L03 ≫ ∀s: (s ∈ S ⇒ s ∈ X) ⇒ s ∈ S ⇒ s ∈ X ;

L08: MP ⊳ L07 ⊳ L06 ≫  s ∈ S ⇒ s ∈ X  ;
L09: Repetition ⊳ L08 ≫  S ⊆ X  □

I linie 7 benytter vi konstruktionen [x ⊳ ⊳ y] til at fortælle bevischeckeren, at de to sidebetingelser er opfyldt, og at vi derfor kan anvende HelperPowerIsSub.

7.4 Potensmængde, variant

Som nævnt er det svært at slippe af med sidebetingelser, men af og til kan det lade sig gøre. Når vi i afsnit 11.3.2 gør brug af lemmaerne HelperPowerIsSub og PowerIsSub, vil metavariablen X f.eks. blive instantieret til termer, der undgår s. Hermed bliver sidebetingelsen [s#X] automatisk opfyldt, mens vi stadigvæk må medregne [s#Y] eksplicit. Imidlertid er bevischeckeren således indrettet, at de automatisk opfyldte sidebetingelser skal stå til sidst, når man bruger et lemma, der indeholder sidebetingelser. Derfor viser vi nu nogle varianter af PowerIsSub og HelperPowerIsSub, hvor der er byttet om på [s#X] og [s#Y]:

[ZFsub lemma (Switch)HelperPowerIsSub: ΠS, X , Y: s#Y ⊢⊢ s#X ⊢⊢ ∀s: (s ∈ X ⇒ s ∈ Y) ⇒ S ∈ X ⇒ S ∈ Y]

ZFsub proof of (Switch)HelperPowerIsSub:

L01: Arbitrary ≫  S, X , Y  ;
L02: Side-condition ≫  s#Y  ;
L03: Side-condition ≫  s#X  ;

L04: HelperPowerIsSub ⊳ ⊳ L03 ⊳ ⊳

L02 ≫ ∀s: (s ∈ X ⇒ s ∈ Y) ⇒ S ∈ X ⇒ S ∈ Y □

[ZFsub lemma (Switch)PowerIsSub: ΠS, X: s#X ⊢⊢ s#S ⊢⊢ S ∈ P(X) ⊢ S ⊆ X]

ZFsub proof of (Switch)PowerIsSub:

L01: Arbitrary ≫  S, X  ;
L02: Side-condition ≫  s#X  ;
L03: Side-condition ≫  s#S  ;
L04: Premise ≫  S ∈ P(X)  ;

L05: PowerIsSub ⊳ ⊳ L03 ⊳ ⊳

L02 ⊳ L04 ≫ S ⊆ X □

Vi kunne naturligvis have sparet noget plads ved at vise disse varianter til at begynde med. Jeg har ikke gjort dette, fordi vi nu har fået illustreret en af ulemperne ved at arbejde med sidebetingelser.

Jeg vil ikke kommentere fænomenet “sidebetingelser af formen [x#y]” yderligere — indtil afsnit 10.4, hvor antallet af sidebetingelser bliver så stort, at det ikke kan ignoreres.

7.5 Separation

Tilfældet “SeparationDef” er næsten lige så enkelt som tilfældet “PairDef” fra afsnit 7.1. Vi skal blot huske at overføre aksiomets sidebetingelse til de to regellemmaer:

[ZFsub lemma Sep2Formula: ΠA, B, P, X , Y: P^{Ph} ∧ ⟨B≡A|P:=Y⟩_{Ph} ⊢⊢ Y ∈ {ph ∈ X | A} ⊢ Y ∈ X ˙∧ B]

ZFsub proof of Sep2Formula:

L01: Arbitrary ≫  A, B, P, X , Y  ;
L02: Side-condition ≫  P^{Ph} ∧ ⟨B≡A|P:=Y⟩_{Ph}  ;
L03: Premise ≫  Y ∈ {ph ∈ X | A}  ;
L04: SeparationDef ⊳ ⊳ L02 ≫  {Y ∈ \{ph ∈ X | A\} ˙⇔ \atop Y ∈ X ˙∧ B  ;}
L05: FirstConjunct ⊳ L04 ≫  {Y ∈ \{ph ∈ X | A\} ⇒ \atop Y ∈ X ˙∧ B  ;}
L06: MP ⊳ L05 ⊳ L03 ≫  Y ∈ X ˙∧ B  □

[ZFsub lemma Formula2Sep: ΠA, B, P, X , Y: P^{Ph} ∧ ⟨B≡A|P:=Y⟩_{Ph} ⊢⊢ Y ∈ X ⊢ B ⊢ Y ∈ {ph ∈ X | A}]

ZFsub proof of Formula2Sep:

L01: Arbitrary ≫  A, B, P, X , Y  ;
L02: Side-condition ≫  P^{Ph} ∧ ⟨B≡A|P:=Y⟩_{Ph}  ;
L03: Premise ≫  Y ∈ X  ;
L04: Premise ≫  B  ;
L05: JoinConjuncts ⊳ L03 ⊳ L04 ≫ Y ∈ X ˙∧ B  ;
L06: SeparationDef ⊳ ⊳ L02 ≫  (Y ∈ {ph ∈ X | A} ⇒ Y ∈ X ˙∧ ; B) ˙∧ (Y ∈ X ˙∧ B ⇒ ; Y ∈ {ph ∈ X | A})  ;

L07: SecondConjunct ⊳ L06 ≫  {Y ∈ X ˙∧ B ⇒ \atop Y ∈ \{ph ∈ X | A\}  ;}
L08: MP ⊳ L07 ⊳ L05 ≫  Y ∈ {ph ∈ X | A}  □

7.6 Ekstentionalitet

Tilfældet “Extensionality” er lidt mere kompliceret end det almindelige tilfælde, fordi vi skal forholde os til objektkvantoren i meta-formlen [X = Y ˙⇔ ∀s: (s ∈ X ˙⇔ s ∈ Y)]. Derfor er der to underafsnit; lemmaerne i underafsnit 7.6.1 er afledt af implikationen [∀s: (s ∈ X ˙⇔ s ∈ Y) ⇒ X = Y], mens lemmaerne i underafsnit 7.6.2 er afledt af den omvendte implikation.

7.6.1 Tilstrækkelig betingelse for lighed

To mængder er lig hinanden, hvis de er hinandens delmængder:

[ZFsub lemma ToSetEquality: ΠX , Y: s ∈ X ⇒ s ∈ Y ⊢ s ∈ Y ⇒ s ∈ X ⊢ X =Y]

Beviset for ToSetEquality er ret enkelt. Vi skal blot huske at sætte en objektkvantor på præmisserne, hvilket gøres med slutningsreglen Gen:

ZFsub proof of ToSetEquality:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  s ∈ X ⇒ s ∈ Y  ;
L03: Premise ≫  s ∈ Y ⇒ s ∈ X  ;
L04: JoinConjuncts ⊳ L02 ⊳ L03 ≫ s ∈ X ˙⇔ s ∈ Y  ;
L05: Gen ⊳ L04 ≫ ∀s: (s ∈ X ˙⇔ s ∈ Y) ;
L06: Extensionality ≫  X =Y ˙⇔ ∀s: (s ∈ X ˙⇔ s ∈ Y) ;
L07: SecondConjunct ⊳ L06 ≫  ∀s: (s ∈ X ˙⇔ s ∈ Y) ⇒ X =Y ;
L08: MP ⊳ L07 ⊳ L05 ≫  X =Y  □

I afsnit 10.1 får vi brug for en version af dette lemma, hvor objektvariablen s er erstattet af en anden objektvariabel (jeg har valgt t). For at vise denne alternative version viser vi først lemmaet HelperToSetEquality(t), som indkapsler en anvendelse af deduktionsreglen:

[ZFsub lemma HelperToSetEquality(t): ΠX , Y: t#X ⊢⊢ t#Y ⊢⊢ ∀t: (t ∈ X ⇒ t ∈ Y) ⇒ (s ∈ X ⇒ s ∈ Y)]

ZFsub proof of HelperToSetEquality(t):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  t ∈ X ⇒ t ∈ Y  ;
L04: Repetition ⊳ L03 ≫  t ∈ X ⇒ t ∈ Y  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  X , Y  ;
L07: Ded ⊳ L05 ≫  {t#X ⊢⊢ t#Y ⊢⊢ ∀t: (t ∈ X ⇒ \atop t ∈ Y) ⇒ (s ∈ X ⇒ s ∈ Y)  □}

Hovedlemmaet hedder ToSetEquality(t):

[ZFsub lemma ToSetEquality(t): ΠX , Y: t#X ⊢⊢ t#Y ⊢⊢ t ∈ X ⇒ t ∈ Y ⊢ t ∈ Y ⇒ t ∈ X ⊢ X =Y]

I beviset herfor kombinerer vi Gen med hjælpelemmaet til at omdanne præmissen [t ∈ X ⇒ t ∈ Y] til [s ∈ X ⇒ s ∈ Y] (linie 6–8). Vi gentager denne procedure mht. præmissen [t ∈ Y ⇒ t ∈ X] (linie 9-11). Vi kan da slutte af med en anvendelse af det oprindelige lemma ToSetEquality (linie 12):

ZFsub proof of ToSetEquality(t):

L01: Arbitrary ≫  X , Y  ;
L02: Side-condition ≫  t#X  ;
L03: Side-condition ≫  t#Y  ;
L04: Premise ≫  t ∈ X ⇒ t ∈ Y  ;
L05: Premise ≫  t ∈ Y ⇒ t ∈ X  ;
L06: Gen ⊳ L04 ≫  ∀t: (t ∈ X ⇒ t ∈ Y)  ;

L07: HelperToSetEquality(t) ⊳ ⊳

L02 ⊳ ⊳ L03 ≫ ∀t: (t ∈ X ⇒ t ∈ Y) ⇒ s ∈ X ⇒ s ∈ Y ;

L08: MP ⊳ L07 ⊳ L06 ≫  s ∈ X ⇒ s ∈ Y  ;
L09: Gen ⊳ L05 ≫  ∀t: (t ∈ Y ⇒ t ∈ X)  ;

L10: HelperToSetEquality(t) ⊳ ⊳

L03 ⊳ ⊳ L02 ≫ ∀t: (t ∈ Y ⇒ t ∈ X) ⇒ s ∈ Y ⇒ s ∈ X ;

L11: MP ⊳ L10 ⊳ L09 ≫  s ∈ Y ⇒ s ∈ X  ;
L12: ToSetEquality ⊳ L08 ⊳ L11 ≫ X =Y  □

Arbejdsfordelingen mellem HelperToSetEquality(t) og ToSetEquality(t) er temmelig ujævn; det meste af arbejdet foregår i beviset for ToSetEquality(t). At der er to lemmaer i stedet for ét, har en teknisk forklaring: Logiwebs bevischecker kan ikke arbejde med konklusioner af formen [x ⊢⊢ y]. Vi kan derfor kun referere til konklusionen [t#X ⊢⊢ t#Y ⊢⊢ (⋯)] ved at lade den være konklusionen på et bevis; og derfor må vi stoppe op, når vi når til linie 7 i HelperToSetEquality(t). Vi vil flere gange senere komme ud for lemmaer, hvis eksistens har denne tekniske forklaring. Jeg vil bruge ordet “lemmastump” om disse lemmaer.

7.6.2 Nødvendig betingelse for lighed

Vi begynder dette underafsnit med et hjælpelemma, som vi bruger til at fjerne objektkvantoren fra Extensionality:

[ZFsub lemma HelperFromSetEquality: ΠS, X , Y: s#X ⊢⊢ s#Y ⊢⊢ ∀s: (s ∈ X ˙⇔ s ∈ Y) ⇒ (S ∈ X ˙⇔ S ∈ Y)]

Beviset for HelperFromSetEquality er en simpel anvendelse af deduktionsreglen:

ZFsub proof of HelperFromSetEquality:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  s ∈ X ˙⇔ s ∈ Y  ;
L04: Repetition ⊳ L03 ≫  s ∈ X ˙⇔ s ∈ Y  ;
L05: Block ≫  End  ;

L06: Arbitrary ≫  S, X , Y  ;
L07: Ded ⊳ L05 ≫  {s#X ⊢⊢ s#Y ⊢⊢ ∀s: (s ∈ X ˙⇔ \atop s ∈ Y) ⇒ (S ∈ X ˙⇔ S ∈ Y)  □}

Hovelemmaet i dette underafsnit udsiger, at hvis X er lig med Y, så er X en delmængde af Y^{19}:

[ZFsub lemma FromSetEquality: ΠS, X , Y: s#X ⊢⊢ s#Y ⊢⊢ X =Y ⊢ S ∈ X ⊢ S ∈ Y]

Beviset er en enkel anvendelse af Extensionality og HelperFromSetEquality:

ZFsub proof of FromSetEquality:

L01: Arbitrary ≫  S, X , Y  ;
L02: Side-condition ≫  s#X  ;
L03: Side-condition ≫  s#Y  ;
L04: Premise ≫  X =Y  ;
L05: Premise ≫  S ∈ X  ;
L06: Extensionality ≫  X =Y ˙⇔ ∀s: (s ∈ X ˙⇔ s ∈ Y) ;
L07: IffSecond ⊳ L06 ⊳ L04 ≫ ∀s: (s ∈ X ˙⇔ s ∈ Y) ;

L08: HelperFromSetEquality ⊳ ⊳

L02 ⊳ ⊳ L03 ≫ ∀s: (s ∈ X ˙⇔ s ∈ Y) ⇒ (S ∈ X ˙⇔ S ∈ Y) ;

L09: MP ⊳ L08 ⊳ L07 ≫  S ∈ X ˙⇔ S ∈ Y  ;
L10: IffSecond ⊳ L09 ⊳ L05 ≫  S ∈ Y  □

8 Definitionslemmaer

Regellemmaerne fra afsnit 7 blev afledt fra aksiomer. Lemmaerne i dette afsnit bliver afledt fra makrodefinitionerne i afsnit 5.7; heraf navnet “definitionslemmaer”. Formålet med definitionslemmaerne er at muliggøre effektiv anvendelse af makrodefinitionerne i beviser.

8.1 Refleksiv relation

Den første definition, vi tager under behandling, er definitionen [ReflRel(R, BS) ¨= ∀s: (s ∈ BS ⇒ R(s, s))]. Vi bruger her en lemmastump ved navn HelperReflexivity, som lader os fjerne objektkvantoren fra denne definitions højreside:

[ZFsub lemma HelperReflexivity: ΠR, S, BS: s#R ⊢⊢ s#BS ⊢⊢ ∀s: (s ∈ BS ⇒ R(s, s)) ⇒ S ∈ BS ⇒ R(S, S)]

Vi viser HelperReflexivity ved hjælp af deduktionsreglen:

19Naturligvis kan man også vise, at hvis X er lig med Y, så er Y en delmængde af X. Det har imidlertid ikke været nødvendigt at bruge dette lemma.

ZFsub proof of HelperReflexivity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, BS  ;
L03: Premise ≫  s ∈ BS ⇒ R(s, s)  ;
L04: Repetition ⊳ L03 ≫  s ∈ BS ⇒ R(s, s)  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  R, S, BS  ;
L07: Ded ⊳ L05 ≫  {s#R ⊢⊢ s#BS ⊢⊢ ∀s: (s ∈ BS ⇒ \atop R(s, s)) ⇒ S ∈ BS ⇒ R(S, S) □}

I hovedlemmaet Reflexivity omdanner vi lemmastumpens implikationer til inferenser:

[ZFsub lemma Reflexivity: ΠR, S, BS: s#R ⊢⊢ s#BS ⊢⊢ ReflRel(R, BS) ⊢ S ∈ BS ⊢ R(S, S)]

ZFsub proof of Reflexivity:

L01: Arbitrary ≫  R, S, BS  ;
L02: Side-condition ≫  s#R  ;
L03: Side-condition ≫  s#BS  ;
L04: Premise ≫  ReflRel(R, BS)  ;
L05: Premise ≫  S ∈ BS  ;

L06: HelperReflexivity ⊳ ⊳ L02 ⊳ ⊳

L03 ≫ ReflRel(R, BS) ⇒ S ∈ BS ⇒ R(S, S) ;

L07: MP2 ⊳ L06 ⊳ L04 ⊳ L05 ≫  R(S, S)  □

Vi skal straks se flere eksempler på netop denne arbejdsdeling mellem lemmastump og hovedlemma.

8.2 Symmetrisk relation

De to lemmaer i dette underafsnit er afledt fra definitionen af “symmetrisk relation” i afsnit 5.7. Fremgangsmåden er den samme som i afsnit 8.1. Lemmaet HelperSymmetry fungerer som lemmastump i forhold til Symmetry:

[ZFsub lemma HelperSymmetry: ΠR, S, T , BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ SymRel(R, BS) ⇒ S ∈ BS ⇒ T ∈ BS ⇒ R(S, T ) ⇒ R(T , S)]

[ZFsub lemma Symmetry: ΠR, S, T , BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ SymRel(R, BS) ⊢ S ∈ BS ⊢ T ∈ BS ⊢ R(S, T ) ⊢ R(T , S)]

Beviset for HelperSymmetry fungerer ligesom beviset for HelperReflexivity fra afsnit 8.1 (dog skriver vi ikke definitionen af SymRel(R, BS) ud):

ZFsub proof of HelperSymmetry:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, BS  ;

L03: Premise ≫  {s ∈ BS ⇒ t ∈ BS ⇒ \atop R(s, t) ⇒ R(t, s)  ;}
L04: Repetition ⊳ L03 ≫  {s ∈ BS ⇒ t ∈ BS ⇒ \atop R(s, t) ⇒ R(t, s)  ;}
L05: Block ≫  End  ;
L06: Arbitrary ≫  R, S, T , BS  ;

L07: Ded ⊳ L05 ≫

s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢
t#BS ⊢⊢ SymRel(R, BS) ⇒
S ∈ BS ⇒ T ∈ BS ⇒
R(S, T ) ⇒ R(T , S) □

I beviset for Symmetry skifter vi fra implikation til inferens:

ZFsub proof of Symmetry:

L01: Arbitrary ≫  R, S, T , BS  ;
L02: Side-condition ≫  s#R  ;
L03: Side-condition ≫  s#BS  ;
L04: Side-condition ≫  t#R  ;
L05: Side-condition ≫  t#BS  ;
L06: Premise ≫  SymRel(R, BS)  ;
L07: Premise ≫  S ∈ BS  ;
L08: Premise ≫  T ∈ BS  ;
L09: Premise ≫  R(S, T )  ;

L10: HelperSymmetry ⊳ ⊳ L02 ⊳ ⊳

L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ≫ SymRel(R, BS) ⇒ S ∈ BS ⇒ T ∈ BS ⇒ R(S, T ) ⇒ R(T , S) ;

L11: MP4 ⊳ L10 ⊳ L06 ⊳ L07 ⊳

L08 ⊳ L09 ≫ R(T , S) □

8.3 Transitiv relation

De to lemmaer i dette underafsnit er afledt fra definitionen af “transitiv relation” i afsnit 5.7. Vi bruger nøjagtig den samme fremgangsmåde som i afsnit 8.1 og 8.2: Lemmastumpen (HelperTransitivity) fjerner definitionens objektkvantor ved hjælp af Ded, og hovedlemmaet (Transitivity) skifter fra implikation til inferens:

[ZFsub lemma HelperTransitivity: ΠR, S, T , U, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ TransRel(R, BS) ⇒ S ∈ BS ⇒ T ∈ BS ⇒ U ∈ BS ⇒ R(S, T ) ⇒ R(T , U) ⇒ R(S, U)]

ZFsub proof of HelperTransitivity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, BS  ;

L03: Premise ≫ s ∈ BS ⇒ t ∈ BS ⇒ u ∈ BS ⇒ R(s, t) ⇒ R(t, u) ⇒ R(s, u) ; L04: Repetition ⊳ L03 ≫

s ∈ BS ⇒ t ∈ BS ⇒
u ∈ BS ⇒ R(s, t) ⇒
R(t, u) ⇒ R(s, u) ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  R, S, T , U, BS  ;

L07: Ded ⊳ L05 ≫

s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢
t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢
TransRel(R, BS) ⇒ S ∈ BS ⇒
T ∈ BS ⇒ U ∈ BS ⇒
R(S, T ) ⇒ R(T , U) ⇒ R(S, U) □

[ZFsub lemma Transitivity: ΠR, S, T , U, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ TransRel(R, BS) ⊢ S ∈ BS ⊢ T ∈ BS ⊢ U ∈ BS ⊢ R(S, T ) ⊢ R(T , U) ⊢ R(S, U)]

ZFsub proof of Transitivity:

L01: Arbitrary ≫  R, S, T , U, BS  ;
L02: Side-condition ≫  s#R  ;
L03: Side-condition ≫  s#BS  ;
L04: Side-condition ≫  t#R  ;
L05: Side-condition ≫  t#BS  ;
L06: Side-condition ≫  u#R  ;
L07: Side-condition ≫  u#BS  ;
L08: Premise ≫  TransRel(R, BS)  ;
L09: Premise ≫  S ∈ BS  ;
L10: Premise ≫  T ∈ BS  ;
L11: Premise ≫  U ∈ BS  ;
L12: Premise ≫  R(S, T )  ;
L13: Premise ≫  R(T , U)  ;

L14: HelperTransitivity ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳ L07 ≫ TransRel(R, BS) ⇒ S ∈ BS ⇒

T ∈ BS ⇒ U ∈ BS ⇒
R(S, T ) ⇒ R(T , U) ⇒ R(S, U) ;

L15: MP5 ⊳ L14 ⊳ L08 ⊳ L09 ⊳

L10 ⊳ L11 ⊳ L12 ≫ R(T , U) ⇒ R(S, U) ;

L16: MP ⊳ L15 ⊳ L13 ≫  R(S, U)  □

8.4 Ækvivalensrelation

De tre lemmaer i dette underafsnit udsiger, at en ækvivalensrelation er hhv. refleksiv, symmetrisk og transitiv. Beviserne er simple; vi anvender et par tautologier på definitionen af EqRel(R, BS) fra afsnit 5.7:

[ZFsub lemma ERisReflexive: ΠR: EqRel(R, BS) ⊢ ReflRel(R, BS)]

ZFsub proof of ERisReflexive:

L01: Arbitrary ≫  R  ;

L02: Premise ≫  EqRel(R, BS)  ;

L03: Repetition ⊳ L02 ≫

ReflRel(R, BS)  ˙∧
SymRel(R, BS)  ˙∧

TransRel(R, BS) ;

L04: FirstConjunct ⊳ L03 ≫

ReflRel(R, BS)  ˙∧
SymRel(R, BS) ;
L05: FirstConjunct ⊳ L04 ≫  ReflRel(R, BS)  □

[ZFsub lemma ERisSymmetric: ΠR: EqRel(R, BS) ⊢ SymRel(R, BS)]

ZFsub proof of ERisSymmetric:

L01: Arbitrary ≫  R  ;
L02: Premise ≫  EqRel(R, BS)  ;

L03: Repetition ⊳ L02 ≫

ReflRel(R, BS)  ˙∧
SymRel(R, BS)  ˙∧

TransRel(R, BS) ;

L04: FirstConjunct ⊳ L03 ≫

ReflRel(R, BS)  ˙∧
SymRel(R, BS) ;
L05: SecondConjunct ⊳ L04 ≫  SymRel(R, BS)  □

[ZFsub lemma ERisTransitive: ΠR: EqRel(R, BS) ⊢ TransRel(R, BS)]

ZFsub proof of ERisTransitive:

L01: Arbitrary ≫  R  ;
L02: Premise ≫  EqRel(R, BS)  ;

L03: Repetition ⊳ L02 ≫

ReflRel(R, BS)  ˙∧
SymRel(R, BS)  ˙∧

TransRel(R, BS) ;

L04: SecondConjunct ⊳ L03 ≫  TransRel(R, BS)  □

9 Basale sætninger i mængdelære

Lemmaerne i dette afsnit er en løs samling af mængdeteoretiske sætninger, som bliver brugt i beviset for hovedresultatet i afsnit 11. Lemmaerne er grupperet efter emne: Underafsnit 9.1 omhandler den tomme mængde, underafsnit 9.2 handler om lighedsrelationen [x = y], og underafsnit 9.3 handler om negeret lighed (x ≠ y). Figur 2 giver et overblik over lemmaerne.

Figur 2: Bevisstrukturen for afsnit 9. Kun lemmaer fra dette afsnit er vist. Tallene i parentes angiver, hvor mange sidebetingelser de forskellige lemmaer indeholder. En pil fra lemma x til lemma y betyder, at x bruges i beviset for y. Tallene ved pilene angiver, hvor mange sidebetingelser y modtager fra x. Hvis der f.eks. står “2 · 4”, betyder det, at x bliver anvendt to gange i beviset for y, begge gange med 4 sidebetingelser. Der er overlap mellem nogle af sidebetingelserne, og lemmaer kan generere deres egne sidebetingelser. Derfor er der ikke nødvendigvis overensstemmelse mellem tallene i parentes og tallene ved lemmaerne.

9.1 Den tomme mængde

Dette underafsnit indeholder 3 lemmaer, der hver har fået sit under-underafsnit. 9.1.1 En delmængde af alle mængder Vi viser først, at den tomme mængde er en delmængde af alle mængder: [ZFsub lemma ØisSubset: ΠS, X: S ∈ Ø ⇒ S ∈ X] Beviset for ØisSubset benytter sig af deduktionsreglen og tautologien FromContradiction: ZFsub proof of ØisSubset:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  S, X  ;
L03: Premise ≫  S ∈ Ø  ;
L04: Ødef ≫  S ∉ Ø  ;

L05: FromContradiction ⊳ L03 ⊳

L04 ≫ S ∈ X ;

L06: Block ≫  End  ;
L07: Arbitrary ≫  S, X  ;
L08: Ded ⊳ L06 ≫  S ∈ Ø ⇒ S ∈ X  □

9.1.2 Der er kun én tom mængde Det næste lemma beviser påstanden “der er kun én tom mængde”. Vi formulerer denne påstand som følger: “Hvis en mængde X ikke har nogen medlemmer, så er X lig med Ø”: [ZFsub lemma UniqueØ: ΠX: s ∉ X ⊢ X =Ø] Vi ved allerede fra lemmaet ØisSubset, at Ø er en delmængde af X. Altså mangler vi blot at vise, at X er en delmængde af Ø. Dette klarer vi med hjælpelemmaet HelperUniqueØ: [ZFsub lemma HelperUniqueØ: ΠS, X: S ∉ X ⊢ S ∈ X ⇒ S ∈ Ø] ZFsub proof of HelperUniqueØ:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  S, X  ;
L03: Premise ≫  S ∉ X  ;
L04: Premise ≫  S ∈ X  ;

L05: FromContradiction ⊳ L04 ⊳

L03 ≫ S ∈ Ø ;

L06: Block ≫  End  ;
L07: Arbitrary ≫  S, X  ;
L08: Ded ⊳ L06 ≫  S ∉ X ⇒ S ∈ X ⇒ S ∈ Ø  ;
L09: Premise ≫  S ∉ X  ;
L10: MP ⊳ L08 ⊳ L09 ≫  S ∈ X ⇒ S ∈ Ø  □

Med HelperUniqueØ til rådighed er det let at vise UniqueØ: [ZFsub lemma UniqueØ: ΠX: s ∉ X ⊢ X =Ø] ZFsub proof of UniqueØ:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  s ∉ X  ;
L03: HelperUniqueØ ⊳ L02 ≫  s ∈ X ⇒ s ∈ Ø  ;
L04: ØisSubset ≫  s ∈ Ø ⇒ s ∈ X  ;
L05: ToSetEquality ⊳ L03 ⊳ L04 ≫ X =Ø  □

9.1.3 Lemmaet “MemberNotØ” Som det sidste resultat i dette underafsnit viser vi, at en mængde, der har et medlem, ikke er lig med den tomme mængde: [ZFsub lemma MemberNotØ: ΠS, X: s#X ⊢⊢ S ∈ X ⊢ X ≠ Ø] Beviset for MemberNotØ kan gengives som følger:

1. “Antag at S tilhører X. Hvis X var lig med Ø, så ville S også tilhøre Ø”.

2. “Men S tilhører ikke Ø. Derfor er X ikke lig med Ø”. Vi viser punkt 1 som lemmastumpen HelperMemberNotØ; herefter gennemfører vi punkt 2 i selve beviset for MemberNotØ: [ZFsub lemma HelperMemberNotØ: ΠS, X: s#X ⊢⊢ S ∈ X ⇒ X =Ø ⇒ S ∈ Ø] ZFsub proof of HelperMemberNotØ:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  S, X  ;
L03: Side-condition ≫  s#X  ;
L04: Premise ≫  S ∈ X  ;
L05: Premise ≫  X =Ø  ;

L06: FromSetEquality ⊳ ⊳

L03 ⊳ L05 ⊳ L04 ≫ S ∈ Ø ;

L07: Block ≫  End  ;
L08: Arbitrary ≫  S, X  ;
L09: Ded ⊳ L07 ≫  {s#X ⊢⊢ \atop S ∈ X ⇒ X =Ø ⇒ S ∈ Ø  □}

[ZFsub lemma MemberNotØ: ΠS, X: s#X ⊢⊢ S ∈ X ⊢ X ≠ Ø] ZFsub proof of MemberNotØ:

L01: Arbitrary ≫  S, X  ;
L02: Side-condition ≫  s#X  ;
L03: Premise ≫  S ∈ X  ;
L04: HelperMemberNotØ ⊳ ⊳ L02 ≫ S ∈ X ⇒ X =Ø ⇒ S ∈ Ø  ;

L05: MP ⊳ L04 ⊳ L03 ≫  X =Ø ⇒ S ∈ Ø  ;
L06: Ødef ≫  S ∉ Ø  ;
L07: MT ⊳ L05 ⊳ L06 ≫  X ≠ Ø  □

9.2 [x=y] er en ækvivalensrelation

Målet med dette underafsnit er at vise, at [x=y] er en refleksiv, symmetrisk og transitiv relation.

At [x=y] er refleksiv, følger af, at [x ⇒ y] er refleksiv: [ZFsub lemma =Reflexivity: ΠS: S =S] ZFsub proof of =Reflexivity:

L01: Arbitrary ≫  S  ;
L02: AutoImply ≫  s ∈ S ⇒ s ∈ S  ;
L03: ToSetEquality ⊳ L02 ⊳ L02 ≫ S =S  □

Symmetri-lemmaet for [x=y] ser således ud: [ZFsub lemma =Symmetry: ΠX , Y: s#X ⊢⊢ s#Y ⊢⊢ X =Y ⊢ Y =X] Vi beviser = Symmetry ved at reducere termen [X = Y] til de to implikationer [s ∈ X ⇒ s ∈ Y] og [s ∈ Y ⇒ s ∈ X]. Herefter sætter vi de to implikationer sammen i omvendt rækkefølge, hvilket giver os [Y =X]: ZFsub proof of =Symmetry:

L01: Arbitrary ≫  X , Y  ;
L02: Side-condition ≫  s#X  ;
L03: Side-condition ≫  s#Y  ;
L04: Premise ≫  X =Y  ;
L05: Extensionality ≫  X =Y ˙⇔ ∀s: (s ∈ X ˙⇔ s ∈ Y) ;
L06: IffSecond ⊳ L05 ⊳ L04 ≫ ∀s: (s ∈ X ˙⇔ s ∈ Y) ;

L07: HelperFromSetEquality ⊳ ⊳

L02 ⊳ ⊳ L03 ≫ ∀s: (s ∈ X ˙⇔ s ∈ Y) ⇒ (s ∈ X ˙⇔ s ∈ Y) ;

L08: MP ⊳ L07 ⊳ L06 ≫  s ∈ X ˙⇔ s ∈ Y  ;
L09: FirstConjunct ⊳ L08 ≫  s ∈ X ⇒ s ∈ Y  ;
L10: SecondConjunct ⊳ L08 ≫  s ∈ Y ⇒ s ∈ X  ;
L11: ToSetEquality ⊳ L10 ⊳ L09 ≫ Y =X  □

Transitivitets-lemmaet for [x=y] ser således ud: [ZFsub lemma =Transitivity: ΠX , Y, Z: s#X ⊢⊢ s#Y ⊢⊢ s#Z ⊢⊢ X =Y ⊢ Y =Z ⊢ X =Z] Vi viser først den svagere påstand, at X er en delmængde af Z: [ZFsub lemma Helper=Transitivity: ΠS, X , Y, Z: s#X ⊢⊢ s#Y ⊢⊢ s#Z ⊢⊢ X =Y ⇒ Y =Z ⇒ S ∈ X ⇒ S ∈ Z] Bevisets kerne består af to anvendelser af FromSetEquality (linie 8–9): ZFsub proof of Helper=Transitivity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  S, X , Y, Z  ;
L03: Side-condition ≫  s#X  ;
L04: Side-condition ≫  s#Y  ;
L05: Side-condition ≫  s#Z  ;
L06: Premise ≫  X =Y  ;
L07: Premise ≫  Y =Z  ;
L08: Premise ≫  S ∈ X  ;

L09: FromSetEquality ⊳ ⊳ L03 ⊳ ⊳

L04 ⊳ L06 ⊳ L08 ≫ S ∈ Y ;

L10: FromSetEquality ⊳ ⊳ L04 ⊳ ⊳

L05 ⊳ L07 ⊳ L09 ≫ S ∈ Z ;

L11: Block ≫  End  ;
L12: Arbitrary ≫  S, X , Y, Z  ;
L13: Ded ⊳ L11 ≫  {s#X ⊢⊢ s#Y ⊢⊢ s#Z ⊢⊢ X = \atop Y ⇒ Y =Z ⇒ S ∈ X ⇒ S ∈ Z □}

Vi bruger nu Helper=Transitivity til at vise, at X er en delmængde af Z (linie 5–8), og vice versa (line 9–12): [ZFsub lemma =Transitivity: ΠX , Y, Z: s#X ⊢⊢ s#Y ⊢⊢ s#Z ⊢⊢ X =Y ⊢ Y =Z ⊢ X =Z] ZFsub proof of =Transitivity:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Side-condition ≫  s#X  ;
L03: Side-condition ≫  s#Y  ;
L04: Side-condition ≫  s#Z  ;
L05: Premise ≫  X =Y  ;
L06: Premise ≫  Y =Z  ;

L07: Helper=Transitivity ⊳ ⊳ L02 ⊳ ⊳

L03 ⊳ ⊳ L04 ≫ X =Y ⇒ Y =Z ⇒ s ∈ X ⇒ s ∈ Z ;

L08: MP2 ⊳ L07 ⊳ L05 ⊳ L06 ≫ s ∈ X ⇒ s ∈ Z ;

L09: =Symmetry ⊳ ⊳ L02 ⊳ ⊳

L03 ⊳ L05 ≫ Y =X ;

L10: =Symmetry ⊳ ⊳ L03 ⊳ ⊳

L04 ⊳ L06 ≫ Z =Y ;

L11: Helper=Transitivity ⊳ ⊳ L04 ⊳ ⊳

L03 ⊳ ⊳ L02 ≫ Z =Y ⇒ Y =X ⇒ s ∈ Z ⇒ s ∈ X ;

L12: MP2 ⊳ L11 ⊳ L10 ⊳ L09 ≫ s ∈ Z ⇒ s ∈ X ;
L13: ToSetEquality ⊳ L08 ⊳ L12 ≫ X =Z  □

9.3 Negeret lighed

I dette sidste underafsnit viser vi, at lige størrelser kan erstatte hinanden i en negeret lighed:

[ZFsub lemma TransferNotEq: ΠX , Y, V, W: s#X ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ X ≠ Y ⊢ X =V ⊢ Y =W ⊢ V ≠ W]

Beviset for TransferNotEq kan gengives som følger:

1. “Antag at V er lig med W. Ud fra præmisserne [X = V] og [Y = W] får vi da [X =Y].”

2. “Men vi har antaget [X ≠ Y]. Derfor kan V ikke være lig med W.”

Vi viser punkt 1 som lemmastumpen HelperTransferNotEq; punkt 2 klares i selve beviset for TransferNotEq:

[ZFsub lemma HelperTransferNotEq: ΠX , Y, V, W: s#X ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ X =V ⇒ Y =W ⇒ V =W ⇒ X =Y]

ZFsub proof of HelperTransferNotEq:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y, V, W  ;
L03: Side-condition ≫  s#X  ;
L04: Side-condition ≫  s#Y  ;
L05: Side-condition ≫  s#V  ;
L06: Side-condition ≫  s#W  ;
L07: Premise ≫  X =V  ;
L08: Premise ≫  Y =W  ;
L09: Premise ≫  V =W  ;

L10: =Transitivity ⊳ ⊳ L03 ⊳ ⊳ L05 ⊳ ⊳

L06 ⊳ L07 ⊳ L09 ≫ X =W ;

L11: =Symmetry ⊳ ⊳ L04 ⊳ ⊳

L06 ⊳ L08 ≫ W =Y ;

L12: =Transitivity ⊳ ⊳ L03 ⊳ ⊳ L06 ⊳ ⊳

L04 ⊳ L10 ⊳ L11 ≫ X =Y ;

L13: Block ≫  End  ;
L14: Arbitrary ≫  X , Y, V, W  ;
L15: Ded ⊳ L13 ≫  s#X ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ ; X = V ⇒ Y = W ⇒ V = W ⇒ ; X =Y  □

[ZFsub lemma TransferNotEq: ΠX , Y, V, W: s#X ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ X ≠ Y ⊢ X =V ⊢ Y =W ⊢ V ≠ W]

ZFsub proof of TransferNotEq:

L01: Arbitrary ≫  X , Y, V, W  ;
L02: Side-condition ≫  s#X  ;
L03: Side-condition ≫  s#Y  ;
L04: Side-condition ≫  s#V  ;
L05: Side-condition ≫  s#W  ;
L06: Premise ≫  X ≠ Y  ;
L07: Premise ≫  X =V  ;
L08: Premise ≫  Y =W  ;

L09: HelperTransferNotEq ⊳ ⊳ L02 ⊳ ⊳

L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ≫ X =V ⇒ Y =W ⇒ V =W ⇒ X =Y ;

L10: MP2 ⊳ L09 ⊳ L07 ⊳ L08 ≫  V =W ⇒ X =Y  ;
L11: MT ⊳ L10 ⊳ L06 ≫  V ≠ W  □

10 Lighedslemmaer

Ved et “unært lighedslemma” vil jeg forstå et lemma af følgende form: “Hvis der gælder [X =Y], så gælder [Op(X)=Op(Y)]” — hvor “ [Op(X)]” står for en unær syntaktisk konstruktion som f.eks. [∪x] eller [{x}].

Tilsvarende kan vi definere et “binært lighedslemma” som et lemma med indholdet: “Hvis der gælder [X =Y] og [V =W], så gælder [Op(X , V)=Op(Y, W)]”

— her kan “[Op(x, y)]” f.eks. stå for [{x, y}] eller [x ∩ y].

I dette afsnit beviser vi lighedslemmaerne for konstruktionerne [{x, y}], [{x}], [∪x], [x ∪ y], [{ph ∈ x | f}] og [x ∩ y]. Figur 3 giver et overblik over afsnittets lemmaer. Hele arbejdet i dette afsnit munder ud i én eneste anvendelse af det sidste lighedslemma (“SameIntersection”) i beviset for hovedresultatet (i afsnit 11.2.5). Man kan altså godt sige, at vi skyder gråspurve med kanoner. Lighedslemmaer har dog også interesse derved, at de kan bruges til at vise, at ZFsub er en teori med lighed (jvf. afsnit 2.8 i [6]); men det er altså ikke et sådant bevis, som er formålet med dette afsnit.

Figur 3: Bevisstrukturen for lighedslemmaerne. Kun lighedslemmaerne er vist. Figuren skal læses ligesom figur 2.

10.1 Par

Når vi skal vise et lighedslemma med konklusionen [Op(X , V) = Op(Y, W)], er det ofte en god ide først at vise et “delmængdelemma” — dvs. et lemma, der konkluderer, at Op(X , V) er en delmængde af Op(Y, W). Vi kan da vise lighedslemmaet ud fra ToSetEquality og to anvendelser af delmængdelemmaet. I dette underafsnit begynder vi med det følgende delmængdelemma:

[ZFsub lemma PairSubset: ΠS, X , Y, V, W: s#X ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ s#S ⊢⊢ X =Y ⇒ V =W ⇒ S ∈ {X , V} ⇒ S ∈ {Y, W}]

Beviset for PairSubset kan gengives som følger:

1. “Antag [X = Y], [V = W] og at S tilhører {X , Y}. Der gælder da S = X eller S =Y.”

2. “S =X medfører [S =Y ˙∨ S =W] (under antagelse af [X =Y]).”

3. “S =Y medfører også [S =Y ˙∨ S =W].”

4. “Derfor må [S = Y ˙∨ S = W] gælde ubetinget. Dette betyder igen, at S tilhører {Y, W}, QED.”

Punkt 2 og 3 varetages af de to lemmastumper HelperPairSubset og Helper(2)PairSubset. Punkt 1 og 4 vises i selve beviset for PairSubset:

[ZFsub lemma HelperPairSubset: ΠS, X , Y, W: s#S ⊢⊢ s#X ⊢⊢ s#Y ⊢⊢ s#W ⊢⊢ X =Y ⇒ S =X ⇒ S =Y ˙∨ S =W]

ZFsub proof of HelperPairSubset:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  S, X , Y, W  ;
L03: Side-condition ≫  s#S  ;
L04: Side-condition ≫  s#X  ;
L05: Side-condition ≫  s#Y  ;
L06: Side-condition ≫  s#W  ;
L07: Premise ≫  X =Y  ;
L08: Premise ≫  S =X  ;

L09: =Transitivity ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳

L05 ⊳ L08 ⊳ L07 ≫ S =Y ;

L10: WeakenOr2 ⊳ L09 ≫  S =Y ˙∨ S =W  ;
L11: Block ≫  End  ;
L12: Arbitrary ≫  S, X , Y, W  ;
L13: Ded ⊳ L11 ≫  s#S ⊢⊢ s#X ⊢⊢ s#Y ⊢⊢ s#W ⊢⊢ ; X =Y ⇒ S =X ⇒ ; S =Y ˙∨ S =W  □

[ZFsub lemma Helper(2)PairSubset: ΠS, Y, V, W: s#S ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ V =W ⇒ S =V ⇒ S =Y ˙∨ S =W] ZFsub proof of Helper(2)PairSubset:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  S, Y, V, W  ;
L03: Side-condition ≫  s#S  ;
L04: Side-condition ≫  s#Y  ;
L05: Side-condition ≫  s#V  ;
L06: Side-condition ≫  s#W  ;
L07: Premise ≫  V =W  ;
L08: Premise ≫  S =V  ;

L09: =Transitivity ⊳ ⊳ L03 ⊳ ⊳ L05 ⊳ ⊳

L06 ⊳ L08 ⊳ L07 ≫ S =W ;

L10: WeakenOr1 ⊳ L09 ≫  S =Y ˙∨ S =W  ;
L11: Block ≫  End  ;
L12: Arbitrary ≫  S, Y, V, W  ;
L13: Ded ⊳ L11 ≫  s#S ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ ; V =W ⇒ S =V ⇒ ; S =Y ˙∨ S =W  □

[ZFsub lemma PairSubset: ΠS, X , Y, V, W: s#X ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ s#S ⊢⊢ X =Y ⇒ V =W ⇒ S ∈ {X , V} ⇒ S ∈ {Y, W}]

ZFsub proof of PairSubset:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  S, X , Y, V, W  ;
L03: Side-condition ≫  s#X  ;
L04: Side-condition ≫  s#Y  ;
L05: Side-condition ≫  s#V  ;
L06: Side-condition ≫  s#W  ;
L07: Side-condition ≫  s#S  ;
L08: Premise ≫  X =Y  ;
L09: Premise ≫  V =W  ;
L10: Premise ≫  S ∈ {X , V}  ;
L11: Pair2Formula ⊳ L10 ≫  S =X ˙∨ S =V  ;

L12: HelperPairSubset ⊳ ⊳ L07 ⊳ ⊳

L03 ⊳ ⊳ L04 ⊳ ⊳ L06 ≫ X =Y ⇒ S =X ⇒ S =Y ˙∨ S =W ;

L13: MP ⊳ L12 ⊳ L08 ≫  S =X ⇒ S =Y ˙∨ S =W  ;

L14: Helper(2)PairSubset ⊳ ⊳ L07 ⊳ ⊳

L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ≫ V =W ⇒ S =V ⇒ S =Y ˙∨ S =W ;

L15: MP ⊳ L14 ⊳ L09 ≫  S =V ⇒ S =Y ˙∨ S =W  ;

L16: FromDisjuncts ⊳ L11 ⊳ L13 ⊳

L15 ≫ S =Y ˙∨ S =W ;

L17: Formula2Pair ⊳ L16 ≫  S ∈ {Y, W}  ;
L18: Block ≫  End  ;
L19: Arbitrary ≫  S, X , Y, V, W  ;

L20: Ded ⊳ L18 ≫  s#X ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ ; s#S ⊢⊢ X =Y ⇒ V =W ⇒ ; S ∈ {X , V} ⇒ S ∈ {Y, W}  □

Kommet så vidt kan vi bevise lighedslemmaet SamePair. Vi viser, at {X , V} er en delmængde af {Y, W} (linie 8–11), og vice versa (linie 12–14):

[ZFsub lemma SamePair: ΠX , Y, V, W: s#X ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ t#{X , V} ⊢⊢ t#{Y, W} ⊢⊢ X =Y ⊢ V =W ⊢ {X , V}={Y, W}]

ZFsub proof of SamePair:

L01: Arbitrary ≫  X , Y, V, W  ;
L02: Side-condition ≫  s#X  ;
L03: Side-condition ≫  s#Y  ;
L04: Side-condition ≫  s#V  ;
L05: Side-condition ≫  s#W  ;
L06: Side-condition ≫  t#{X , V}  ;
L07: Side-condition ≫  t#{Y, W}  ;
L08: Premise ≫  X =Y  ;
L09: Premise ≫  V =W  ;

L10: PairSubset ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳

L04 ⊳ ⊳ L05 ≫ X =Y ⇒ V =W ⇒ t ∈ {X , V} ⇒ t ∈ {Y, W} ;

L11: MP2 ⊳ L10 ⊳ L08 ⊳ L09 ≫  t ∈ {X , V} ⇒ t ∈ {Y, W}  ;

L12: =Symmetry ⊳ ⊳ L02 ⊳ ⊳

L03 ⊳ L08 ≫ Y =X ;

L13: =Symmetry ⊳ ⊳ L04 ⊳ ⊳

L05 ⊳ L09 ≫ W =V ;

L14: PairSubset ⊳ ⊳ L03 ⊳ ⊳ L02 ⊳ ⊳

L05 ⊳ ⊳ L04 ≫ Y =X ⇒ W =V ⇒ t ∈ {Y, W} ⇒ t ∈ {X , V} ;

L15: MP2 ⊳ L14 ⊳ L12 ⊳ L13 ≫  t ∈ {Y, W} ⇒ t ∈ {X , V}  ;

L16: ToSetEquality(t) ⊳ ⊳ L06 ⊳ ⊳

L07 ⊳ L11 ⊳ L15 ≫ {X , V}={Y, W} □

10.2 Singleton-mængde

Lighedslemmaet for singleton-konstruktionen ser således ud:

[ZFsub lemma SameSingleton: ΠX , Y: s#X ⊢⊢ s#Y ⊢⊢ t#{X , X } ⊢⊢ t#{Y, Y} ⊢⊢ X =Y ⊢ {X }={Y}]

Da [{x}] er makrodefineret som [{x, x}], kan vi let vise SameSingleton ud fra SamePair:

ZFsub proof of SameSingleton:

L01: Arbitrary ≫  X , Y  ;
L02: Side-condition ≫  s#X  ;

L03: Side-condition ≫  s#Y  ;
L04: Side-condition ≫  t#{X , X }  ;
L05: Side-condition ≫  t#{Y, Y}  ;
L06: Premise ≫  X =Y  ;

L07: SamePair ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳

L05 ⊳ L06 ⊳ L06 ≫ {X , X }={Y, Y} ;

L08: Repetition ⊳ L07 ≫  {X }={Y}  □

10.3 Foreningsmængde

Delmængdelemmaet mht. [∪x] ser således ud: [ZFsub lemma UnionSubset: ΠS, X , Y: s#X ⊢⊢ s#Y ⊢⊢ X =Y ⇒ S ∈ ∪X ⇒ S ∈ ∪Y] Bevisets kerne (linie 7–11) er en simpel anvendelse af definitionen af [∪x]: ZFsub proof of UnionSubset:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  S, X , Y  ;
L03: Side-condition ≫  s#X  ;
L04: Side-condition ≫  s#Y  ;
L05: Premise ≫  X =Y  ;
L06: Premise ≫  S ∈ ∪X  ;
L07: Union2Formula ⊳ L06 ≫  S ∈ Ex_{10} ˙∧ Ex_{10} ∈ X  ;
L08: FirstConjunct ⊳ L07 ≫  S ∈ Ex_{10}  ;
L09: SecondConjunct ⊳ L07 ≫  Ex_{10} ∈ X  ;

L10: FromSetEquality ⊳ ⊳ L03 ⊳ ⊳

L04 ⊳ L05 ⊳ L09 ≫ Ex_{10} ∈ Y ;

L11: Formula2Union ⊳ L08 ⊳ L10 ≫  S ∈ ∪Y  ;
L12: Block ≫  End  ;
L13: Arbitrary ≫  S, X , Y  ;
L14: Ded ⊳ L12 ≫  {s#X ⊢⊢ s#Y ⊢⊢ \atop X =Y ⇒ S ∈ ∪X ⇒ S ∈ ∪Y  □}

I beviset for lighedslemmaet SameUnion viser vi, at ∪X er en delmængde af ∪Y (linie 4–6), og vice versa (line 7–9): [ZFsub lemma SameUnion: ΠX , Y: s#X ⊢⊢ s#Y ⊢⊢ X =Y ⊢ ∪X =∪Y] ZFsub proof of SameUnion:

L01: Arbitrary ≫  X , Y  ;
L02: Side-condition ≫  s#X  ;
L03: Side-condition ≫  s#Y  ;
L04: Premise ≫  X =Y  ;
L05: UnionSubset ⊳ ⊳ L02 ⊳ ⊳ L03 ≫ X =Y ⇒ s ∈ ∪X ⇒ s ∈ ∪Y  ;
L06: MP ⊳ L05 ⊳ L04 ≫  s ∈ ∪X ⇒ s ∈ ∪Y  ;

L07: =Symmetry ⊳ ⊳ L02 ⊳ ⊳

L03 ⊳ L04 ≫ Y =X ;

L08: UnionSubset ⊳ ⊳ L03 ⊳ ⊳ L02 ≫ Y =X ⇒ s ∈ ∪Y ⇒ s ∈ ∪X  ;
L09: MP ⊳ L08 ⊳ L07 ≫ s ∈ ∪Y ⇒ s ∈ ∪X ;
L10: ToSetEquality ⊳ L06 ⊳ L09 ≫ ∪X =∪Y  □

10.4 Binær foreningsmængde

I lighedslemmaet for [x ∪ y] bliver problemet med sidebetingelserne meget tydeligt:

[ZFsub lemma SameBinaryUnion: ΠX , Y, V, W: s#X ⊢⊢ s#Y ⊢⊢ t#{X , X } ⊢⊢ t#{Y, Y} ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ t#{V, V} ⊢⊢ t#{W, W} ⊢⊢ s#{X } ⊢⊢ s#{Y} ⊢⊢ s#{V} ⊢⊢ s#{W} ⊢⊢ s#{{X }, {V}} ⊢⊢ s#{{Y}, {W}} ⊢⊢ t#{{X }, {V}} ⊢⊢ t#{{Y}, {W}} ⊢⊢ X =Y ⊢ V =W ⊢ X ∪ V =Y ∪ W]

Alt i alt er der 16 sidebetingelser. Et sådant lemma er jo ikke til at arbejde med. Derfor vil vi bruge objektvariable i formuleringen af de lemmaer, der afhænger af SameBinaryUnion. På dén måde bliver alle sidebetingelserne automatisk opfyldt, og vi behøver ikke at behandle dem eksplicit.

Problemet med SameBinaryUnion er, at det nedarver sidebetingelser fra tre forskellige lemmaer (jvf. figur 3), og at der ikke er noget overlap mellem sidebetingelserne. Mange af sidebetingelserne er ensbetydende; f.eks. medfører [s#X] og [s#{X }] hinanden. Bevischeckeren er imidlertid ikke i stand til at udnytte dette; vi kan ikke gøre andet end at opremse alle sidebetingelserne.

Ironisk nok er selve beviset for SameBinaryUnion ret enkelt. Vi sætter blot lighedslemmaerne SameSingleton, SamePair og SameUnion sammen:

ZFsub proof of SameBinaryUnion:

L01: Arbitrary ≫  X , Y, V, W  ;
L02: Side-condition ≫  s#X  ;
L03: Side-condition ≫  s#Y  ;
L04: Side-condition ≫  t#{X , X }  ;
L05: Side-condition ≫  t#{Y, Y}  ;
L06: Side-condition ≫  s#V  ;
L07: Side-condition ≫  s#W  ;
L08: Side-condition ≫  t#{V, V}  ;
L09: Side-condition ≫  t#{W, W}  ;
L10: Side-condition ≫  s#{X }  ;
L11: Side-condition ≫  s#{Y}  ;
L12: Side-condition ≫  s#{V}  ;
L13: Side-condition ≫  s#{W}  ;
L14: Side-condition ≫  s#{{X }, {V}}  ;
L15: Side-condition ≫  s#{{Y}, {W}}  ;
L16: Side-condition ≫  t#{{X }, {V}}  ;
L17: Side-condition ≫  t#{{Y}, {W}}  ;
L18: Premise ≫  X =Y  ;

L19: Premise ≫  V =W  ;

L20: SameSingleton ⊳ ⊳ L02 ⊳ ⊳

L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ L18 ≫ {X }={Y} ;

L21: SameSingleton ⊳ ⊳ L06 ⊳ ⊳

L07 ⊳ ⊳ L08 ⊳ ⊳ L09 ⊳ L19 ≫ {V}={W} ;

L22: SamePair ⊳ ⊳ L10 ⊳ ⊳ L11 ⊳ ⊳ L12 ⊳ ⊳ L13 ⊳ ⊳ L16 ⊳ ⊳

L17 ⊳ L20 ⊳ L21 ≫ {{X }, {V}}={{Y}, {W}} ;

L23: SameUnion ⊳ ⊳ L14 ⊳ ⊳

L15 ⊳ L22 ≫ ∪{{X }, {V}}=∪{{Y}, {W}} ;

L24: Repetition ⊳ L23 ≫  X ∪ V =Y ∪ W  □

10.5 Separation

Delmængdelemmaet for konstruktionen [{ph ∈ T | F}] ser således ud:

[ZFsub lemma SeparationSubset: ΠA, B, S, X , Y: s#X ⊢⊢ s#Y ⊢⊢ X =Y ⇒ (A ˙⇔ B) ⇒ S ∈ {ph ∈ X | A} ⇒ S ∈ {ph ∈ Y | B}]

I beviset går vi fra [S ∈ X] til [S ∈ Y] (linie 9–10), og fra [A] til [B] (linie 11–12):

ZFsub proof of SeparationSubset:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B, S, X , Y  ;
L03: Side-condition ≫  s#X  ;
L04: Side-condition ≫  s#Y  ;
L05: Premise ≫  X =Y  ;
L06: Premise ≫  A ˙⇔ B  ;
L07: Premise ≫  S ∈ {ph ∈ X | A}  ;
L08: Sep2Formula ⊳ L07 ≫  S ∈ X ˙∧ A  ;
L09: FirstConjunct ⊳ L08 ≫  S ∈ X  ;

L10: FromSetEquality ⊳ ⊳ L03 ⊳ ⊳

L04 ⊳ L05 ⊳ L09 ≫ S ∈ Y ;

L11: SecondConjunct ⊳ L08 ≫  A  ;
L12: IffSecond ⊳ L06 ⊳ L11 ≫  B  ;
L13: Formula2Sep ⊳ L10 ⊳ L12 ≫  S ∈ {ph ∈ Y | B}  ;
L14: Block ≫  End  ;
L15: Arbitrary ≫  A, B, S, X , Y  ;
L16: Ded ⊳ L14 ≫  s#X ⊢⊢ s#Y ⊢⊢ X =Y ⇒ ; (A ˙⇔ B) ⇒ S ∈ {ph ∈ X | ; A} ⇒ S ∈ {ph ∈ Y | B}  □

I beviset for lighedslemmaet SameSeparation viser vi, at {ph ∈ X | A} er en delmængde af {ph ∈ Y | B} (linie 4–7), og vice versa (linie 8–11):

[ZFsub lemma SameSeparation: ΠA, B, X , Y: s#X ⊢⊢ s#Y ⊢⊢ X =Y ⊢ A ˙⇔ B ⊢ {ph ∈ X | A}={ph ∈ Y | B}] ZFsub proof of SameSeparation:

L01: Arbitrary ≫  A, B, X , Y  ;
L02: Side-condition ≫  s#X  ;
L03: Side-condition ≫  s#Y  ;
L04: Premise ≫  X =Y  ;
L05: Premise ≫  A ˙⇔ B  ;

L06: SeparationSubset ⊳ ⊳ L02 ⊳ ⊳

L03 ≫ X =Y ⇒ (A ˙⇔ B) ⇒ s ∈ {ph ∈ X | A} ⇒ s ∈ {ph ∈ Y | B} ;

L07: MP2 ⊳ L06 ⊳ L04 ⊳ L05 ≫  {s ∈ \{ph ∈ X | A\} ⇒ \atop s ∈ \{ph ∈ Y | B\}  ;}

L08: =Symmetry ⊳ ⊳ L02 ⊳ ⊳

L03 ⊳ L04 ≫ Y =X ;

L09: IffCommutativity ⊳ L05 ≫ B ˙⇔ A ;

L10: SeparationSubset ⊳ ⊳ L03 ⊳ ⊳

L02 ≫ Y =X ⇒ (B ˙⇔ A) ⇒ s ∈ {ph ∈ Y | B} ⇒ s ∈ {ph ∈ X | A} ;

L11: MP2 ⊳ L10 ⊳ L08 ⊳ L09 ≫  {s ∈ \{ph ∈ Y | B\} ⇒ \atop s ∈ \{ph ∈ X | A\}  ;}
L12: ToSetEquality ⊳ L07 ⊳ L11 ≫ {ph ∈ X | A}={ph ∈ Y | B} □

10.6 Binær fællesmængde

Delmængdelemmaet for konstruktionen [x ∩ y] adskiller sig fra normen ved ikke at nævne [x ∩ y] eksplicit:

[ZFsub lemma IntersectionSubset: ΠS, X , Y, V, W: s#X ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ X =Y ⇒ V =W ⇒ S ∈ X ˙∧ S ∈ V ⇒ S ∈ Y ˙∧ S ∈ W]

Bevisets kerne består af to anvendelser af FromSetEquality (linie 10–11 og 12–13):

ZFsub proof of IntersectionSubset:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  S, X , Y, V, W  ;
L03: Side-condition ≫  s#X  ;
L04: Side-condition ≫  s#Y  ;
L05: Side-condition ≫  s#V  ;
L06: Side-condition ≫  s#W  ;
L07: Premise ≫  X =Y  ;
L08: Premise ≫  V =W  ;
L09: Premise ≫  S ∈ X ˙∧ S ∈ V  ;
L10: FirstConjunct ⊳ L09 ≫  S ∈ X  ;

L11: FromSetEquality ⊳ ⊳ L03 ⊳ ⊳

L04 ⊳ L07 ⊳ L10 ≫ S ∈ Y ;

L12: SecondConjunct ⊳ L09 ≫  S ∈ V  ;

L13: FromSetEquality ⊳ ⊳ L05 ⊳ ⊳

L06 ⊳ L08 ⊳ L12 ≫ S ∈ W ;

L14: JoinConjuncts ⊳ L11 ⊳ L13 ≫  S ∈ Y ˙∧ S ∈ W  ;
L15: Block ≫  End  ;
L16: Arbitrary ≫  S, X , Y, V, W  ;
L17: Ded ⊳ L15 ≫  s#X ⊢⊢ s#Y ⊢⊢ s#V ⊢⊢ s#W ⊢⊢ ; X = Y ⇒ V = W ⇒ S ∈ X ˙∧ ; S ∈ V ⇒ S ∈ Y ˙∧ S ∈ W  □

Så er vi kommet til lighedslemmaet SameIntersection. Da dette lemma afhænger af SameBinaryUnion, slår vi her over til objektvariable (jvf. afsnit 10.4). Den store ulempe herved er, at objektvariable ikke kan instantieres til andre variable. Derfor vil en formulering som f.eks. [x = y ⊢ v = w ⊢ x ∩ v = y ∩ w] sandsynligvis ikke kunne anvendes senere hen i rapporten, da vi ikke kan instantiere x, y, v eller w.

Vi må altså undersøge, hvad SameIntersection egentlig skal bruges til, før vi formulerer lemmaet. Det viser sig, at den følgende formulering kan bruges:

[ZFsub lemma SameIntersection: x = [Ex_{1} ∈ OBS]_{r} ⊢ y = [Ex_{2} ∈ OBS]_{r} ⊢ x ∩ y =[Ex_{1} ∈ OBS]_{r} ∩ [Ex_{2} ∈ OBS]_{r}]

Man kan sige, at vi har instantieret objektvariablene “på forhånd”.

Beviset for SameIntersection kan beskrives som følger:

1. Fra SameBinaryUnion får vi, at de to binære foreningsmængder er éns (linie 3).

2. De to formler [ph_{3} ∈ x ˙∧ ph_{3} ∈ y] og [ph_{3} ∈ [Ex_{1} ∈ OBS]_{r} ˙∧ ph_{3} ∈ [Ex_{2} ∈ OBS]_{r}] implicerer hinanden (linie 4–5 og 6–9).

3. Fra punkt 1, punkt 2 og SameSeparation får vi da, at de to binære fællesmængder er éns (linie 10–12).

Her er beviset:

ZFsub proof of SameIntersection:

L01: Premise ≫  x =[Ex_{1} ∈ OBS]_{r}  ;
L02: Premise ≫  y =[Ex_{2} ∈ OBS]_{r}  ;

L03: SameBinaryUnion ⊳ L01 ⊳

L02 ≫ x ∪ y =

[Ex_{1} ∈ OBS]_{r} ∪ [Ex_{2} ∈ OBS]_{r} ;

L04: IntersectionSubset ≫ x =[Ex_{1} ∈ OBS]_{r} ⇒ y =[Ex_{2} ∈ OBS]_{r} ⇒ ph_{3} ∈ x ˙∧ ph_{3} ∈ y ⇒ ph_{3} ∈ [Ex_{1} ∈ OBS]_{r} ˙∧ ph_{3} ∈ [Ex_{2} ∈ OBS]_{r} ; L05: MP2 ⊳ L04 ⊳ L01 ⊳ L02 ≫ ph_{3} ∈ x ˙∧ ph_{3} ∈ y ⇒ ph_{3} ∈ [Ex_{1} ∈ OBS]_{r} ˙∧ ph_{3} ∈ [Ex_{2} ∈ OBS]_{r} ;

L06: =Symmetry ⊳ L01 ≫  [Ex_{1} ∈ OBS]_{r} =x  ;
L07: =Symmetry ⊳ L02 ≫  [Ex_{2} ∈ OBS]_{r} =y  ;

L08: IntersectionSubset ≫ [Ex_{1} ∈ OBS]_{r} =x ⇒ [Ex_{2} ∈ OBS]_{r} =y ⇒ ph_{3} ∈ [Ex_{1} ∈ OBS]_{r} ˙∧ ph_{3} ∈ [Ex_{2} ∈ OBS]_{r} ⇒ ph_{3} ∈ x ˙∧ ph_{3} ∈ y ;

L09: MP2 ⊳ L08 ⊳ L06 ⊳ L07 ≫ ph_{3} ∈ [Ex_{1} ∈ OBS]_{r} ˙∧ ph_{3} ∈ [Ex_{2} ∈ OBS]_{r} ⇒ ph_{3} ∈ x ˙∧ ph_{3} ∈ y ;

L10: JoinConjuncts ⊳ L05 ⊳ L09 ≫ ph_{3} ∈ x ˙∧ ph_{3} ∈ y ˙⇔ ph_{3} ∈ [Ex_{1} ∈ OBS]_{r} ˙∧ ph_{3} ∈ [Ex_{2} ∈ OBS]_{r} ;

L11: SameSeparation⊳L03⊳L10 ≫ {ph ∈ x ∪ y | ph_{3} ∈ x ˙∧ ph_{3} ∈ y}= {ph ∈ [Ex_{1} ∈ OBS]_{r} ∪ [Ex_{2} ∈ OBS]_{r} | ph_{3} ∈ [Ex_{1} ∈ OBS]_{r} ˙∧ ph_{3} ∈ [Ex_{2} ∈ OBS]_{r}} ;

L12: Repetition ⊳ L11 ≫ x ∩ y = [Ex_{1} ∈ OBS]_{r} ∩ [Ex_{2} ∈ OBS]_{r} □

11 Hovedresultatet

Vi kan nu endelig gå i gang med hovedresultatet, som vi allerede udtrykte formelt i afsnit 5.10:

[ZFsub lemma EqSysIsPartition: EqRel(r, OBS) ⊢ Partition(OBS/r, OBS)]

Vi skal vise tre ting:

• Ingen ækvivalensklasser er tomme (underafsnit 11.1),

• Alle ækvivalensklasser er disjunkte (underafsnit 11.2), og

• Fællesmængden af alle ækvivalensklasserne er lig den oprindelige mængde OBS (underafsnit 11.3).

Til sidst binder vi alle trådene sammen i underafsnit 11.4.

11.1 Ingen ækvivalensklasser er tomme

Lemmaet AutoMember udsiger, at ækvivalensklassen [S ∈ BS]_{R} indeholder S selv som medlem:

[ZFsub lemma AutoMember: ΠR, S, BS: s#R ⊢⊢ s#BS ⊢⊢ EqRel(R, BS) ⊢ S ∈ BS ⊢ S ∈ [S ∈ BS]_{R}] AutoMember følger af, at vi har R(S, S), fordi ækvivalensrelationen R er refleksiv:

ZFsub proof of AutoMember:

L01: Arbitrary ≫  R, S, BS  ;
L02: Side-condition ≫  s#R  ;
L03: Side-condition ≫  s#BS  ;
L04: Premise ≫  EqRel(R, BS)  ;
L05: Premise ≫  S ∈ BS  ;
L06: ERisReflexive ⊳ L04 ≫  ReflRel(R, BS)  ;

L07: Reflexivity ⊳ ⊳ L02 ⊳ ⊳

L03 ⊳ L06 ⊳ L05 ≫ R(S, S) ;

L08: Formula2Sep ⊳ L05 ⊳ L07 ≫  S ∈ {ph ∈ BS | R(ph_{1}, S)}  □

Ud fra AutoMember kan vi nu vise, at ingen medlemmer af et ækvivalenssystem er tomme:

[ZFsub lemma EqSysNotØ: ΠR, S, BS: s#R ⊢⊢ s#S ⊢⊢ s#BS ⊢⊢ s#[Ex_{1} ∈ BS]_{R} ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ EqRel(R, BS) ⊢ S ∈ BS/R ⇒ S ≠ Ø]

Pga. sidebetingelserne deler vi beviset op i to, med HelperEqSysNotØ som lemmastump:

[ZFsub lemma HelperEqSysNotØ: ΠR, S, BS: s#R ⊢⊢ s#S ⊢⊢ s#BS ⊢⊢ s#[Ex_{1} ∈ BS]_{R} ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ EqRel(R, BS) ⇒ S ∈ BS/R ⇒ S ≠ Ø]

Næsten hele beviset varetages af HelperEqSysNotØ. Beviset forløber som følger: Lad S være et medlem af et ækvivalenssystem (linie 8). Pr. definition er S en ækvivalensklasse (linie 9–12). Da enhver ækvivalensklasse har et medlem, har S et medlem (linie 13–14). Da enhver mængde med et medlem ikke er tom, er S ikke tom, QED (linie 15).

ZFsub proof of HelperEqSysNotØ:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, S, BS  ;
L03: Side-condition ≫  s#R  ;
L04: Side-condition ≫  s#S  ;
L05: Side-condition ≫  s#BS  ;
L06: Side-condition ≫  s#[Ex_{1} ∈ BS]_{R}  ;
L07: Premise ≫  EqRel(R, BS)  ;
L08: Premise ≫  S ∈ BS/R  ;
L09: Sep2Formula ⊳ L08 ≫  {S ∈ P(BS) ˙∧ (Ex_{1} ∈ BS ˙∧ \atop [Ex_{1} ∈ BS]_{R} =S)  ;}
L10: SecondConjunct ⊳ L09 ≫  Ex_{1} ∈ BS ˙∧ [Ex_{1} ∈ BS]_{R} =S ;
L11: FirstConjunct ⊳ L10 ≫  Ex_{1} ∈ BS  ;
L12: SecondConjunct ⊳ L10 ≫  [Ex_{1} ∈ BS]_{R} =S  ;

L13: AutoMember ⊳ ⊳ L03 ⊳ ⊳

L05 ⊳ L07 ⊳ L11 ≫ Ex_{1} ∈ [Ex_{1} ∈ BS]_{R} ;

L14: FromSetEquality ⊳ ⊳ L06 ⊳ ⊳

L04 ⊳ L12 ⊳ L13 ≫ Ex_{1} ∈ S ;

L15: MemberNotØ ⊳ ⊳ L04 ⊳ L14 ≫  S ≠ Ø  ;
L16: Block ≫  End  ;
L17: Arbitrary ≫  R, S, BS  ;

L18: Ded ⊳ L16 ≫

s#R ⊢⊢ s#S ⊢⊢ s#BS ⊢⊢
s#[Ex_{1} ∈ BS]_{R} ⊢⊢ t#R ⊢⊢
t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢
EqRel(R, BS) ⇒ S ∈ BS/R ⇒
S ≠ Ø □

I hovedlemmaet skifter vi en implikation ud med en inferens:

[ZFsub lemma EqSysNotØ: ΠR, S, BS: s#R ⊢⊢ s#S ⊢⊢ s#BS ⊢⊢ s#[Ex_{1} ∈ BS]_{R} ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ EqRel(R, BS) ⊢ S ∈ BS/R ⇒ S ≠ Ø]

ZFsub proof of EqSysNotØ:

L01: Arbitrary ≫  R, S, BS  ;
L02: Side-condition ≫  s#R  ;
L03: Side-condition ≫  s#S  ;
L04: Side-condition ≫  s#BS  ;
L05: Side-condition ≫  s#[Ex_{1} ∈ BS]_{R}  ;
L06: Side-condition ≫  t#R  ;
L07: Side-condition ≫  t#BS  ;
L08: Side-condition ≫  u#R  ;
L09: Side-condition ≫  u#BS  ;
L10: Premise ≫  EqRel(R, BS)  ;

L11: HelperEqSysNotØ ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳ L07 ⊳ ⊳ L08 ⊳ ⊳ L09 ≫

EqRel(R, BS) ⇒ S ∈ BS/R ⇒ S ≠ Ø ;
L12: MP ⊳ L11 ⊳ L10 ≫  S ∈ BS/R ⇒ S ≠ Ø  □

11.2 Alle ækvivalensklasser er disjunkte

Dette underafsnit indeholder den mest komplicerede del af beviset for hovedresultatet. Som det kan ses af figur 4, har jeg måttet tage et “snyde-aksiom” til hjælp for at blive færdig.

Figur 4: Bevisstrukturen for underafsnit 11.2. Kun lemmaerne fra dette afsnit er vist. Figuren skal læses ligesom figur 2. Kassen mærket “CheatAllDisjoint” repræsenterer et “snyde-aksiom”, så der går ingen pile ind i denne kasse.

11.2.1 Lemmaet “EqSubset”

Indholdet af det første lemma, EqSubset, kan udtrykkes som følger: “Lad X og Y være to medlemmer af BS. Hvis der gælder R(X , Y), så er ækvivalensklassen [X ∈ BS]_{R} en delmængde af ækvivalensklassen [Y ∈ BS]_{R}”:

[ZFsub lemma EqSubset: ΠR, S, X , Y, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ X ∈ BS ⊢ Y ∈ BS ⊢ EqRel(R, BS) ⊢ R(X , Y) ⊢ S ∈ [X ∈ BS]_{R} ⇒ S ∈ [Y ∈ BS]_{R}]

Beviset forløber som følger:

1. Lad S være et vilkårligt medlem af [X ∈ BS]_{R}. Vi har da R(S, X) (linie 13–16).

2. Ud fra R(S, X) og antagelsen R(X , Y) får vi R(S, Y), da R er transitiv (linie 17–19).

3. R(S, Y) medfører igen S ∈ [Y ∈ BS]_{R}, QED (linie 20).

Hele dette ræsonnement gennemføres i lemmastumpen HelperEqSubset. Selve beviset for EqSubset består af den sædvanlige omskrivning fra implikation til inferens. Her er beviserne:

[ZFsub lemma HelperEqSubset: ΠR, S, X , Y, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ X ∈ BS ⇒ Y ∈ BS ⇒ EqRel(R, BS) ⇒ R(X , Y) ⇒ S ∈ [X ∈ BS]_{R} ⇒ S ∈ [Y ∈ BS]_{R}]

ZFsub proof of HelperEqSubset:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, S, X , Y, BS  ;
L03: Side-condition ≫  s#R  ;
L04: Side-condition ≫  s#BS  ;
L05: Side-condition ≫  t#R  ;
L06: Side-condition ≫  t#BS  ;
L07: Side-condition ≫  u#R  ;
L08: Side-condition ≫  u#BS  ;
L09: Premise ≫  X ∈ BS  ;
L10: Premise ≫  Y ∈ BS  ;
L11: Premise ≫  EqRel(R, BS)  ;
L12: Premise ≫  R(X , Y)  ;
L13: Premise ≫  S ∈ [X ∈ BS]_{R}  ;
L14: Repetition ⊳ L13 ≫  S ∈ {ph ∈ BS | R(ph_{1}, X)} ;
L15: Sep2Formula ⊳ L14 ≫  S ∈ BS ˙∧ R(S, X)  ;
L16: SecondConjunct ⊳ L15 ≫  R(S, X)  ;
L17: ERisTransitive ⊳ L11 ≫  TransRel(R, BS)  ;
L18: FirstConjunct ⊳ L15 ≫  S ∈ BS  ;

L19: Transitivity ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳ L07 ⊳ ⊳ L08 ⊳ L17 ⊳ L18 ⊳ L09 ⊳ L10 ⊳

L16 ⊳ L12 ≫ R(S, Y) ;

L20: Formula2Sep ⊳ L18 ⊳ L19 ≫  S ∈ [Y ∈ BS]_{R}  ;
L21: Block ≫  End  ;
L22: Arbitrary ≫  R, S, X , Y, BS  ;

L23: Ded ⊳ L21 ≫

s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢
t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢
X ∈ BS ⇒ Y ∈ BS ⇒
EqRel(R, BS) ⇒ R(X , Y) ⇒
S ∈ [X ∈ BS]_{R} ⇒
S ∈ [Y ∈ BS]_{R} □

[ZFsub lemma EqSubset: ΠR, S, X , Y, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ X ∈ BS ⊢ Y ∈ BS ⊢ EqRel(R, BS) ⊢ R(X , Y) ⊢ S ∈ [X ∈ BS]_{R} ⇒ S ∈ [Y ∈ BS]_{R}]

ZFsub proof of EqSubset:

L01: Arbitrary ≫  R, S, X , Y, BS  ;
L02: Side-condition ≫  s#R  ;
L03: Side-condition ≫  s#BS  ;
L04: Side-condition ≫  t#R  ;
L05: Side-condition ≫  t#BS  ;
L06: Side-condition ≫  u#R  ;
L07: Side-condition ≫  u#BS  ;
L08: Premise ≫  X ∈ BS  ;
L09: Premise ≫  Y ∈ BS  ;
L10: Premise ≫  EqRel(R, BS)  ;
L11: Premise ≫  R(X , Y)  ;

L12: HelperEqSubset ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳

L07 ≫ X ∈ BS ⇒ Y ∈ BS ⇒ EqRel(R, BS) ⇒ R(X , Y) ⇒ S ∈ [X ∈ BS]_{R} ⇒ S ∈ [Y ∈ BS]_{R} ;

L13: MP4 ⊳ L12 ⊳ L08 ⊳ L09 ⊳

L10 ⊳ L11 ≫ S ∈ [X ∈ BS]_{R} ⇒ S ∈ [Y ∈ BS]_{R} □

11.2.2 Lemmaet “EqNecessary”

Det er nu en let sag at vise den stærkere påstand, at [X ∈ BS]_{R} rent faktisk er lig med [Y ∈ BS]_{R}^{20}. Som så ofte før ligger den interessante del af beviset i en lemmastump, der her hedder “HelperEqNecessary”:

20Dette er lemma 4.4.a.1 i [5].

[ZFsub lemma HelperEqNecessary: ΠR, X , Y, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ X ∈ BS ⇒ Y ∈ BS ⇒ EqRel(R, BS) ⇒ R(X , Y) ⇒ [X ∈ BS]_{R} =[Y ∈ BS]_{R}]

Beviset kan beskrives som følger:

1. Fra EqSubset ved vi, at antagelsen R(X , Y) medfører, at [X ∈ BS]_{R} er en delmængde af [X ∈ BS]_{R}. (Linie 13).

2. Da R er symmetrisk, gælder der også R(Y, X). (Linie 14–15).

3. Vi kan derfor bruge EqSubset én gang til — vi får, at [Y ∈ BS]_{R} er en delmængde af [X ∈ BS]_{R}. (Linie 16).

4. Ud fra punkt 1 og 3 følger [[X ∈ BS]_{R} =[Y ∈ BS]_{R}], QED. (Linie 17).

Her er selve beviset:

ZFsub proof of HelperEqNecessary:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, X , Y, BS  ;
L03: Side-condition ≫  s#R  ;
L04: Side-condition ≫  s#BS  ;
L05: Side-condition ≫  t#R  ;
L06: Side-condition ≫  t#BS  ;
L07: Side-condition ≫  u#R  ;
L08: Side-condition ≫  u#BS  ;
L09: Premise ≫  X ∈ BS  ;
L10: Premise ≫  Y ∈ BS  ;
L11: Premise ≫  EqRel(R, BS)  ;
L12: Premise ≫  R(X , Y)  ;

L13: EqSubset ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳ L07 ⊳ ⊳

L08⊳L09⊳L10⊳L11⊳L12 ≫ s ∈ [X ∈ BS]_{R} ⇒ s ∈ [Y ∈ BS]_{R} ;

L14: ERisSymmetric ⊳ L11 ≫  SymRel(R, BS)  ;

L15: Symmetry ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳

L06⊳L14⊳L09⊳L10⊳L12 ≫ R(Y, X) ;

L16: EqSubset ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳ L07 ⊳ ⊳

L08⊳L10⊳L09⊳L11⊳L15 ≫ s ∈ [Y ∈ BS]_{R} ⇒ s ∈ [X ∈ BS]_{R} ;

L17: ToSetEquality ⊳ L13 ⊳ L16 ≫  [X ∈ BS]_{R} =[Y ∈ BS]_{R}  ;
L18: Block ≫  End  ;
L19: Arbitrary ≫  R, X , Y, BS  ;

L20: Ded ⊳ L18 ≫

s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢
t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢
X ∈ BS ⇒ Y ∈ BS ⇒
EqRel(R, BS) ⇒ R(X , Y) ⇒
[X ∈ BS]_{R} =[Y ∈ BS]_{R} □

Vi mangler nu blot at skifte fra implikationer til inferenser:

[ZFsub lemma EqNecessary: ΠR, X , Y, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ X ∈ BS ⊢ Y ∈ BS ⊢ EqRel(R, BS) ⊢ R(X , Y) ⇒ [X ∈ BS]_{R} =[Y ∈ BS]_{R}]

ZFsub proof of EqNecessary:

L01: Arbitrary ≫  R, X , Y, BS  ;
L02: Side-condition ≫  s#R  ;
L03: Side-condition ≫  s#BS  ;
L04: Side-condition ≫  t#R  ;
L05: Side-condition ≫  t#BS  ;
L06: Side-condition ≫  u#R  ;
L07: Side-condition ≫  u#BS  ;
L08: Premise ≫  X ∈ BS  ;
L09: Premise ≫  Y ∈ BS  ;
L10: Premise ≫  EqRel(R, BS)  ;

L11: HelperEqNecessary ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳

L07 ≫ X ∈ BS ⇒ Y ∈ BS ⇒ EqRel(R, BS) ⇒ R(X , Y) ⇒ [X ∈ BS]_{R} =[Y ∈ BS]_{R} ;

L12: MP3⊳L11⊳L08⊳L09⊳L10 ≫ {R(X , Y) ⇒ \atop [X ∈ BS]_{R} =[Y ∈ BS]_{R}  □}

11.2.3 Lemmaet “NoneEqNecessary”

Resultatet fra dette under-underafsnit kan formuleres som følger: “Lad X og Y være to medlemmer af BS, som ikke opfylder R(X , Y). Da er de to ækvivalensklasser [X ∈ BS]_{R} og [Y ∈ BS]_{R} indbyrdes disjunkte.”^{21}

Vi viser dette ved at vise den kontrapositive påstand: Hvis ækvivalensklasserne har et medlem tilfælles, så gælder R(X , Y). Dette varetages af lemmaet HelperNoneEqNecessary:

[ZFsub lemma HelperNoneEqNecessary: ΠR, S, X , Y, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ X ∈ BS ⇒ Y ∈ BS ⇒ EqRel(R, BS) ⇒ S ∈ [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} ⇒ R(X , Y)]

Beviset for HelperEqNecessary kan beskrives som følger:

21Dette er lemma 4.4.b.1 i [5].

1. Antag at S tilhører både [X ∈ BS]_{R} og [Y ∈ BS]_{R}. Da gælder R(S, X) (linie 17–19) og R(S, Y) (linie 20–22).

2. Da R er symmetrisk, følger R(X , S) af R(S, X). (Linie 24).

3. Da R også er transitiv, medfører R(X , S) og R(S, Y) tilsammen R(X , Y), QED. (Linie 25).

Her er selve beviset:

ZFsub proof of HelperNoneEqNecessary:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, S, X , Y, BS  ;
L03: Side-condition ≫  s#R  ;
L04: Side-condition ≫  s#BS  ;
L05: Side-condition ≫  t#R  ;
L06: Side-condition ≫  t#BS  ;
L07: Side-condition ≫  u#R  ;
L08: Side-condition ≫  u#BS  ;
L09: Premise ≫  X ∈ BS  ;
L10: Premise ≫  Y ∈ BS  ;
L11: Premise ≫  EqRel(R, BS)  ;
L12: Premise ≫  S ∈ [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R}  ;
L13: ERisSymmetric ⊳ L11 ≫  SymRel(R, BS)  ;
L14: ERisTransitive ⊳ L11 ≫  TransRel(R, BS)  ;
L15: Sep2Formula ⊳ L12 ≫  S ∈ [X ∈ BS]_{R} ∪ [Y ∈ BS]_{R} ˙∧ ; (S ∈ [X ∈ BS]_{R} ˙∧ ; S ∈ [Y ∈ BS]_{R})  ;

L16: SecondConjunct ⊳ L15 ≫  {S ∈ [X ∈ BS]_{R} ˙∧ \atop S ∈ [Y ∈ BS]_{R}  ;}
L17: FirstConjunct ⊳ L16 ≫  S ∈ [X ∈ BS]_{R}  ;
L18: Sep2Formula ⊳ L17 ≫  S ∈ BS ˙∧ R(S, X)  ;
L19: SecondConjunct ⊳ L18 ≫  R(S, X)  ;
L20: SecondConjunct ⊳ L16 ≫  S ∈ [Y ∈ BS]_{R}  ;
L21: Sep2Formula ⊳ L20 ≫  S ∈ BS ˙∧ R(S, Y)  ;
L22: SecondConjunct ⊳ L21 ≫  R(S, Y)  ;
L23: FirstConjunct ⊳ L18 ≫  S ∈ BS  ;

L24: Symmetry ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳

L06⊳L13⊳L23⊳L09⊳L19 ≫ R(X , S) ;

L25: Transitivity ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳ L07 ⊳ ⊳ L08 ⊳ L14 ⊳ L09 ⊳ L23 ⊳ L10 ⊳

L24 ⊳ L22 ≫ R(X , Y) ;

L26: Block ≫  End  ;
L27: Arbitrary ≫  R, S, X , Y, BS  ;

L28: Ded ⊳ L26 ≫

s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢
t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢
X ∈ BS ⇒ Y ∈ BS ⇒
EqRel(R, BS) ⇒
S ∈ [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} ⇒
R(X , Y) □

Vi bruger nu modus tollens til at vise en kontrapositiv version af HelperNoneEqNecessary. Dette sker i beviset for en lemmastump ved navn Helper(2)NoneEqNecessary:

[ZFsub lemma Helper(2)NoneEqNecessary: ΠR, X , Y, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ X ∈ BS ⇒ Y ∈ BS ⇒ EqRel(R, BS) ⇒ ˙¬ R(X , Y) ⇒ [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} =Ø]

ZFsub proof of Helper(2)NoneEqNecessary:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, X , Y, BS  ;
L03: Side-condition ≫  s#R  ;
L04: Side-condition ≫  s#BS  ;
L05: Side-condition ≫  t#R  ;
L06: Side-condition ≫  t#BS  ;
L07: Side-condition ≫  u#R  ;
L08: Side-condition ≫  u#BS  ;
L09: Premise ≫  X ∈ BS  ;
L10: Premise ≫  Y ∈ BS  ;
L11: Premise ≫  EqRel(R, BS)  ;
L12: Premise ≫  ˙¬ R(X , Y)  ;

L13: HelperNoneEqNecessary ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳

L07 ⊳ ⊳ L08 ≫ X ∈ BS ⇒ Y ∈ BS ⇒ EqRel(R, BS) ⇒ s ∈ [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} ⇒ R(X , Y) ;

L14: MP3⊳L13⊳L09⊳L10⊳L11 ≫  {s ∈ [X ∈ BS]_{R} ∩ [Y ∈ \atop BS]_{R} ⇒ R(X , Y)  ;}
L15: MT ⊳ L14 ⊳ L12 ≫  s ∉ [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} ;
L16: UniqueØ ⊳ L15 ≫  [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} =Ø ;
L17: Block ≫  End  ;
L18: Arbitrary ≫  R, X , Y, BS  ;

L19: Ded ⊳ L17 ≫ s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ X ∈ BS ⇒ Y ∈ BS ⇒ EqRel(R, BS) ⇒ ˙¬ R(X , Y) ⇒ [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} =Ø □ I beviset for hovedlemmaet NoneEqNecessary foretager vi den sædvanlige konvertering fra [x ⇒ y] til [x ⊢ y]:

[ZFsub lemma NoneEqNecessary: ΠR, X , Y, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ X ∈ BS ⊢ Y ∈ BS ⊢ EqRel(R, BS) ⊢ ˙¬ R(X , Y) ⇒ [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} =Ø]

ZFsub proof of NoneEqNecessary:

L01: Arbitrary ≫  R, X , Y, BS  ;
L02: Side-condition ≫  s#R  ;
L03: Side-condition ≫  s#BS  ;
L04: Side-condition ≫  t#R  ;
L05: Side-condition ≫  t#BS  ;
L06: Side-condition ≫  u#R  ;
L07: Side-condition ≫  u#BS  ;
L08: Premise ≫  X ∈ BS  ;
L09: Premise ≫  Y ∈ BS  ;
L10: Premise ≫  EqRel(R, BS)  ;

L11: Helper(2)NoneEqNecessary ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳

L06 ⊳ ⊳ L07 ≫ X ∈ BS ⇒ Y ∈ BS ⇒ EqRel(R, BS) ⇒ ˙¬ R(X , Y) ⇒ [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} =Ø ;

L12: MP3⊳L11⊳L08⊳L09⊳L10 ≫ {˙¬ R(X , Y) ⇒ \atop [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} =Ø  □}

11.2.4 To ækvivalensklasser er disjunkte

Vi kan nu bevise, at to forskellige ækvivalensklasser er disjunkte:

[ZFsub lemma EqClassesAreDisjoint: ΠR, X , Y, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ X ∈ BS ⊢ Y ∈ BS ⊢ EqRel(R, BS) ⊢ [X ∈ BS]_{R} ≠ [Y ∈ BS]_{R} ⊢ [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} =Ø]

Beviset for EqClassesAreDisjoint forløber som følger:

1. Vi antager, at [X ∈ BS]_{R} og [Y ∈ BS]_{R} ikke er lig med hinanden. Fra EqNecessary ved vi, at hvis der gjaldt R(X , Y), så ville [X ∈ BS]_{R} og [Y ∈ BS]_{R} være lig med hinanden. Derfor må der gælde ˙¬ R(X , Y). (Linie 12–13).

2. Fra NoneEqNecessary ved vi, at ˙¬ R(X , Y) medfører, at de to ækvivalensklasser er disjunkte; QED. (Linie 14–15).

Her er beviset:

ZFsub proof of EqClassesAreDisjoint:

L01: Arbitrary ≫  R, X , Y, BS  ;

L02: Side-condition ≫  s#R  ;
L03: Side-condition ≫  s#BS  ;
L04: Side-condition ≫  t#R  ;
L05: Side-condition ≫  t#BS  ;
L06: Side-condition ≫  u#R  ;
L07: Side-condition ≫  u#BS  ;
L08: Premise ≫  X ∈ BS  ;
L09: Premise ≫  Y ∈ BS  ;
L10: Premise ≫  EqRel(R, BS)  ;
L11: Premise ≫  [X ∈ BS]_{R} ≠ [Y ∈ BS]_{R}  ;

L12: EqNecessary ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳

L07 ⊳ L08 ⊳ L09 ⊳ L10 ≫ R(X , Y) ⇒ [X ∈ BS]_{R} =[Y ∈ BS]_{R} ;

L13: MT ⊳ L12 ⊳ L11 ≫  ˙¬ R(X , Y)  ;

L14: NoneEqNecessary ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳

L07 ⊳ L08 ⊳ L09 ⊳ L10 ≫ ˙¬ R(X , Y) ⇒ [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} =Ø ;

L15: MP ⊳ L14 ⊳ L13 ≫  [X ∈ BS]_{R} ∩ [Y ∈ BS]_{R} =Ø  □

11.2.5 Alle ækvivalensklasser er disjunkte

Ud fra EqClassesAreDisjoint kan vi nu vise, at alle medlemmer af et ækvivalenssystem er parvis disjunkte. Da beviset afhænger af SameIntersection, som igen afhænger af SameBinaryUnion, bruger vi objektvariable (jvf. afsnit 10.4):

[ZFsub lemma AllDisjoint: EqRel(r, OBS) ⊢ x ∈ OBS/r ⊢ y ∈ OBS/r ⊢ x ≠ y ⊢ x ∩ y =Ø]

Beviset forløber som følger:

1. Lad x og y være to forskellige medlemmer af et ækvivalenssystem OBS/r (linie 2–4).

2. Mængden x må være en ækvivalensklasse; vi kan altså skrive x =[Ex_{1} ∈ OBS]_{r} for et Ex_{1}, som tilhører OBS. (Linie 5–9).

3. Det samme gælder for y; her skriver vi y =[Ex_{2} ∈ OBS]_{r}. (Linie 10–14).

4. Da x og y er forskellige, må [Ex_{1} ∈ OBS]_{r} og [Ex_{2} ∈ OBS]_{r} også være forskellige. (Linie 15).

5. Heraf følger, at fællesmængden mellem [Ex_{1} ∈ OBS]_{r} og [Ex_{2} ∈ OBS]_{r} er tom. (Linie 16).

6. Af lighedslemmaet SameIntersection får vi x ∩ y =[Ex_{1} ∈ OBS]_{r} ∩ [Ex_{1} ∈ OBS]_{r}. (Linie 17).

7. Da [Ex_{1} ∈ OBS]_{r} ∩ [Ex_{1} ∈ OBS]_{r} er tom (punkt 5), må x ∩ y derfor også være tom, QED. (Linie 18).

Her er beviset:

ZFsub proof of AllDisjoint:

L01: Premise ≫  EqRel(r, OBS)  ;
L02: Premise ≫  x ∈ OBS/r  ;
L03: Premise ≫  y ∈ OBS/r  ;
L04: Premise ≫  x ≠ y  ;

L05: Sep2Formula ⊳ L02 ≫

x ∈ P(OBS) ˙∧ (Ex_{1} ∈ OBS ˙∧
[Ex_{1} ∈ OBS]_{r} =x) ;
L06: SecondConjunct ⊳ L05 ≫  Ex_{1} ∈ OBS ˙∧ [Ex_{1} ∈ OBS]_{r} =x ;
L07: FirstConjunct ⊳ L06 ≫  Ex_{1} ∈ OBS  ;
L08: SecondConjunct ⊳ L06 ≫  [Ex_{1} ∈ OBS]_{r} =x  ;
L09: =Symmetry ⊳ L08 ≫  x =[Ex_{1} ∈ OBS]_{r}  ;

L10: Sep2Formula ⊳ L03 ≫

y ∈ P(OBS) ˙∧ (Ex_{2} ∈ OBS ˙∧
[Ex_{2} ∈ OBS]_{r} =y) ;
L11: SecondConjunct ⊳ L10 ≫  Ex_{2} ∈ OBS ˙∧ [Ex_{2} ∈ OBS]_{r} =y ;
L12: FirstConjunct ⊳ L11 ≫  Ex_{2} ∈ OBS  ;
L13: SecondConjunct ⊳ L11 ≫  [Ex_{2} ∈ OBS]_{r} =y  ;
L14: =Symmetry ⊳ L13 ≫  y =[Ex_{2} ∈ OBS]_{r}  ;

L15: TransferNotEq ⊳ L04 ⊳ L09 ⊳ L14 ≫

[Ex_{1} ∈ OBS]_{r} ≠ [Ex_{2} ∈ OBS]_{r} ;

L16: EqClassesAreDisjoint ⊳ L07 ⊳

L12 ⊳ L01 ⊳ L15 ≫ [Ex_{1} ∈ OBS]_{r} ∩ [Ex_{2} ∈ OBS]_{r} =

Ø ;

L17: SameIntersection⊳L09⊳L14 ≫

x ∩ y =

[Ex_{1} ∈ OBS]_{r} ∩ [Ex_{2} ∈ OBS]_{r} ;

L18: =Transitivity ⊳ L17 ⊳ L16 ≫ x ∩ y =Ø  □

Bemærk at vi i dette bevis introducerer både Ex_{1} og Ex_{2} ud fra definitionen af [OBS/r], selvom denne definition bruger eksistensvariablen Ex_{20}. Vi nyder her gavn af, at separationsaksiomet tillader introduktion af ubrugte eksistensvariable (som nævnt i afsnit 4.2.1).

11.2.6 Implikation i stedet for inferens

Det sidste skridt i dette afsnit er at skifte inferenserne fra AllDisjoint ud med implikationer. (Dette er påkrævet for, at resultatet fra AllDisjoint kan bruges i beviset for hovedresultatet). Vi plejer jo at bruge deduktionsreglen til dén slags konverteringer; men der et problem. Vi kan ikke konkludere

[EqRel(r, OBS) ⇒ x ∈ OBS/r ⇒ y ∈ OBS/r ⇒ x ≠ y ⇒ x ∩ y =Ø]

ud fra Ded; vi kan kun konkludere

[∀r, OBS: EqRel(r, OBS) ⇒ ∀r, x, OBS: x ∈ OBS/r ⇒ ∀r, y, OBS: y ∈ OBS/r ⇒ ∀x, y: x ≠ y ⇒ x ∩ y =Ø].

Deduktionsreglen tillader altså ikke frie objektvariable i antecedenterne. Dette er også et rimeligt krav; ellers ville vi f.eks. kunne slutte den falske implikation [s =Ø ⇒ ∀s: s =Ø] ud fra lemmaet [s =Ø ⊢ ∀s: s =Ø]. Problemet er, at beviset for hovedresultatet kræver, at implikationen er renset for objektkvantorer. Så vi er altså havnet i en blindgyde.

Vi løser problemet ved at indføre følgende “snyde-aksiom”:

[ZFsub rule CheatAllDisjoint: ΠR, X , Y, BS: EqRel(R, BS) ⊢ X ∈ BS/R ⊢ Y ∈ BS/R ⊢ X ≠ Y ⊢ X ∩ Y =Ø]

I CheatAllDisjoint formulerer vi AllDisjoint ved hjælp af metavariable. Vi kan opfatte CheatAllDisjoint som dét resultat, vi var nået frem til, hvis vi havde kæmpet videre med de mange sidebetingelser (bortset fra at der ikke er nogen sidebetingelser i formuleringen af CheatAllDisjoint). Ud fra denne formulering af AllDisjoint er det nemt at aflede en implikation:

[ZFsub lemma AllDisjointImply: ΠR, X , Y, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ EqRel(R, BS) ⇒ X ∈ BS/R ⇒ Y ∈ BS/R ⇒ X ≠ Y ⇒ X ∩ Y =Ø]

ZFsub proof of AllDisjointImply:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, X , Y, BS  ;
L03: Premise ≫  EqRel(R, BS)  ;
L04: Premise ≫  X ∈ BS/R  ;
L05: Premise ≫  Y ∈ BS/R  ;
L06: Premise ≫  X ≠ Y  ;

L07: CheatAllDisjoint ⊳ L03 ⊳

L04 ⊳ L05 ⊳ L06 ≫ X ∩ Y =Ø ;

L08: Block ≫  End  ;
L09: Arbitrary ≫  R, X , Y, BS  ;

L10: Ded ⊳ L08 ≫

s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢
t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢
EqRel(R, BS) ⇒ X ∈ BS/R ⇒
Y ∈ BS/R ⇒ X ≠ Y ⇒
X ∩ Y =Ø □

Vores brug af metavariable betyder, at sidebetingelserne straks vender tilbage — dog i et tåleligt omfang. Det er lemmaet AllDisjointImply, som vi kommer til at bruge i beviset for EqSysIsPartition.

11.3 Ækvivalensklassernes foreningsmængde

I dette underafsnit viser vi først, at BS er en delmængde af ækvivalensklassernes foreningsmængde ∪(BS/R) (under-underafsnit 11.3.1), og vice versa (underunderafsnit 11.3.2). Herudfra kan vi let vise, at de to mængder er lig hinanden (under-underafsnit 11.3.3).

11.3.1 Den ene halvdel

Lemmaet EqClassIsSubset udsiger, at en ækvivalensklasse [X ∈ BS]_{R} defineret på en mængde BS er en delmængde af BS:

[ZFsub lemma EqClassIsSubset: ΠR, S, X , BS: S ∈ [X ∈ BS]_{R} ⇒ S ∈ BS]

Lemmaet følger direkte af definitionen af [[X ∈ BS]_{R}] fra afsnit 5.9:

ZFsub proof of EqClassIsSubset:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, S, X , BS  ;
L03: Premise ≫  S ∈ [X ∈ BS]_{R}  ;
L04: Sep2Formula ⊳ L03 ≫  S ∈ BS ˙∧ R(S, X)  ;
L05: FirstConjunct ⊳ L04 ≫  S ∈ BS  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  R, S, X , BS  ;
L08: Ded ⊳ L06 ≫  S ∈ [X ∈ BS]_{R} ⇒ S ∈ BS  □

Kommet så vidt kan vi bevise, at BS er en delmængde af ∪(BS/R):

[ZFsub lemma BSsubset: ΠR, S, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ EqRel(R, BS) ⇒ S ∈ BS ⇒ S ∈ ∪(BS/R)]

Beviset for BSsubset falder i tre dele:

1. Lad S være et vilkårligt medlem af BS. Ud fra AutoMember har vi, at S tilhører sin egen ækvivalensklasse [S ∈ BS]_{R} (linie 6–7).

2. Videre har vi, at denne ækvivalensklasse tilhører ækvivalenssystemet BS/R (linie 8–13).

3. Ud fra punkt 1 og 2 og definitionen af “foreningsmængde” får vi, at S tilhører ækvivalenssystemets foreningsmængde ∪(BS/R), QED (linie 14–16).

Her er selve beviset:

ZFsub proof of BSsubset:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, S, BS  ;
L03: Side-condition ≫  s#R  ;
L04: Side-condition ≫  s#BS  ;
L05: Premise ≫  EqRel(R, BS)  ;
L06: Premise ≫  S ∈ BS  ;

L07: AutoMember ⊳ ⊳ L03 ⊳ ⊳

L04 ⊳ L05 ⊳ L06 ≫ S ∈ [S ∈ BS]_{R} ;

L08: EqClassIsSubset ≫  s ∈ [S ∈ BS]_{R} ⇒ s ∈ BS  ;
L09: SubsetInPower ⊳ L08 ≫  [S ∈ BS]_{R} ∈ P(BS)  ;
L10: =Reflexivity ≫  [S ∈ BS]_{R} =[S ∈ BS]_{R}  ;

L11: JoinConjuncts ⊳ L06 ⊳ L10 ≫  {S ∈ BS ˙∧ \atop [S ∈ BS]_{R} =[S ∈ BS]_{R}  ;}
L12: ExistIntro @ Ex_{1} @ S ⊳ L11 ≫  {Ex_{1} ∈ BS ˙∧ \atop [Ex_{1} ∈ BS]_{R} =[S ∈ BS]_{R}  ;}
L13: Formula2Sep ⊳ L09 ⊳ L12 ≫  [S ∈ BS]_{R} ∈ BS/R  ;

L14: ExistIntro @ Ex_{10} @

[S ∈ BS]_{R} ⊳ L07 ≫ S ∈ Ex_{10} ;

L15: ExistIntro @ Ex_{10} @

[S ∈ BS]_{R} ⊳ L13 ≫ Ex_{10} ∈ BS/R ;

L16: Formula2Union ⊳ L14 ⊳ L15 ≫  S ∈ ∪(BS/R)  ;
L17: Block ≫  End  ;
L18: Arbitrary ≫  R, S, BS  ;

L19: Ded ⊳ L17 ≫

s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢
t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢
EqRel(R, BS) ⇒ S ∈ BS ⇒
S ∈ ∪(BS/R) □

I beviset bruger vi for første gang slutningsreglen ExistIntro. Vi anvender her konstruktionen [x @ y] til at fortælle bevischeckeren, hvordan metavariablene X og T i ExistIntro skal instantieres. Dette kan bevischeckeren ikke selv finde frem til, da både “X ” og “T ” kun optræder i reglens sidebetingelse. Det er med andre ord det samme problem som ved separationsaksiomet i afsnit 4.2.1, som vi her har løst på en anden måde.

11.3.2 Den anden halvdel

Vi viser nu det modsatte resultat af BSsubset: BS er en delmængde af ∪(BS/R):

[ZFsub lemma Union(BS/R)subset: ΠR, S, BS: s#BS ⊢⊢ s#R ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ EqRel(R, BS) ⇒ S ∈ ∪(BS/R) ⇒ S ∈ BS]

Beviset for Union(BS/R)subset kan opdeles i fire dele:

1. Lad S være et medlem af ∪(BS/R). [S] må tilhøre en ækvivalensklasse, som vi kalder for Ex_{10} (linie 5–7).

2. [Ex_{10}] tilhører ækvivalenssystemet BS/R, som igen er en delmængde af potensmængden P(BS). Derfor må Ex_{10} tilhøre P(BS) (linie 8–10).

3. Dette medfører igen, at Ex_{10} er en delmængde af BS (linie 11).

4. Ud fra punkt 1 og 3 får vi, at S tilhører BS, QED (linie 12–14).

Her er selve beviset:

ZFsub proof of Union(BS/R)subset:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  R, S, BS  ;
L03: Side-condition ≫  s#BS  ;

L04: Premise ≫  EqRel(R, BS)  ;
L05: Premise ≫  S ∈ ∪(BS/R)  ;
L06: Union2Formula ⊳ L05 ≫  S ∈ Ex_{10} ˙∧ Ex_{10} ∈ BS/R  ;
L07: FirstConjunct ⊳ L06 ≫  S ∈ Ex_{10}  ;
L08: SecondConjunct ⊳ L06 ≫  Ex_{10} ∈ BS/R  ;

L09: Sep2Formula ⊳ L08 ≫

Ex_{10} ∈ P(BS) ˙∧
(Ex_{1} ∈ BS ˙∧
[Ex_{1} ∈ BS]_{R} =Ex_{10}) ;
L10: FirstConjunct ⊳ L09 ≫ Ex_{10} ∈ P(BS) ;

L11: (Switch)PowerIsSub ⊳ ⊳

L03 ⊳ L10 ≫ Ex_{10} ⊆ BS ;

L12: Gen ⊳ L11 ≫ ∀s: (s ∈ Ex_{10} ⇒ s ∈ BS) ;

L13: (Switch)HelperPowerIsSub ⊳ ⊳

L03 ≫ ∀s: (s ∈ Ex_{10} ⇒ s ∈ BS) ⇒ S ∈ Ex_{10} ⇒ S ∈ BS ;

L14: MP2 ⊳ L13 ⊳ L12 ⊳ L07 ≫  S ∈ BS  ;
L15: Block ≫  End  ;
L16: Arbitrary ≫  R, S, BS  ;

L17: Ded ⊳ L15 ≫

s#BS ⊢⊢ s#R ⊢⊢ t#R ⊢⊢
t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢
EqRel(R, BS) ⇒
S ∈ ∪(BS/R) ⇒ S ∈ BS □

11.3.3 De to halvdele sættes sammen

Nu hvor vi har vist, at BS og ∪(BS/R) er hinandens delmængder, er det let at vise, at de er lig med hinanden:

[ZFsub lemma UnionIdentity: ΠR, BS: s#R ⊢⊢ s#BS ⊢⊢ t#R ⊢⊢ t#BS ⊢⊢ u#R ⊢⊢ u#BS ⊢⊢ EqRel(R, BS) ⊢ ∪ (BS/R)=BS]

ZFsub proof of UnionIdentity:

L01: Arbitrary ≫  R, BS  ;
L02: Side-condition ≫  s#R  ;
L03: Side-condition ≫  s#BS  ;
L04: Side-condition ≫  t#R  ;
L05: Side-condition ≫  t#BS  ;
L06: Side-condition ≫  u#R  ;
L07: Side-condition ≫  u#BS  ;
L08: Premise ≫  EqRel(R, BS)  ;

L09: BSsubset ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳ L07 ≫

EqRel(R, BS) ⇒ s ∈ BS ⇒ s ∈ ∪(BS/R) ;

L10: MP ⊳ L09 ⊳ L08 ≫  s ∈ BS ⇒ s ∈ ∪(BS/R)  ;

L11: Union(BS/R)subset ⊳ ⊳ L03 ⊳ ⊳ L02 ⊳ ⊳ L04 ⊳ ⊳ L05 ⊳ ⊳ L06 ⊳ ⊳

L07 ≫ EqRel(R, BS) ⇒ s ∈ ∪(BS/R) ⇒ s ∈ BS ;

L12: MP ⊳ L11 ⊳ L08 ≫  s ∈ ∪(BS/R) ⇒ s ∈ BS  ;
L13: ToSetEquality ⊳ L12 ⊳ L10 ≫ ∪(BS/R)=BS  □

11.4 Det sidste bevis

Rapportens sidste bevis vedrører naturligvis hovedresultatet:

[ZFsub lemma EqSysIsPartition: EqRel(r, OBS) ⊢ Partition(OBS/r, OBS)]

I beviset sammensætter vi resultaterne fra underafsnit 11.1 (linie 2–4), underafsnit 11.2 (linie 5–8) og underafsnit 11.3 (linie 9):

ZFsub proof of EqSysIsPartition:

L01: Premise ≫  EqRel(r, OBS)  ;
L02: EqSysNotØ ⊳ L01 ≫  x ∈ OBS/r ⇒ x ≠ Ø  ;
L03: Ded ⊳ L02 ≫  s ∈ OBS/r ⇒ s ≠ Ø  ;
L04: Gen ⊳ L03 ≫  ∀s: (s ∈ OBS/r ⇒ s ≠ Ø)  ;

L05: AllDisjointImply ≫ EqRel(r, OBS) ⇒ s ∈ OBS/r ⇒ t ∈ OBS/r ⇒ s ≠ t ⇒ s ∩ t =Ø ;

L06: MP ⊳ L05 ⊳ L01 ≫

s ∈ OBS/r ⇒ t ∈ OBS/r ⇒
s ≠ t ⇒ s ∩ t =Ø ;

L07: Gen ⊳ L06 ≫ ∀t: (s ∈ OBS/r ⇒ t ∈ OBS/r ⇒ s ≠ t ⇒ s∩t =Ø) ;

L08: Gen ⊳ L07 ≫ ∀s, t: (s ∈ OBS/r ⇒ t ∈ OBS/r ⇒ s ≠ t ⇒ s∩t =Ø) ;

L09: UnionIdentity ⊳ L01 ≫ ∪(OBS/r)=OBS ;

L10: JoinConjuncts ⊳ L04 ⊳ L08 ≫

(∀s: (s ∈ OBS/r ⇒ s ≠ Ø)) ˙∧
∀s, t: (s ∈ OBS/r ⇒
t ∈ OBS/r ⇒

s ≠ t ⇒ s ∩ t =Ø) ;

L11: JoinConjuncts ⊳ L10 ⊳ L09 ≫

(∀s: (s ∈ OBS/r ⇒ s ≠ Ø)) ˙∧
(∀s, t: (s ∈ OBS/r ⇒
t ∈ OBS/r ⇒
s ≠ t ⇒ s ∩ t = Ø)) ˙∧

∪(OBS/r)=OBS ;

L12: Repetition ⊳ L11 ≫  Partition(OBS/r, OBS)  □

Læg mærke til, at vi i linie 2 instantierer meta-variablen S i EqSysNotØ til objektvariablen x, selvom det egentlig er s, vi gerne ville have fat i. Dette skyldes, at EqSysNotØ indeholder sidebetingelsen [s#S] (jvf. afsnit 11.1). Vi løser problemet i linie 3, hvor deduktionsreglen skifter x ud med s. Deduktionsreglen tillader kun sådanne variabelskift, når der ikke er nogen metavariable i nærheden; det er derfor, at vi ikke tidligere har brugt reglen på denne måde.

12 Konklusion

Vi har ikke haft 100% succes med at bevise hovedresultatet; der måtte et “snydeaksiom” til hjælp. Problemet er, at systemet kræver et stort antal sidebetingelser for at sikre, at objekt- og metavariable undgår hinanden. Et spørgsmål er, om vi kunne have undgået dette problem ved at håndtere aksiomerne og definitionerne fra afsnit 4 og 5 anderledes. Her er en kort diskussion af et par alternative strategier:

Det er næppe holdbart kun at arbejde med objektvariable. Deduktionsreglen kan gennemføre variabelskift som f.eks. “y i stedet for x”, men ikke instantieringer som f.eks. “{y, z} i stedet for x”. (Jvf. formuleringen af SameIntersection i afsnit 10.6, hvor vi måtte instantiere objektvariablene “på forhånd”). Vi så også i afsnit 11.2.6, at det er svært at skifte fra inferens til implikation med objektvariable; deduktionsreglen kan ikke anvendes.

Det andet ekstrem er kun at arbejde med metavariable og -kvantorer. Man kunne da f.eks. formulere den ene halvdel af Extensionality som

[ΠX , Y: (ΠS: S ∈ X ˙⇔ S ∈ Y) ⊢ X =Y].

Logiwebs bevischecker er imidlertid ikke gearet til denne løsning, og det virker heller ikke som om, at vi på denne måde løser det egentlige problem: F.eks. giver det noget sludder, hvis vi instantierer “S” til “X ” i det ovenstående. Den samme kritik kan rettes mod forslaget “lad objektkvantorerne binde metavariable i stedet for objektvariable”.

Den bedste løsning må derfor være at lade bevischeckeren få ansvaret for at administrere sidebetingelserne, således at brugeren kun lægger mærke til dem, hvis han overtræder dem. Jeg har imidlertid ikke noget overblik over, hvor krævende det er at implementere denne løsning.

Min anden hovedkonklusion er, at deduktionsreglen skal suppleres med A4 fra [6], hvis eksistenskvantorer skal håndteres tilfredsstillende. Min løsning med eksistens-variable har fungeret i denne rapport, men det er ikke nogen sikker metode. Der er f.eks. intet, som forhindrer brugeren i at introducere allerede brugte eksistens-variable og dermed opnå systemets godkendelse af et ukorrekt bevis. Det er et åbent spørgsmål, hvor brugervenlig kombinationen “Ded og A4” er; den interesserede læser skal være velkommen til at gøre sine egne erfaringer.

Litteratur

[1] Frederik Eriksen. Et bevis i peano aritmetik, 2005. Logiwebdokument tilgængelig på hjemmesiden: http://www.diku.dk/

~grue/logiweb/20050502/home/eriksen/peano-commutativity/
GRD-2005-06-29-UTC-11-26-23-740136.

[2] Derek Goldrei. Classic Set Theory — For Guided Independent Study. Chapman & Hall, 1996.

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

på hjemmesiden: http://www.diku.dk/~grue/logiweb/20060417/home/
grue/base/GRD-2006-06-06-UTC-07-18-19-012409.

[4] Klaus Grue. The logiweb sequent calculus. Logiweb-dokument tilgængelig

på hjemmesiden: http://www.diku.dk/~grue/logiweb/20060417/home/
grue/check/GRD-2006-06-06-UTC-07-49-23-045248. Dokumentet er for-

delt på tre .pdf-filer, hvis adresser (relativt til den ovenstående adresse) er: body/tex/page.pdf, body/tex/appendix.pdf og body/tex/chores.pdf. De to første filer er så langt de vigtigste.

[5] Karel Hrbacek and Thomas Jech. Introduction to Set Theory. Marcel Dekker, third edition, 1999.

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

A Oversigt over variabelnavne

• De fire vigtigste objektvariable er: [s], [t], [u] og [OBS].

• Eksistens-variablen [Ex_{10}] bruges i aksiomet [UnionDef] fra afsnit 4.2.

• Ekistens-variablen [Ex_{20}] bruges i definitionen af [bs/r] fra afsnit 5.9.

• Eksistens-variablene [Ex_{1}] og [Ex_{2}] bruges i beviser, når [Ex_{10}] eller [Ex_{20}] ikke er påkrævede.

• Pladsholder-variablen [ph_{1}] bruges i definitionen af [[x ∈ bs]_{r}] fra afsnit 5.9.

• Pladsholder-variablen [ph_{2}] bruges i definitionen af [bs/r] fra afsnit 5.9.

• Pladsholder-variablen [ph_{3}] bruges i definitionen af [x ∩ y] fra afsnit 5.5.

• Metavariablene [A], [B] ⋯ [F] varierer over formler.

• Metavariabelene [R], [S] ⋯ [Z] samt [BS] varierer over termer. ([R] står altid for en relation).

• Metavariablen [P] varierer over pladsholder-variable.

• Endelig kan de “rå” variable [a], [b] ⋯ [z] samt [bs] variere over hvad som helst; disse variable er ikke tilknyttet nogen semantik.

B Det samlede aksiomsystem

[ZFsub rule MP: ΠA, B: A ⇒ B ⊢ A ⊢ B] [ZFsub rule Gen: ΠX , A: A ⊢ ∀X: A] [ZFsub rule Repetition: ΠA: A ⊢ A] [ZFsub rule Neg: ΠA, B: ˙¬ B ⇒ A ⊢ ˙¬ B ⇒ ˙¬ A ⊢ B] [ZFsub rule Ded: ΠA, B: Dedu(A, B) ⊢⊢ A ⊢ B] [ZFsub rule ExistIntro: ΠX , T , A, B: ⟨A≡B|X:=T ⟩_{Ex} ⊢⊢ A ⊢ B] [ZFsub rule Extensionality: ΠX , Y: X =Y ˙⇔ ∀s: (s ∈ X ˙⇔ s ∈ Y)] [ZFsub rule Ødef: ΠS: ˙¬ S ∈ Ø] [ZFsub rule PairDef: ΠS, X , Y: S ∈ {X , Y} ˙⇔ S =X ˙∨ S =Y] [ZFsub rule UnionDef: ΠS, X: S ∈ ∪X ˙⇔ (S ∈ Ex_{10} ˙∧ Ex_{10} ∈ X)] [ZFsub rule PowerDef: ΠS, X: S ∈ P(X) ˙⇔ ∀s: (s ∈ S ⇒ s ∈ X)] [ZFsub rule SeparationDef: ΠA, B, P, X , Z: P^{Ph} ∧ ⟨B≡A|P:=Z⟩_{Ph} ⊢⊢ Z ∈ {ph ∈ X | A} ˙⇔ Z ∈ X ˙∧ B] [ZFsub rule CheatAllDisjoint: ΠR, X , Y, BS: EqRel(R, BS) ⊢ X ∈ BS/R ⊢ Y ∈ BS/R ⊢ X ≠ Y ⊢ X ∩ Y =Ø]

C Deduktionsreglen

Dette bilag præsenterer dén version af deduktionsreglen fra [4], som jeg har brugt af. Underafsnit C.1 forklarer, hvorfor jeg har ændret på den oprindelige regel, og underafsnit C.2 indeholder selve den ændrede kode (som er skrevet i L).

C.1 Motivering

I beviset for HelperMemberNotØ i afsnit 9.1.3 konkluderer vi [s#X ⊢⊢ S ∈ X ⇒ X =Ø ⇒ S ∈ Ø] ud fra præmissen [s#X ⊢⊢ S ∈ X ⊢ X = Ø ⊢ S ∈ Ø] ved hjælp af deduktionsreglen; det er et klassisk skift fra inferens til implikation. Denne slutning kan imidlertid ikke gennemføres med deduktionsreglen fra [4], fordi denne regel fjerner alle sidebetingelser fra konklusionen, før præmis og konklusion sammenlignes. Da præmissen stadigvæk begynder med sidebetingelsen [s#X], matcher præmis og konklusion ikke hinanden, og slutningen fra præmis til konklusion forkastes. Deduktionsreglen fra dette bilag tillader derimod, at præmis og konklusion begynder med et antal identiske sidebetingelser. Dermed kan vi uden problemer gennemføre slutninger som den ovenstående, hvor præmissen indeholder sidebetingelser.

C.2 Kode

Funktionen [Dedu(p, c)] er en kopi af [Ded(p, c)] fra [4]:

[Dedu(p, c) ¨= λx.Dedu_{0}(⌈p⌉, ⌈c⌉)]

Jeg har ændret funktionen [Ded_{0}(p, c)], så den kalder [Dedu_{s}(Dedu_{7}(p), c, T)] i stedet for [Ded_{1}(Ded_{7}(p), c, T)]:

[Dedu_{0}(p, c) ˙= c!Dedu_{8}(p, T) ¨∧ Dedu_{s}(Dedu_{7}(p), c, T)]

Funktionen [Dedu_{s}(p, c, s)] giver straks kontrollen videre til [Ded_{1}(p, c, s)] — medmindre p og c begynder med et antal identiske sidebetingelser. I så fald flyttes disse sidebetingelser fra p og c over til listen s, før kontrollen går videre til [Ded_{1}(p, c, s)]:

[Dedu_{s}(p, c, s) ˙= if p =^{r} ⌈x ⊢⊢ y⌉ then c =^{r} ⌈x ⊢⊢ y⌉ ∧ p^{1} =^{t} c^{1} ∧ Dedu_{s}(p^{2}, c^{2}, c^{1} : : s) else Dedu_{1}(p, c, s)]

Fra og med [Ded_{1}(p, c, s)] er koden kopieret fra appendikset til [4]:

[Dedu_{1}(p, c, s) ˙= if c =^{r} ⌈x ⊢⊢ y⌉ then Dedu_{1}(p, c^{2}, c^{1} : : s) else Dedu_{2}(p, c, s)]

[Dedu_{2}(p, c, s) ˙= s!

p =^{r} ⌈x ⊢ y⌉ ∧ c =^{r} ⌈x ⇒ y⌉ \{ \begin{matrix}Dedu_{3}(p^{1}, c^{1}, s, T) ∧ Dedu_{2}(p^{2}, c^{2}, s) \\ Dedu_{4}(p, c, s, Dedu_{6}(p, c, T, T)) \end{matrix} ] [Dedu_{3}(p, c, s, b) ˙= if ¬c =^{r} ⌈∀x: y⌉ then Dedu_{4}(p, c, s, b) else if p =^{r} ⌈∀x: y⌉ ∧ p^{1} =^{t} c^{1} then Dedu_{4}(p, c, s, b) else Dedu_{3}(p, c^{2}, s, (c^{1} : : c^{1}) : : b)] [Dedu_{4}(p, c, s, b) ˙= s!b! if p =^{r} ⌈x⌉ then lookup(p, b, T) =^{t} c else if ¬p =^{r} c then F else if p =^{r} ⌈∀x: y⌉ then p^{1} =^{t} c^{1} ∧ Dedu_{4}(p^{2}, c^{2}, s, (p^{1} : : p^{1}) : : b) else if ¬p =^{r} ⌈X ⌉ then Dedu_{4}^{∗}(p^{t}, c^{t}, s, b) else p^{1} =^{t} c^{1} ∧ Dedu_{5}(p, s, b)] [Dedu_{4}^{∗}(p, c, s, b) ˙= c!s!b!if p then T else Dedu_{4}(p^{h}, c^{h}, s, b) ∧ Dedu_{4}^{∗}(p^{t}, c^{t}, s, b)] [Dedu_{5}(p, s, b) ˙= p!s!if b then T else ⟨⌈x#y⌉^{h}, ⟨⌈⌈∗⌉⌉^{h}, b^{h}^{h}⟩, ⟨⌈⌈x⌉⌉^{h}, p⟩⟩ ∈_{t} s ∧ Dedu_{5}(p, s, b^{t})] [Dedu_{6}(p, c, e, b) ˙= p!c!b!e! if p =^{r} ⌈x⌉ then p ∈_{t} e \{ \begin{matrix}b \\ (p : : c) : : b \end{matrix} else if ¬p =^{r} c then T else if p =^{r} ⌈A⌉ then b else if p =^{r} ⌈∀x: y⌉ then Dedu_{6}(p^{2}, c^{2}, c^{1} : : e, b) else Dedu_{6}^{∗}(p^{t}, c^{t}, e, b)] [Dedu_{6}^{∗}(p, c, e, b) ˙= p!c!b!e!if p then b else Dedu_{6}^{∗}(p^{t}, c^{t}, e, Dedu_{6}(p^{h}, c^{h}, e, b))] [Dedu_{7}(p) ˙= p =^{r} ⌈Πx: y⌉ \{ \begin{matrix}Dedu_{7}(p^{2}) \\ p \end{matrix} ] [Dedu_{8}(p, b) ˙= if p =^{r} ⌈Πx: y⌉ then Dedu_{8}(p^{2}, p^{1} : : b) else if p =^{r} ⌈A⌉ then p ∈_{t} b else Dedu_{8}^{∗}(p^{t}, b)] [Dedu_{8}^{∗}(p, b) ˙= b!if p then T else Dedu_{8}(p^{h}, b) ¨∧ Dedu_{8}^{∗}(p^{t}, b)]

D Pyk definitioner

([(⋯) →^{pyk} “cdots”] [Objekt-var →^{pyk} “object-var”] [Ex-var →^{pyk} “ex-var”] [Ph-var →^{pyk} “ph-var”] [Værdi →^{pyk} “vaerdi”] [Variabel →^{pyk} “variabel”] [Op(∗) →^{pyk} “op " end op”] [Op(∗, ∗) →^{pyk} “op2 " comma " end op2”] [∗ ¨= ∗ →^{pyk} “define-equal " comma " end equal”] [ContainsEmpty(∗) →^{pyk} “contains-empty " end empty”] [Dedu(∗, ∗) →^{pyk} “1deduction " conclude " end 1deduction”] [Dedu_{0}(∗, ∗) →^{pyk} “1deduction zero " conclude " end 1deduction”] [Dedu_{s}(∗, ∗, ∗) →^{pyk} “1deduction side " conclude " condition " end 1deduction”] [Dedu_{1}(∗, ∗, ∗) →^{pyk} “1deduction one " conclude " condition " end 1deduction”] [Dedu_{2}(∗, ∗, ∗) →^{pyk} “1deduction two " conclude " condition " end 1deduction”] [Dedu_{3}(∗, ∗, ∗, ∗) →^{pyk} “1deduction three " conclude " condition " bound " end 1deduction”] [Dedu_{4}(∗, ∗, ∗, ∗) →^{pyk} “1deduction four " conclude " condition " bound " end 1deduction”] [Dedu_{4}^{∗}(∗, ∗, ∗, ∗) →^{pyk} “1deduction four star " conclude " condition " bound " end 1deduction”] [Dedu_{5}(∗, ∗, ∗) →^{pyk} “1deduction five " condition " bound " end 1deduction”] [Dedu_{6}(∗, ∗, ∗, ∗) →^{pyk} “1deduction six " conclude " exception " bound " end 1deduction”] [Dedu_{6}^{∗}(∗, ∗, ∗, ∗) →^{pyk} “1deduction six star " conclude " exception " bound " end 1deduction”] [Dedu_{7}(∗) →^{pyk} “1deduction seven " end 1deduction”] [Dedu_{8}(∗, ∗) →^{pyk} “1deduction eight " bound " end 1deduction”] [Dedu_{8}^{∗}(∗, ∗) →^{pyk} “1deduction eight star " bound " end 1deduction”]

[Ex_{1} →^{pyk} “ex1”]

[Ex_{2} →^{pyk} “ex2”]

[Ex_{10} →^{pyk} “ex10”]

[Ex_{20} →^{pyk} “ex20”]

[∗_{Ex} →^{pyk} “existential var " end var”] [∗^{Ex} →^{pyk} “" is existential var”] [⟨∗≡ ∗ | ∗:=∗⟩_{Ex} →^{pyk} “exist-sub " is " where " is " end sub”] [⟨∗≡^{0} ∗ | ∗:=∗⟩_{Ex} →^{pyk} “exist-sub0 " is " where " is " end sub”] [⟨∗≡^{1} ∗ | ∗:=∗⟩_{Ex} →^{pyk} “exist-sub1 " is " where " is " end sub”] [⟨∗≡^{∗} ∗ | ∗:=∗⟩_{Ex} →^{pyk} “exist-sub∗ " is " where " is " end sub”] [ph_{1} →^{pyk} “placeholder-var1”] [ph_{2} →^{pyk} “placeholder-var2”] [ph_{3} →^{pyk} “placeholder-var3”] [∗_{Ph} →^{pyk} “placeholder-var " end var”] [∗^{Ph} →^{pyk} “" is placeholder-var”] [⟨∗≡ ∗ | ∗:=∗⟩_{Ph} →^{pyk} “ph-sub " is " where " is " end sub”] [⟨∗≡^{0} ∗ | ∗:=∗⟩_{Ph} →^{pyk} “ph-sub0 " is " where " is " end sub”] [⟨∗≡^{1} ∗ | ∗:=∗⟩_{Ph} →^{pyk} “ph-sub1 " is " where " is " end sub”] [⟨∗≡^{∗} ∗ | ∗:=∗⟩_{Ph} →^{pyk} “ph-sub∗ " is " where " is " end sub”] [bs →^{pyk} “var big set”] [OBS →^{pyk} “object big set”] [BS →^{pyk} “meta big set”] [Ø →^{pyk} “zermelo empty set”] [ZFsub →^{pyk} “system zf”] [MP →^{pyk} “1rule mp”] [Gen →^{pyk} “1rule gen”] [Repetition →^{pyk} “1rule repetition”] [Neg →^{pyk} “1rule ad absurdum”] [Ded →^{pyk} “1rule deduction”] [ExistIntro →^{pyk} “1rule exist intro”] [Extensionality →^{pyk} “axiom extensionality”] [Ødef →^{pyk} “axiom empty set”] [PairDef →^{pyk} “axiom pair definition”] [UnionDef →^{pyk} “axiom union definition”] [PowerDef →^{pyk} “axiom power definition”] [SeparationDef →^{pyk} “axiom separation definition”] [CheatAllDisjoint →^{pyk} “cheating axiom all disjoint”] [AddDoubleNeg →^{pyk} “prop lemma add double neg”] [RemoveDoubleNeg →^{pyk} “prop lemma remove double neg”] [AndCommutativity →^{pyk} “prop lemma and commutativity”] [AutoImply →^{pyk} “prop lemma auto imply”] [Contrapositive →^{pyk} “prop lemma contrapositive”] [FirstConjunct →^{pyk} “prop lemma first conjunct”] [SecondConjunct →^{pyk} “prop lemma second conjunct”] [FromContradiction →^{pyk} “prop lemma from contradiction”] [FromDisjuncts →^{pyk} “prop lemma from disjuncts”] [IffCommutativity →^{pyk} “prop lemma iff commutativity”] [IffFirst →^{pyk} “prop lemma iff first”] [IffSecond →^{pyk} “prop lemma iff second”] [ImplyTransitivity →^{pyk} “prop lemma imply transitivity”] [JoinConjuncts →^{pyk} “prop lemma join conjuncts”] [MP2 →^{pyk} “prop lemma mp2”] [MP3 →^{pyk} “prop lemma mp3”] [MP4 →^{pyk} “prop lemma mp4”] [MP5 →^{pyk} “prop lemma mp5”] [MT →^{pyk} “prop lemma mt”] [NegativeMT →^{pyk} “prop lemma negative mt”] [Technicality →^{pyk} “prop lemma technicality”] [Weakening →^{pyk} “prop lemma weakening”] [WeakenOr1 →^{pyk} “prop lemma weaken or first”] [WeakenOr2 →^{pyk} “prop lemma weaken or second”] [Formula2Pair →^{pyk} “lemma formula2pair”] [Pair2Formula →^{pyk} “lemma pair2formula”] [Formula2Union →^{pyk} “lemma formula2union”] [Union2Formula →^{pyk} “lemma union2formula”] [Formula2Sep →^{pyk} “lemma formula2separation”] [Sep2Formula →^{pyk} “lemma separation2formula”] [SubsetInPower →^{pyk} “lemma subset in power set”] [HelperPowerIsSub →^{pyk} “lemma power set is subset0”] [PowerIsSub →^{pyk} “lemma power set is subset”] [(Switch)HelperPowerIsSub →^{pyk} “lemma power set is subset0-switch”] [(Switch)PowerIsSub →^{pyk} “lemma power set is subset-switch”] [ToSetEquality →^{pyk} “lemma set equality suff condition”] [HelperToSetEquality(t) →^{pyk} “lemma set equality suff condition(t)0”] [ToSetEquality(t) →^{pyk} “lemma set equality suff condition(t)”] [HelperFromSetEquality →^{pyk} “lemma set equality skip quantifier”] [FromSetEquality →^{pyk} “lemma set equality nec condition”] [HelperReflexivity →^{pyk} “lemma reflexivity0”] [Reflexivity →^{pyk} “lemma reflexivity”] [HelperSymmetry →^{pyk} “lemma symmetry0”] [Symmetry →^{pyk} “lemma symmetry”] [HelperTransitivity →^{pyk} “lemma transitivity0”] [Transitivity →^{pyk} “lemma transitivity”] [ERisReflexive →^{pyk} “lemma er is reflexive”] [ERisSymmetric →^{pyk} “lemma er is symmetric”] [ERisTransitive →^{pyk} “lemma er is transitive”] [ØisSubset →^{pyk} “lemma empty set is subset”] [HelperMemberNotØ →^{pyk} “lemma member not empty0”] [MemberNotØ →^{pyk} “lemma member not empty”] [HelperUniqueØ →^{pyk} “lemma unique empty set0”] [UniqueØ →^{pyk} “lemma unique empty set”] [=Reflexivity →^{pyk} “lemma =reflexivity”] [=Symmetry →^{pyk} “lemma =symmetry”] [Helper=Transitivity →^{pyk} “lemma =transitivity0”] [=Transitivity →^{pyk} “lemma =transitivity”] [HelperTransferNotEq →^{pyk} “lemma transfer ˜ is0”] [TransferNotEq →^{pyk} “lemma transfer ˜ is”] [HelperPairSubset →^{pyk} “lemma pair subset0”] [Helper(2)PairSubset →^{pyk} “lemma pair subset1”] [PairSubset →^{pyk} “lemma pair subset”] [SamePair →^{pyk} “lemma same pair”] [SameSingleton →^{pyk} “lemma same singleton”] [UnionSubset →^{pyk} “lemma union subset”] [SameUnion →^{pyk} “lemma same union”] [SeparationSubset →^{pyk} “lemma separation subset”] [SameSeparation →^{pyk} “lemma same separation”] [SameBinaryUnion →^{pyk} “lemma same binary union”] [IntersectionSubset →^{pyk} “lemma intersection subset”] [SameIntersection →^{pyk} “lemma same intersection”] [AutoMember →^{pyk} “lemma auto member”] [HelperEqSysNotØ →^{pyk} “lemma eq-system not empty0”] [EqSysNotØ →^{pyk} “lemma eq-system not empty”] [HelperEqSubset →^{pyk} “lemma eq subset0”] [EqSubset →^{pyk} “lemma eq subset”] [HelperEqNecessary →^{pyk} “lemma equivalence nec condition0”] [EqNecessary →^{pyk} “lemma equivalence nec condition”] [HelperNoneEqNecessary →^{pyk} “lemma none-equivalence nec condition0”] [Helper(2)NoneEqNecessary →^{pyk} “lemma none-equivalence nec condition1”] [NoneEqNecessary →^{pyk} “lemma none-equivalence nec condition”] [EqClassIsSubset →^{pyk} “lemma equivalence class is subset”] [EqClassesAreDisjoint →^{pyk} “lemma equivalence classes are disjoint”] [AllDisjoint →^{pyk} “lemma all disjoint”] [AllDisjointImply →^{pyk} “lemma all disjoint-imply”] [BSsubset →^{pyk} “lemma bs subset union(bs/r)”] [Union(BS/R)subset →^{pyk} “lemma union(bs/r) subset bs”] [UnionIdentity →^{pyk} “lemma union(bs/r) is bs”] [EqSysIsPartition →^{pyk} “theorem eq-system is partition”] [∗/∗ →^{pyk} “eq-system of " modulo "”] [∗ ∩ ∗ →^{pyk} “intersection " comma " end intersection”] [∪∗ →^{pyk} “union " end union”] [∗ ∪ ∗ →^{pyk} “binary-union " comma " end union”] [P(∗) →^{pyk} “power " end power”] [{∗} →^{pyk} “zermelo singleton " end singleton”] [{∗, ∗} →^{pyk} “zermelo pair " comma " end pair”] [⟨∗, ∗⟩ →^{pyk} “zermelo ordered pair " comma " end pair”] [∗ ∈ ∗ →^{pyk} “" zermelo in "”] [∗(∗, ∗) →^{pyk} “" is related to " under "”] [ReflRel(∗, ∗) →^{pyk} “" is reflexive relation in "”] [SymRel(∗, ∗) →^{pyk} “" is symmetric relation in "”] [TransRel(∗, ∗) →^{pyk} “" is transitive relation in "”] [EqRel(∗, ∗) →^{pyk} “" is equivalence relation in "”] [[∗ ∈ ∗]_{∗} →^{pyk} “equivalence class of " in " modulo "”] [Partition(∗, ∗) →^{pyk} “" is partition of "”] [∗=∗ →^{pyk} “" zermelo is "”] [∗ ⊆ ∗ →^{pyk} “" is subset of "”]

[ ˙¬ ∗ →^{pyk} “not0 "”]

[∗ ∉ ∗ →^{pyk} “" zermelo ˜ in "”] [∗ ≠ ∗ →^{pyk} “" zermelo ˜ is "”]

[∗ ˙∧ ∗ →^{pyk} “" and0 "”]

[∗ ˙∨ ∗ →^{pyk} “" or0 "”]

[∗ ˙⇔ ∗ →^{pyk} “" iff "”]

[{ph ∈ ∗ | ∗} →^{pyk} “the set of ph in " such that " end set”] [EquivalenceRelations →^{pyk} “equivalence-relations”] )^{p}

E Prioritetstabel

Den nedenstående tabel indeholder alle de formelle konstruktioner, som er til rådighed i dette dokument. Konstruktionerne er grupperet efter prioritet; de førstnævnte grupper har størst prioritet. Hver gruppe er markeret med et af de to ord “Preassociative” eller “Postassociative”, der angiver, om konstruktionerne er venstre- eller højreassociative.

Priority table Preassociative [EquivalenceRelations], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [ $ ∗ $ ], [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}(∗, ∗)], [array-plus(∗, ∗)], [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̃^{∗}(∗, ∗, ∗)], [(∗)], [(∗)], [display(∗)], [statement(∗)], [[∗]^{·}], [[∗]^{−}], [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}(∗, ∗)], [check], [[∗ =^{∘} ∗]], [RootVisible(∗)], [A], [R], [C], [T], [L], [\{∗\}], [\overline{∗}], [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], [⟨∗≡ ∗ | ∗:=∗⟩], [⟨∗≡^{0} ∗ | ∗:=∗⟩], [⟨∗≡^{1} ∗ | ∗:=∗⟩], [⟨∗≡^{∗} ∗ | ∗:=∗⟩], [Ded(∗, ∗)], [Ded_{0}(∗, ∗)], [Ded_{1}(∗, ∗, ∗)], [Ded_{2}(∗, ∗, ∗)], [Ded_{3}(∗, ∗, ∗, ∗)], [Ded_{4}(∗, ∗, ∗, ∗)], [Ded_{4}^{∗}(∗, ∗, ∗, ∗)], [Ded_{5}(∗, ∗, ∗)], [Ded_{6}(∗, ∗, ∗, ∗)], [Ded_{6}^{∗}(∗, ∗, ∗, ∗)], [Ded_{7}(∗)], [Ded_{8}(∗, ∗)], [Ded_{8}^{∗}(∗, ∗)], [S], [Neg], [MP], [Gen], [Ded], [S1], [S2], [S3], [S4], [S5], [S6], [S7], [S8], [S9], [Repetition], [A1′], [A2′], [A4′], [A5′], [Prop 3.2a], [Prop 3.2b], [Prop 3.2c], [Prop 3.2d], [Prop 3.2e_{1}], [Prop 3.2e_{2}], [Prop 3.2e], [Prop 3.2f_{1}], [Prop 3.2f_{2}], [Prop 3.2f], [Prop 3.2g_{1}], [Prop 3.2g_{2}], [Prop 3.2g], [Prop 3.2h_{1}], [Prop 3.2h_{2}], [Prop 3.2h], [Block_{1}(∗, ∗, ∗)], [Block_{2}(∗)], [(⋯)], [Objekt-var], [Ex-var], [Ph-var], [Værdi], [Variabel], [Op(∗)], [Op(∗, ∗)], [∗ ¨= ∗], [ContainsEmpty(∗)], [Dedu(∗, ∗)], [Dedu_{0}(∗, ∗)], [Dedu_{s}(∗, ∗, ∗)], [Dedu_{1}(∗, ∗, ∗)], [Dedu_{2}(∗, ∗, ∗)], [Dedu_{3}(∗, ∗, ∗, ∗)], [Dedu_{4}(∗, ∗, ∗, ∗)], [Dedu_{4}^{∗}(∗, ∗, ∗, ∗)], [Dedu_{5}(∗, ∗, ∗)], [Dedu_{6}(∗, ∗, ∗, ∗)], [Dedu_{6}^{∗}(∗, ∗, ∗, ∗)], [Dedu_{7}(∗)], [Dedu_{8}(∗, ∗)], [Dedu_{8}^{∗}(∗, ∗)], [Ex_{1}], [Ex_{2}], [Ex_{10}], [Ex_{20}], [∗_{Ex}], [∗^{Ex}], [⟨∗≡ ∗ | ∗:=∗⟩_{Ex}], [⟨∗≡^{0} ∗ | ∗:=∗⟩_{Ex}], [⟨∗≡^{1} ∗ | ∗:=∗⟩_{Ex}], [⟨∗≡^{∗} ∗ | ∗:=∗⟩_{Ex}], [ph_{1}], [ph_{2}], [ph_{3}], [∗_{Ph}], [∗^{Ph}], [⟨∗≡ ∗ | ∗:=∗⟩_{Ph}], [⟨∗≡^{0} ∗ | ∗:=∗⟩_{Ph}], [⟨∗≡^{1} ∗ | ∗:=∗⟩_{Ph}], [⟨∗≡^{∗} ∗ | ∗:=∗⟩_{Ph}], [bs], [OBS], [BS], [Ø], [ZFsub], [MP], [Gen], [Repetition], [Neg], [Ded], [ExistIntro], [Extensionality], [Ødef], [PairDef], [UnionDef], [PowerDef], [SeparationDef], [CheatAllDisjoint], [AddDoubleNeg], [RemoveDoubleNeg], [AndCommutativity], [AutoImply], [Contrapositive], [FirstConjunct], [SecondConjunct], [FromContradiction], [FromDisjuncts], [IffCommutativity], [IffFirst], [IffSecond], [ImplyTransitivity], [JoinConjuncts], [MP2], [MP3], [MP4], [MP5], [MT], [NegativeMT], [Technicality], [Weakening], [WeakenOr1], [WeakenOr2], [Formula2Pair], [Pair2Formula], [Formula2Union], [Union2Formula], [Formula2Sep], [Sep2Formula], [SubsetInPower], [HelperPowerIsSub], [PowerIsSub], [(Switch)HelperPowerIsSub], [(Switch)PowerIsSub], [ToSetEquality], [HelperToSetEquality(t)], [ToSetEquality(t)], [HelperFromSetEquality], [FromSetEquality], [HelperReflexivity], [Reflexivity], [HelperSymmetry], [Symmetry], [HelperTransitivity], [Transitivity], [ERisReflexive], [ERisSymmetric], [ERisTransitive], [ØisSubset], [HelperMemberNotØ], [MemberNotØ], [HelperUniqueØ], [UniqueØ], [=Reflexivity], [=Symmetry], [Helper=Transitivity], [=Transitivity], [HelperTransferNotEq], [TransferNotEq], [HelperPairSubset], [Helper(2)PairSubset], [PairSubset], [SamePair], [SameSingleton], [UnionSubset], [SameUnion], [SeparationSubset], [SameSeparation], [SameBinaryUnion], [IntersectionSubset], [SameIntersection], [AutoMember], [HelperEqSysNotØ], [EqSysNotØ], [HelperEqSubset], [EqSubset], [HelperEqNecessary], [EqNecessary], [HelperNoneEqNecessary], [Helper(2)NoneEqNecessary], [NoneEqNecessary], [EqClassIsSubset], [EqClassesAreDisjoint], [AllDisjoint], [AllDisjointImply], [BSsubset], [Union(BS/R)subset], [UnionIdentity], [EqSysIsPartition]; Preassociative [∗ {∗}], [∗/indexintro(∗, ∗, ∗, ∗)], [∗/intro(∗, ∗, ∗)], [∗/bothintro(∗, ∗, ∗, ∗, ∗)], [∗/nameintro(∗, ∗, ∗, ∗)], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)], [∗^{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^{∗}}], [∗^{hide}]; 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 ∗], [MacroIndent(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗′]; Preassociative [∗/∗], [∗ ∩ ∗]; Preassociative [∪∗], [∗ ∪ ∗], [P(∗)]; Preassociative [{∗}]; Preassociative [{∗, ∗}], [⟨∗, ∗⟩]; Preassociative [∗ ∈ ∗], [∗(∗, ∗)], [ReflRel(∗, ∗)], [SymRel(∗, ∗)], [TransRel(∗, ∗)], [EqRel(∗, ∗)], [[∗ ∈ ∗]_{∗}], [Partition(∗, ∗)]; 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} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ = ∗], [∗ ≠ ∗], [∗^{var}], [∗#^{0}∗], [∗#^{1}∗], [∗#^{∗}∗], [∗=∗], [∗ ⊆ ∗]; Preassociative [¬∗], [ ˙¬ ∗], [∗ ∉ ∗], [∗ ≠ ∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗], [∗ ˙∧ ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗], [∗ ˙∨ ∗]; Preassociative [∃∗: ∗], [∀∗: ∗], [∀_{obj}∗: ∗]; Postassociative [∗ ¨⇒ ∗], [∗ ⇒ ∗], [∗ ⇔ ∗], [∗ ˙⇔ ∗]; Preassociative [{ph ∈ ∗ | ∗}]; Postassociative [∗ : ∗], [∗ spy ∗], [∗!∗]; Preassociative

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

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

F TEX definitioner

[EquivalenceRelations =^{tex} “EquivalenceRelations”]

[(⋯) =^{tex} “(\cdots{})”]

[Objekt-var =^{tex} “\texttt{Objekt-var}”]

[Ex-var =^{tex} “\texttt{Ex-var}”]

[Ph-var =^{tex} “\texttt{Ph-var}”]

[Værdi =^{tex} “\texttt{V\ae{}rdi}”]

[Variabel =^{tex} “\texttt{Variabel}”]

[Op(x) =^{tex} “Op(#1. )”]

[Op(x, y) =^{tex} “Op(#1. , #2. )”]

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

\mathrel {\ddot {=}} #2.”]

[ContainsEmpty(x) =^{tex} “ContainsEmpty(#1. )”]

[Dedu(x, y) =^{tex} “ Dedu(#1. , #2. )”] [Dedu_{0}(x, y) =^{tex} “ Dedu 0(#1. , #2. )”]

[Dedu_{s}(x, y, z) =^{tex} “Dedu {s}(#1. , #2. , #3. )”]

[Dedu_{1}(x, y, z) =^{tex} “ Dedu 1(#1. , #2. , #3. )”]

[Dedu_{2}(x, y, z) =^{tex} “ Dedu 2(#1. , #2. , #3. )”]

[Dedu_{3}(x, y, z, u) =^{tex} “ Dedu 3(#1. , #2. , #3. , #4. )”]

[Dedu_{4}(x, y, z, u) =^{tex} “ Dedu 4(#1. , #2. , #3. , #4. )”]

[Dedu_{4}^{∗}(x, y, z, u) =^{tex} “ Dedu 4ˆ ∗(#1. , #2. , #3. , #4. )”]

[Dedu_{5}(x, y, z) =^{tex} “ Dedu 5(#1. , #2. , #3. )”] [Dedu_{6}(p, c, e, b) =^{tex} “ Dedu 6(#1. , #2. , #3. , #4. )”]

[Dedu_{6}^{∗}(p, c, e, b) =^{tex} “ Dedu 6ˆ ∗(#1. , #2. , #3. , #4. )”]

[Dedu_{7}(p) =^{tex} “ Dedu 7(#1. )”]

[Dedu_{8}(p, b) =^{tex} “ Dedu 8(#1. , #2. )”]

[Dedu_{8}^{∗}(p, b) =^{tex} “ Dedu 8ˆ ∗(#1. , #2. )”]

[Ex_{1} =^{tex} “Ex {1}”]

[Ex_{2} =^{tex} “Ex {2}”]

[Ex_{10} =^{tex} “Ex {10}”]

[Ex_{20} =^{tex} “Ex {20}”]

[x_{Ex} =^{tex} “#1.

{Ex}”]

[x^{Ex} =^{tex} “#1.

ˆ {Ex}”]

[⟨x≡y|z:=u⟩_{Ex} =^{tex} “\langle #1. {\equiv} #2. | #3. {:=} #4. \rangle {Ex} ”]

[⟨x≡^{0}y|z:=u⟩_{Ex} =^{tex} “\langle #1. {\equiv}ˆ 0 #2.

| #3. {:=} #4. \rangle {Ex} ”]

[⟨x≡^{1}y|z:=u⟩_{Ex} =^{tex} “\langle #1. {\equiv}ˆ 1 #2. | #3. {:=} #4. \rangle {Ex} ”]

[⟨x≡^{∗}y|z:=u⟩_{Ex} =^{tex} “\langle #1. {\equiv}ˆ ∗ #2. | #3. {:=} #4. \rangle {Ex} ”]

[ph_{1} =^{tex} “ph {1}”]

[ph_{2} =^{tex} “ph {2}”]

[ph_{3} =^{tex} “ph {3}”]

[x_{Ph} =^{tex} “#1.

{Ph} ”]

[x^{Ph} =^{tex} “#1.

ˆ {Ph}”]

[⟨x≡y|z:=u⟩_{Ph} =^{tex} “\langle #1. {\equiv} #2. | #3. {:=} #4. \rangle {Ph} ”]

[⟨x≡^{0}y|z:=u⟩_{Ph} =^{tex} “\langle #1. {\equiv}ˆ 0 #2. | #3. {:=} #4. \rangle {Ph} ”]

[⟨x≡^{1}y|z:=u⟩_{Ph} =^{tex} “\langle #1. {\equiv}ˆ 1 #2. | #3. {:=} #4. \rangle {Ph} ”]

[⟨x≡^{∗}y|z:=u⟩_{Ph} =^{tex} “\langle #1. {\equiv}ˆ ∗ #2. | #3.

{:=} #4. \rangle {Ph} ”] [bs =^{tex} “\mathsf {bs}”] [OBS =^{tex} “ \mathsf {OBS}”] [BS =^{tex} “{\cal BS}”] [Ø =^{tex} “\mathrm{\O}”] [ZFsub =^{tex} “ZFsub”]

[MP =^{tex} “MP”]

[Gen =^{tex} “Gen”] [Repetition =^{tex} “Repetition”] [Neg =^{tex} “Neg”] [Ded =^{tex} “Ded”] [ExistIntro =^{tex} “ExistIntro”] [Extensionality =^{tex} “Extensionality”] [Ødef =^{tex} “\O{}def”] [PairDef =^{tex} “PairDef”] [UnionDef =^{tex} “UnionDef”] [PowerDef =^{tex} “PowerDef”] [SeparationDef =^{tex} “SeparationDef”] [CheatAllDisjoint =^{tex} “CheatAllDisjoint”] [AddDoubleNeg =^{tex} “AddDoubleNeg”] [RemoveDoubleNeg =^{tex} “RemoveDoubleNeg”] [AndCommutativity =^{tex} “AndCommutativity”] [AutoImply =^{tex} “AutoImply”] [Contrapositive =^{tex} “Contrapositive”] [FirstConjunct =^{tex} “FirstConjunct”] [SecondConjunct =^{tex} “SecondConjunct”] [FromContradiction =^{tex} “FromContradiction”] [FromDisjuncts =^{tex} “FromDisjuncts”] [IffCommutativity =^{tex} “IffCommutativity”] [IffFirst =^{tex} “IffFirst”] [IffSecond =^{tex} “IffSecond”] [ImplyTransitivity =^{tex} “ImplyTransitivity”] [JoinConjuncts =^{tex} “JoinConjuncts”]

[MP2 =^{tex} “MP2”]

[MP3 =^{tex} “MP3”]

[MP4 =^{tex} “MP4”]

[MP5 =^{tex} “MP5”]

[MT =^{tex} “MT”]

[NegativeMT =^{tex} “NegativeMT”] [Technicality =^{tex} “Technicality”] [Weakening =^{tex} “Weakening”] [WeakenOr1 =^{tex} “WeakenOr1”] [WeakenOr2 =^{tex} “WeakenOr2”] [Pair2Formula =^{tex} “Pair2Formula”] [Formula2Pair =^{tex} “Formula2Pair”] [Union2Formula =^{tex} “Union2Formula”] [Formula2Union =^{tex} “Formula2Union”] [Sep2Formula =^{tex} “Sep2Formula”] [Formula2Sep =^{tex} “Formula2Sep”] [SubsetInPower =^{tex} “SubsetInPower”] [HelperPowerIsSub =^{tex} “HelperPowerIsSub”] [PowerIsSub =^{tex} “PowerIsSub”] [(Switch)HelperPowerIsSub =^{tex} “(Switch)HelperPowerIsSub”] [(Switch)PowerIsSub =^{tex} “(Switch)PowerIsSub”] [ToSetEquality =^{tex} “ToSetEquality”] [HelperToSetEquality(t) =^{tex} “HelperToSetEquality(t)”] [ToSetEquality(t) =^{tex} “ToSetEquality(t)”] [HelperFromSetEquality =^{tex} “HelperFromSetEquality”] [FromSetEquality =^{tex} “FromSetEquality”] [HelperReflexivity =^{tex} “HelperReflexivity”] [Reflexivity =^{tex} “Reflexivity”] [HelperSymmetry =^{tex} “HelperSymmetry”] [Symmetry =^{tex} “Symmetry”] [HelperTransitivity =^{tex} “HelperTransitivity”] [Transitivity =^{tex} “Transitivity”], [ERisReflexive =^{tex} “ERisReflexive”] [ERisSymmetric =^{tex} “ERisSymmetric”] [ERisTransitive =^{tex} “ERisTransitive”] [ØisSubset =^{tex} “\O{}isSubset”] [HelperMemberNotØ =^{tex} “HelperMemberNot\O{}”] [MemberNotØ =^{tex} “MemberNot\O{}”] [HelperUniqueØ =^{tex} “HelperUnique\O{}”] [UniqueØ =^{tex} “Unique\O{}”] [=Reflexivity =^{tex} “=\!{}Reflexivity”] [=Symmetry =^{tex} “=\!{}Symmetry”] [Helper=Transitivity =^{tex} “Helper\!{}=\!{}Transitivity”] [=Transitivity =^{tex} “\!{}=\!{}Transitivity”] [HelperTransferNotEq =^{tex} “HelperTransferNotEq”] [TransferNotEq =^{tex} “TransferNotEq”] [HelperPairSubset =^{tex} “HelperPairSubset”] [Helper(2)PairSubset =^{tex} “Helper(2)PairSubset”] [PairSubset =^{tex} “PairSubset”] [SamePair =^{tex} “SamePair”] [SameSingleton =^{tex} “SameSingleton”] [UnionSubset =^{tex} “UnionSubset”] [SameUnion =^{tex} “SameUnion”] [SeparationSubset =^{tex} “SeparationSubset”] [SameSeparation =^{tex} “SameSeparation”] [SameBinaryUnion =^{tex} “SameBinaryUnion”] [IntersectionSubset =^{tex} “IntersectionSubset”] [SameIntersection =^{tex} “SameIntersection”] [AutoMember =^{tex} “AutoMember”] [HelperEqSysNotØ =^{tex} “HelperEqSysNot\O{}”] [EqSysNotØ =^{tex} “EqSysNot\O{}”] [HelperEqSubset =^{tex} “HelperEqSubset”] [EqSubset =^{tex} “EqSubset”] [EqNecessary =^{tex} “EqNecessary”] [HelperEqNecessary =^{tex} “HelperEqNecessary”] [HelperNoneEqNecessary =^{tex} “HelperNoneEqNecessary”] [Helper(2)NoneEqNecessary =^{tex} “Helper(2)NoneEqNecessary”] [NoneEqNecessary =^{tex} “NoneEqNecessary”] [EqClassIsSubset =^{tex} “EqClassIsSubset”] [EqClassesAreDisjoint =^{tex} “EqClassesAreDisjoint”] [AllDisjoint =^{tex} “AllDisjoint”] [AllDisjointImply =^{tex} “AllDisjointImply”] [BSsubset =^{tex} “BSsubset”] [Union(BS/R)subset =^{tex} “Union(BS/R)subset”] [UnionIdentity =^{tex} “UnionIdentity”] [EqSysIsPartition =^{tex} “EqSysIsPartition”]

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

/ #2.”]

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

\cap #2.”]

[∪x =^{tex} “\cup #1.”]

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

\mathrel{\cup} #2.”]

[P(x) =^{tex} “P(#1.

)”]

[{x} =^{tex} “\{#1.

\}”]

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

, #2. \}”] [⟨x, y⟩ =^{tex} “\langle #1. , #2. \rangle”],

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

\mathrel{\in} #2.”]

[z(x, y) =^{tex} “#3.

(#1. , #2. )”]

[ReflRel(r, x) =^{tex} “ReflRel(#1. , #2. )”]

[SymRel(r, x) =^{tex} “SymRel(#1. , #2. )”]

[TransRel(r, x) =^{tex} “TransRel(#1. , #2. )”]

[EqRel(r, x) =^{tex} “EqRel(#1. , #2. )”]

[[x ∈ bs]_{r} =^{tex} “[#1.

\mathrel{\in} #2. ] {#3. }”]

[Partition(x, y) =^{tex} “Partition(#1. , #2. )”]

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

\!\mathrel{=}\! #2.”]

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

\mathrel{\subseteq} #2.”]

[ ˙¬ x =^{tex} “\dot{\neg}\, #1.”]

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

\mathrel{\notin} #2.”]

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

\mathrel{\neq} #2.”]

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

\mathrel{\dot{\wedge}} #2.”]

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

\mathrel{\dot{\vee}} #2.”]

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

\mathrel{\dot{\Leftrightarrow}} #2.”]

[{ph ∈ x | a} =^{tex} “ \{ ph \mathrel{\in} #1. \mid #2. \}”]