Thinning operators and {_P63_1tn4-reflection [Pi4-reflection] [Elektronische Ressource] / vorgelegt von Christoph Duchhardt
118 Pages
English

Thinning operators and {_P63_1tn4-reflection [Pi4-reflection] [Elektronische Ressource] / vorgelegt von Christoph Duchhardt

Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

Description

Christoph DuchhardtThinning Operators and Π -Reflection4-2008-Mathematische Logik und GrundlagenforschungThinning Operators and Π -Reflection4Inaugural-Dissertationzur Erlangung des akademischen Gradeseines Doktors der Naturwissenschaftendurch den Fachbereich Mathematik und Informatikder Westf¨alischen Wilhelms-Universit¨at Mu¨nstervorgelegt vonChristoph Duchhardt-2008-Dekan: Prof. Dr. Dr. h.c. Joachim CuntzErster Gutachter: Prof. Dr. Wolfram PohlersZweiter Gutachter: Prof. Dr. Wilfried BuchholzTag der mu¨ndlichen Pru¨fung: 25.04.2008Tag der Promotion:ContentsIntroduction iii1. Preliminaries 11.1. Ordinal Proof Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11.2. Theories of Reflection . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41.3. Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7I. The Ordinal Notation System 92. Collapsing Functions 112.1. Basic Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112.2. Thinning Hierarchies and Collapsing Functions . . . . . . . . . . . . . . 143. Structure Theory 213.1. Structure Theory forK . . . . . . . . . . . . . . . . . . . . . . . . . . . 213.2. Structure Theory for κ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 253.3. Structure Theory for π . . . . . . . . . . . . . . . . . . . . . . . . . . . . 303.4. Comparison of Collapsing Functions . . . . . . . . . . . . . . . . . . . . 353.5.

Subjects

Informations

Published by
Published 01 January 2008
Reads 21
Language English

Exrait

Christoph Duchhardt
Thinning Operators and Π -Reflection4
-2008-Mathematische Logik und Grundlagenforschung
Thinning Operators and Π -Reflection4
Inaugural-Dissertation
zur Erlangung des akademischen Grades
eines Doktors der Naturwissenschaften
durch den Fachbereich Mathematik und Informatik
der Westf¨alischen Wilhelms-Universit¨at Mu¨nster
vorgelegt von
Christoph Duchhardt
-2008-Dekan: Prof. Dr. Dr. h.c. Joachim Cuntz
Erster Gutachter: Prof. Dr. Wolfram Pohlers
Zweiter Gutachter: Prof. Dr. Wilfried Buchholz
Tag der mu¨ndlichen Pru¨fung: 25.04.2008
Tag der Promotion:Contents
Introduction iii
1. Preliminaries 1
1.1. Ordinal Proof Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2. Theories of Reflection . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.3. Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
I. The Ordinal Notation System 9
2. Collapsing Functions 11
2.1. Basic Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2. Thinning Hierarchies and Collapsing Functions . . . . . . . . . . . . . . 14
3. Structure Theory 21
3.1. Structure Theory forK . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.2. Structure Theory for κ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.3. Structure Theory for π . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3.4. Comparison of Collapsing Functions . . . . . . . . . . . . . . . . . . . . 35
3.5. Checking Indescribability . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.6. Checking Stationarity . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4. The Ordinal Notation System 45
II. Collapsing 49
5. Operator-controlled derivations 51
5.1. The Language and Rules of RS(K) . . . . . . . . . . . . . . . . . . . . . 51
5.2. The infinitary calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
5.3. Predicative Cut Elimination . . . . . . . . . . . . . . . . . . . . . . . . . 60
6. Embeddings 63
6.1. The intermediate proof system . . . . . . . . . . . . . . . . . . . . . . . 63
6.2. Embedding into the main system . . . . . . . . . . . . . . . . . . . . . . 65
i7. Preparations 67
7.1. The OperatorsH . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67γ
7.2. Preparations for the First Collapsing Theorem . . . . . . . . . . . . . . 68
7.3. Preparations for the Second Collapsing Theorem . . . . . . . . . . . . . 69
7.4. Preparations for the Third Collapsing Theorem . . . . . . . . . . . . . . 72
8. Collapsing 77
8.1. The First Collapsing Theorem . . . . . . . . . . . . . . . . . . . . . . . . 77
8.2. The Second Collapsing Theorem . . . . . . . . . . . . . . . . . . . . . . 81
8.3. The Third Collapsing Theorem . . . . . . . . . . . . . . . . . . . . . . . 85
Appendix: An Alternative Collapsing Theorem 95
iiIntroduction
This thesis belongs to the area of (ordinal) proof-theory, which is a subarea of math-
ematical logic. It deals with assigning certain ordinal numbers to axiom systems by
analyzing formal proofs, thereby measuring the strength of these systems and gaining
further insight into them. The hour of birth of this fascinating field was Gentzen’s
analysis of Peano-Arithmetic, PA, i.e. first order number theory. Since then, much
stronger systems of first and second order number theory have been treated proof-
1theoretically. All these theories also have counterparts in set theory, i.e. (very weak)
subsystems of Zermelo-Fraenkel set theory that prove the same relevant sentences
about the natural numbers. It turned out that such systems are technically much easier
2tohandle. Thisthesisdealswithsuchatheory,Π −Ref, whichaxiomatizes auniverse4
that allows reflection of Π -formulas. It uses the elegant (new) technique of thinning4
hierarchies induced by thinning operators, that can implicitly be found in Rathjen’s
analysis of Π -reflection, [Rat94b], and was in its general, explicit form taught to me by3
¨Mollerfeld. Although Rathjen has successfully analyzed much stronger systems,
this is the firstdetailed treatment ofΠ −Ref. We thinkthat the newtechnique we use4
gives someadditional insight. We also thinkthat ourapproach can easily begeneralized
to arbitrary Π −Ref.
n
Ideas Recall that an ordinal α is called F-reflecting on a set Y of ordinals < α iff for
every formula F ∈F (which may contain parameters) we have
L |=F ⇒(∃β∈Y)L |=F.α β
In order to analyze a system T of set theory, one devises an infinitary calculus which
is strong enough to derive the axioms of T. If T contains reflection axioms, one way
to achieve this is to equip the calculus with an appropriate reflection rule. The crucial
connection between reflection rules and thinning hierarchies is provided by the
Reflection Lemma. Let n≥2, Δ⊆Π andn
YA (X) ={α|α is Σ -reflecting on X∩Y}.n
If _
(∀α∈X)L |= {Δ,F},α
1Here we would like to mention the works of Schu¨tte, Feferman, Buchholz, Pohlers, Rathjen,
and others.
2The first step into this direction was taken by Ja¨ger.
iiithen _
Y(∀α∈A (X))L |= {Δ,(∃β∈Y)L |=F}.α β
IfweregardX asasetofmodelcandidates forΔ,F itshowshowX hasto bethinned
out in order to get a set of model candidates for Δ,(∃β ∈ Y)L |= F. As α is Σ -β n+1
reflectingonY iffitisΠ -reflectingonY, thisindicateshowcomplicated (Π -reflecting)n n
ordinals can be replaced by easier (Σ -reflecting) ordinals. Of course when we considern
infinitary proofs, this process has to be iterated reasonably.
The Reflection Lemma leads to an elegant analysis of the system Π −Ref of Π -2 2
reflection, which is proof-theoretically equivalent to the well-known theoryKPω. Here,
one only needs to compute the ordinal
|Π −Ref| =α.(∀F ∈Σ )(Π −Ref ⊢F ⇒L |=F),2 Σ 1 2 α1
because in this special case we have
CKω =|KPω| =|Π −Ref| =α.L |=Π −Ref.∞ 2 ∞ α 21
This fact makes things considerably easier. As indicated, the theory can be embedded
into a semiformal system which contains a (Π -) reflection rule. Knowing that ρ is2
Π -reflecting on Y iff it is a limit point of Y, one defines1
CK ∗A ={ρ∈Eps∩ω |(∀α < α)(ρ∈Lim(A ))},α 0 α1 ρ 0
∗where {α | α < α} is both large enough for proof-theoretical purposes and, as it0 0 ρ
contains only ”simple” α , small enough so that A stays nonempty. Following the0 α
pattern that an application of the critical reflection rule (Π −Ref) in the semiformal2
system corresponds to an application of the thinning operator A (= Lim in the above
definition), W
⊢ Δ,F X |= {Δ,F}∼ W(Π −Ref) = (A)2 ⊢Δ,(∃z)z|=F A(X)|= {Δ,(∃z)z|=F}
we get the translation from derivability in the semiformal system to truth in L by_