A simple proof of Σ_{3}^{1} correctness of K

Ralf Schindler

Institut für Formale Logik, Universität Wien, 1090 Wien, Austria

                    rds@logic.univie.ac.at
              http://www.logic.univie.ac.at/^{∼}rds/

The purpose of the present paper is to present a simple proof of the following result, which is due to John Steel.

Theorem 0.1 (Steel 1993, [2, Theorem 7.9]) Let A ⊂ ℝ be Π_{2}^{1}. Suppose that there is some x ∈ A such that (x^{†})^{#} exists. Suppose also that there is no inner model with a Woodin cardinal. There is then an iterable lightface premouse M such that A ∩ M ≠ ∅.

We take our statement of Theorem 0.1 and Steel’s statement of [2, Theorem 7.9] to be basically just linguistic variants of each other.

Our proof of Theorem 0.1 is purely combinatorial in contrast to the proof given in [2, §7.D]. The latter one uses methods from descriptive set theory, for instance the Martin-Solovay tree and the Kunen-Martin theorem. We shall be able to avoid any serious use of descriptive set theory, except for Shoenfield absoluteness. We believe that the argument to follow might help showing the right correctness results for higher core models.

The arguments given below would in fact enable us to prove the stronger version of Theorem 0.1 in which “(x^{†})^{#} exists” is replaced by “x^{†} exists” (or even by something slightly less). The key problem that still remains open, however, is how to prove the version of Theorem 0.1 in which “(x^{†})^{#} exists” is replaced by “x^{#} exists.”

As for prerequisites, an acquaintance with [2, §§1-6 and p. 58] will certainly suffice. We shall also use the result of [1]; this result would not be needed, though, and could be replaced by a use of the weaker result [2, Lemma 7.13] at the cost of introducing just a bit more notational fog to the argument to follow.

We’ll need only a few definitions before we can commence with proving Theorem 0.1.

Definition 0.2 Let x be a real. An x-premouse D is called an x-dagger provided that for all ξ ≤ D ∩ OR do we have that ξ = D ∩ OR if and only if E_{ξ}^{D} ≠ ∅ and there is some ν < ξ with E_{ν}^{D} ≠ ∅ and ν ≥ crit(E_{ν}^{D})^{+D}. D is called a dagger if D is an x-dagger for some real x.

D is thus a dagger if and only if D is a premouse built over a real and D is the least initial segment of itself which has two active extenders. Note, however, that we do not require a dagger to be iterable. Therefore, x^{†} is a dagger for any real x, but not the other way round.

Definition 0.3 Let D be a dagger. We shall denote by κ^{D}, Ω^{D} the critical points of the two active extenders of D, where we understand that κ^{D} < Ω^{D}.

Definition 0.4 Let D be a dagger. Set Ω = Ω^{D}. Suppose that D ⊧ “there is no transitive model of ZFC and of height Ω which contains a Woodin cardinal.” We then let K^{D} denote Steel’s core model of height Ω, as being constructed inside D.

[2, §§1-5] give the recipe for how to construct K^{D}. We remark that the ultrapower of D by its top extender doesn’t have to be well-founded for K^{D} to provably exist.

Definition 0.5 Let A be a transitive model of ZFC. Then by K^{A} we denote the model which is recursively constructed inside A in the manner of [2, §6], if it exists (otherwise we let K^{A} undefined).

If D is a premouse then we let D||ξ denote D being cut off at ξ. If D is as in Definition 0.4 then K^{D} in the sense of Definition 0.4 is identical with K^{D||Ω^{D}} in the sense of Definition 0.5. This follows from [2, §6]. The two notations introduced by definitions 0.4 and 0.5 cannot be confused, as no dagger is a model of the power set axiom.

We now turn to our proof of Theorem 0.1.

Proof of Theorem 0.1. Fix A and x. Let A = {y ∈ ℝ: Φ(y)}, where Φ(−) is Π_{2}^{1}. By the hypotheses, we know that K^{L[x^{†}]} exists (cf. [2, p. 58]). Let us write K = K^{L[x^{†}]}.

There is a tree T ∈ K of height ω searching for a quadruple (y, D, T , σ) with the properties that:

• y is a real,

• D is a y-dagger with D ⊧ Φ(y),

• T is an iteration tree on K of countable successor length, and

• σ: K^{D} → M_{∞}^{T}||α is elementary for some α ≤ M_{∞}^{T} ∩ OR.

We leave it to the reader’s discretion to construct such a tree T.

Let us write p[T] = {y: ∃D ∃T ∃σ (y, D, T , σ) ∈ [T]}. We claim that ∅ ≠ p[T] ⊂ A. This will establish Theorem 0.1.

Claim 1. [T] ≠ ∅ (in V, and hence in K).

Proof. Set D = x^{†}. Let (U, T′) denote the coiteration of K^{D} with K, which exists inside L[x^{†}]. (We here use the fact that K^{D} is iterable in L[x^{†}].) We’ll have that π_{0∞}^{U}: K^{D} → M_{∞}^{T′}||α for some α ≤ M_{∞}^{T′} ∩ OR. However, as T′ might be uncountable, we’ll have to take a Skolem hull to finish the argument.

Let τ: H̄ → H_{θ}, where θ is regular and large enough, H̄ is countable and transitive, and {x, D, U, T′} ⊂ ran(τ). Let us copy τ^{−1}(T′) onto K, using τ. We get a countable tree τ^{−1}(T′)^{τ} on K; let us write T for τ^{−1}(T′)^{τ}. We also get a last copy map φ: M_{∞}^{τ^{−1}(T′)} → M_{∞}^{T}. As τ ↾ D ∪ {D} = id, we then have that

φ ∘ τ^{−1}(π_{0∞}^{U}): K^{D} → M_{∞}^{T}||φ(α),

where we understand that φ(α) = M_{∞}^{T} ∩ OR if α = M_{∞}^{T′} ∩ OR (a case which actually never comes up). Setting σ = φ ∘ τ^{−1}(π_{0∞}^{U}), we’ll thus have that (x, D, T , σ) ∈ [T].

□ (Claim 1)

Claim 2. p[T] ⊂ A.

Proof. Let (y, D, T , σ) ∈ [T]. Let ν < D ∩ OR be such that E_{ν}^{D} ≠ ∅, crit(E_{ν}^{D}) = κ^{D}, and ν ≥ (κ^{D})^{+D}. Let us write E = E_{ν}^{D}. By Shoenfield absoluteness it will suffice to prove that D||Ω^{D} is iterable by U and its images. Let (D_{i}, π_{ij}: i ≤ j ≤ γ) be a putative iteration of D||Ω^{D}, where γ < ω_{1} and π_{ii+1}: D_{i} →_{π_{0i}(E)} D_{i+1} for all i < γ. We have to prove that D_{γ} is well-founded. For i < γ let us write E_{i} for π_{0i}(E).

Let us first assume that γ is a successor ordinal, γ = δ + 1, say. Then D_{γ} is obtained by an internal ultrapower of D_{δ}. We may thus argue inside D_{δ} to conclude that D_{γ} is well-founded.

Let us now assume that γ is a limit ordinal. (D_{i}, π_{ij}: i ≤ j ≤ γ) is then the direct limit of (D_{i}, π_{ij}: i ≤ j < γ).

We shall, for each δ < γ, recursively construct an iteration tree T^{δ} of length β_{δ} +1 on K^{D}, and we shall inductively verify that the following clauses hold true:

(a)_{δ} T^{i} = T^{δ} ↾ β_{i} + 1 for all i ≤ δ,

(b)_{δ} M_{β_{δ}}^{T^{δ}} = K^{D_{δ}}, and

(c)_{δ} π_{β_{i}β_{δ}}^{T^{δ}} = π_{iδ} ↾ K^{D_{i}} for all i ≤ δ.

However, this is a straightforward task. To get started, let us apply [1, Corollary 3.1] inside D to get an iteration tree U on K^{D} with M_{∞}^{U} = K^{Ult(D;E)} and π_{0∞}^{U} = π_{01} ↾ K^{D}. Notice that we may expand the model D||Ω^{D} by a predicate coding U, which we shall also denote by U, to get (D||Ω^{D}; U) as an amenable model. We may and shall construe (D_{i}, π_{ij}: i ≤ j ≤ γ) as an iteration of (D||Ω^{D}; U) rather than of D||Ω^{D}. For i < γ we’ll write π_{0i}(U) for the image of U under π_{0i}, which is well-defined by the amenability of (D||Ω^{D}; U). We’ll have that

D_{0} = (D||Ω^{D}; U) ⊧ “M_{∞}^{U} = K^{Ult(V;E)}, and
π_{0∞}^{U} = π_{E} ↾ K.”

Let us now construct (T^{δ}: δ < γ). To commence, we let T^{0} be trivial. (a)_{0}, (b)_{0}, and (c)_{0} are trivially true. Now suppose that T^{δ} has been constructed for some δ < γ. We may then simply let T^{δ+1} be the concatenation of T^{δ} with π_{0δ}(U). The elementarity of the map π_{0δ} gives that

D_{δ} ⊧ “M_{∞}^{π_{0i}(U)} = K^{Ult(V;E_{i})}, and
π_{0∞}^{π_{0i}(U)} = π_{E_{i}} ↾ K.”

(a)_{δ+1}, (b)_{δ+1}, and (c)_{δ+1} will then be evident. Finally, let δ < γ be a limit ordinal and suppose that T^{i} has been constructed for every i < δ. Let T′ be the “union” of all T^{i} for i < δ, and let b be the unique cofinal branch through T′ which is generated by {β_{i}: i < δ}. As (b)_{i} and (c)_{i} hold for all i < δ we’ll have that K^{D_{δ}} = M_{b}^{T′} and π_{β_{i}b}^{T′} = π_{iδ} ↾ K^{D_{i}} for all i < δ. We may thus let T^{δ} be that extension of T′ which adds the branch b as well as the final model M_{b}^{U′}. Then (a)_{δ}, (b)_{δ}, and (c)_{δ} are evident.

We may now let U^{∗} be the union of all U^{δ} for δ < γ. Let b be the unique cofinal branch through U^{∗}, which is given by {β_{δ}: δ < γ}. The tree T on K and the map σ witness that K^{D} is iterable (in L[x^{†}], and hence in V). The model M_{b}^{U^{∗}} is thus well-founded. As (c)_{δ} holds for all δ < γ, we now have an ∈-isomorphism between the ordinals of D_{γ} and the ones of M_{b}^{U^{∗}}. Therefore, D_{γ} is well-founded, too.

□ (Claim 2)

Now let y ∈ p[T] ∩ K. Let ϵ least such that y ∈ K||ϵ + 1. Then K||ϵ + 1 is iterable in L[x^{†}], and hence in V. We have found an iterable premouse as desired.

□ (Theorem 0.1)

References

[1] Ralf Schindler, Iterates of the core model, J. Symb. Logic, submitted.

[2] John Steel, The core model iterability problem, Lecture Notes in Logic ♯8.