Simple proofs of correctness

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 note is to provide information on how those proofs really go which were sketched in the talk “Einfache Korrektheitsbeweise” in Bonn on 06/20/02.

Theorem 0.1 (Steel [5, 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 ≠ ∅.

Theorem 0.2 (Steel-Welch [6, Theorem 4.1]) Let A ⊂ ℝ be Π_{2}^{1}. Suppose that there is some sequence (x_{n}: n < ω) such that x_{0} ∈ A and for all n < ω, x_{n+1} = x_{n}^{#}. Suppose also that there is some N < ω such that there is no inner model with N strong cardinals. Then A ∩ K ≠ ∅.

Our proofs of Theorems 0.1 and 0.2 are purely combinatorial in contrast to the ones given in [5, §7.D] and [6]. The papers [5, §7.D] and [6] use 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 arguments 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.”

In the statement of Theorem 0.2, K denotes the core model; cf. the remarks right after Definition 0.6. It is open whether Theorem 0.2 still holds if we replace the second sentence in its statement by “Suppose that there is some x ∈ A such that x^{#} exists.” It is also open whether Theorem 0.2 still holds if we replace the third sentence in its statement by “Suppose also that there is no inner model with a Woodin cardinal, but K exists” (cf. Definition 0.6).

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

Let us first prove Theorem 0.1. We’ll need only a few definitions before we can commence with doing this.

Definition 0.3 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.4 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.5 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.

[5, §§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.6 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 [5, §6], if it exists (otherwise we let K^{A} undefined). If K^{A} ↓ then we say that K^{A} exists. If K^{V} ↓ then we write K = K^{V} and say that K exists.

If D is a premouse then we let D||ξ denote D being cut off at ξ. If D is as in Definition 0.5 then K^{D} in the sense of Definition 0.5 is identical with K^{D||Ω^{D}} in the sense of Definition 0.6. This follows from [5, §6]. The two notations introduced by definitions 0.5 and 0.6 cannot be confused, as no dagger is a model of the power set axiom. It is shown in [3] that K exists if 0^{|^{•}} doesn’t exist.

We now turn towards 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. [5, 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 [4, 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)

Let us now turn towards proving Theorem 0.2.

We shall prove Theorem 0.2 with the third sentence in its statement being replaced by “Suppose also that 0^{¶} doesn’t exist.” We’ll leave a proof of Theorem 0.2 as stated as an exercise to the reader.

Definition 0.7 Let (♣) denote the following assertion. Let x ∈ ℝ be such that x^{#} exists. If K^{L[x]} and K^{L[x^{#}]} both exist and are coiterable then there is some α ∈ OR such that K^{L[x^{#}]}||α iterates past K^{L[x]}.

Lemma 0.8 Suppose that 0^{¶} doesn’t exist. Then (♣) holds.

Proof. Suppose that x ∈ ℝ witnesses the failure of (♣). It is fairly easy too see that then K^{L[x^{#}]} ⊧ “there is a strong cardinal.” (Cf. the proof of [6, Lemma 3.3].) Let us now assume that 0^{¶} doesn’t exist. We aim to derive a contradiction. Let us work in L[x^{#}].

Claim 1. cf(κ^{+K^{L[x]}}) = ω for all κ.

Proof. It is true that cf(κ^{+L[x]}) = ω for all κ. Let us thus fix some K^{L[x]}-cardinal κ such that κ^{+K^{L[x]}} < κ^{+L[x]}. Let λ = Card^{L[x]}(κ) ≤ κ. Then λ is neither an x-indiscernible nor singular in L[x]. Let η < λ be the largest x-indiscernible which is smaller than λ.

Let τ_{n} enumerate the Skolem terms of L[x]. The sequence (λ_{n}: n < ω), where

λ_{n} = sup({τ_{n}(ξ⃗): ξ⃗ < η} ∩ λ) < λ

witnesses that cf(λ) = ω. But we’ll have that cf^{L[x]}(κ^{+K^{L[x]}}) = λ by weak covering applied inside L[x] (cf. [2]).

□ (Claim 1)

Claim 2. K^{L[x]} doesn’t move in the comparison with K^{L[x^{#}]}.

Proof sketch. The point is that by our assumption K^{L[x]} absorbs all coiterable set-sized premice which exist in L[x^{#}]. Jensen’s argument yielding that below 0^{¶} any universal weasel is an iterate of K then gives this Claim.

□ (Claim 2)

It is now easy to see that Claims 1 and 2, combined with an application of weak covering applied inside L[x^{#}] (cf. [2]) yields the Lemma.

□ (Lemma 0.8)

The proof of Lemma 0.8 is certainly more interesting than its result. If we had assumed the existence of x^{##} then we could have just cited [6, Lemma 3.3]. We conjecture that (♣) still holds under much weaker assuptions than the non-existence of 0^{¶} (cf. [6, p. 188, Question3]).

We are now going to prove the following result, which will immediately give Theorem 0.2 (the third sentence in its statement being replaced by “Suppose also that 0^{¶} doesn’t exist”) via Lemma 0.8.

We emphasize that Theorem 0.9 is not given by the results of [6]; the proof of [6, Theorem 4.1] which is given in [6] heavily uses universal iterations which are not known to exist significantly above 0^{¶}.

Theorem 0.9 Let A ⊂ ℝ be Π_{2}^{1}. Suppose that there is some sequence x⃗ = (x_{n}: n < ω) such that x_{0} ∈ A and for all n < ω, x_{n+1} = x_{n}^{#}. Suppose also that there is no inner model with a Woodin cardinal, that K^{L[x⃗]} exists, and that (♣) holds. Then A ∩ K^{L[x⃗]} ≠ ∅.

Proof of Theorem 0.9. Let A = {z ∈ ℝ: Φ(z)} where Φ(−) is Π_{2}^{1}. There is a tree T ∈ K^{L[x⃗]} searching for a quadruple (y⃗, M⃗, T⃗ , σ⃗) such that the following hold true.

• y⃗ = (y_{n}: n < ω) ∈ ^{ω}ℝ,

• M⃗ = (M_{n}: n < ω) such that for all n < ω do we have the following: (a) M_{n} = (J_{α_{n}}[y_{n}]; ∈, y_{n}, U_{n}) for some α_{n}, U_{n},

(b) M_{n+1} ⊧ “M_{n} = y_{n}^{#}” (in particular, M_{n+1} thinks that M_{n} is iterable),

(c) y_{n+1} is the master code of M_{n},

(d) M_{0} ⊧ Φ(y_{0}), and

(e) setting κ = crit(U_{n+1}), there is an initial segment of K^{M_{n+1}} which iterates past K^{L_{κ}[y_{n}]}, and

• (T⃗ , σ⃗) witnesses that each individual K^{M_{n}} (n < ω) is iterable (cf. the proof of Theorem 0.1), i.e., T⃗ = (T_{n}: n < ω), σ⃗ = (σ_{n}: n < ω), and for all n < ω do we have the following:

(a) T_{n} is a countable tree of successor length on K^{L[x⃗]}, and

(b) σ_{n}: K^{M_{n}} → M_{∞}^{T_{n}}||β_{n}, some β_{n} ≤ M_{∞}^{T_{n}} ∩ OR, is elementary.

We are now going to prove that

∅ ≠ p[T] = {y_{0}: ∃(y_{1}, y_{2}, ...)∃M⃗∃T⃗ ∃σ⃗((y_{0}, y_{1}, ...), M⃗, T⃗ , σ⃗) ∈ [T]} ⊂ A.

We may well leave the verification of p[T] ≠ ∅ as an exercise to the reader.

Now fix (y⃗, M⃗, T⃗ , σ⃗) ∈ T. Let y⃗ = (y_{n}: n < ω) and M⃗ = (M_{n}: n < ω). Let us prove that y_{0} ∈ A. Let (_{n}^{α}) denote the assertion that the α^{th} iterate of M_{n} is well-founded. It clearly suffices to prove the following.

Main Claim. For all α, for all n, (_{n}^{α}) holds.

Definition 0.10 Let n < ω. We write (M_{n}^{i}, π_{n}^{ij}: i ≤ j ≤ α) for the putative iteration of M_{n} of length α + 1, if it exists; and if so then for i < α we write κ_{n}^{i} for the critical point of π_{n}^{0i}(U_{n}), i.e., of the top extender of M_{n}^{i}. We call α a uniform indiscernible provided that for all n < ω, the putative iteration (M_{n}^{i}, π_{n}^{ij}: i ≤ j ≤ α) of M_{n} of length α + 1 exists and {κ_{i}: i < α} is (closed and) unbounded in α.

Proof of the Main Claim. We’ll prove the Main Claim by induction on α.

Case 1. α is not a uniform indiscernible.

Let n < ω. By our case assumption, there are some m > n and β < α such that α ∈ M_{m}^{β}. But M_{m}^{β} ⊧ “M_{n} = y_{n}^{#},” so that we may argue inside M_{m}^{β} and deduce that the α^{th} iterate of M_{n}, viz. M_{n}^{α}, is well-founded.

Case 2. α is a uniform indiscernible.

Let n < ω. Let κ = crit(U_{n+1}) = κ_{n+1}^{0}, and let P be the proper initial segment of K^{M_{n+1}} = K^{L_{κ}[y_{n+1}]} which iterates past K^{L_{κ}[y_{n}]}. Let (T , U) be the coiteration of K^{L_{κ}[y_{n}]} with K^{L_{κ}[y_{n+1}]}. (M_{n}^{i}, π_{n}^{ij}: i ≤ j < α) is the putative iteration of M_{n} of length α + 1. Let

σ: M_{n+1} →_{U_{n+1}} M′,

i.e., σ = π_{n+1}^{01} and M′ = M_{n+1}^{1}.

Let X ∈ P(κ) ∩ M_{∞}^{U}. Then X = π_{i∞}^{U}(X̄), some i < κ, X̄, and σ(X) = π_{i∞}^{σ(U)}(X̄) = π_{κ∞}^{σ(U)}(X). Therefore, π_{κ∞}^{σ(U)} ↾ κ^{+M_{∞}^{U}} = σ ↾ κ^{+M_{∞}^{U}}. The same argument shows that π_{n}^{κσ(κ)} ↾ κ^{+M_{n}^{κ}} = σ ↾ κ^{+M_{n}^{κ}}; we construe M_{n} in such a way that crit(U_{n})^{+M_{n}} = M_{n} ∩ OR, so that this latter equality means that π_{n}^{κσ(κ)} ↾ M_{n}^{κ} ∩ OR = σ ↾ M_{n}^{κ} ∩ OR. Let us write λ = σ(κ) = κ_{n+1}^{1}.

Now (σ(T ), σ(U)) is the coiteration of K^{L_{λ}[y_{n}]} with K^{L_{λ}[y_{n+1}]}. We’ll have that κ^{+M_{∞}^{U}} = κ^{+M_{κ}^{σ(U)}} = κ^{+M_{κ}^{σ(T )}} ≥ κ^{+K^{L_{λ}[yn]}} = κ^{+L_{λ}[y_{n}]} = κ^{+M_{n}^{κ}}, so that we get that

π_{n}^{κλ} ↾ M_{n}^{κ} ∩ OR = π_{κ∞}^{σ(U)} ↾ M_{n}^{κ} ∩ OR.

This now buys us that if we let (T^{∗}, U^{∗}) denote the coiteration of K^{L_{α}[y_{n}]} with K^{L_{α}[y_{n+1}]} then for typical i ≤ j < α (namely, for all i ≤ j ∈ {κ_{n+1}^{β}: β < α}) we’ll have that

π_{n}^{ij} ↾ M_{n}^{i} ∩ OR = π_{ij}^{U^{∗}} ↾ M_{n}^{i} ∩ OR.

Moreover, U^{∗} may be construed as an iteration of P. As P is iterable, we may thus conclude that the α^{th} iterate of M_{n}, viz. M_{n}^{α}, is well-founded (cf. the argument in the proof of Theorem 0.1).

□ (Main Claim) □ (Theorem 0.9)

Using [1] it can be verified that Theorem 0.9 still holds if the assumption that K^{L[x⃗]} exists is being crossed out and the conclusion is being replaced by “Then there is some lightface iterable premouse M with A ∩ M ≠ ∅.

References

[1] Bill Mitchell and R. Schindler, A universal extender model without large cardinals in V, preprint.

[2] Bill Mitchell and E.Schimmerling, Covering without countable closure, Math.Research Letters 2 (1995), pp. 595-609

[3] Ralf Schindler, The core model for almost linear iterations, Annals of Pure and Appl. Logic 116 (2002), pp. 207 - 274.

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

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

[6] John Steel and Philip Welch, Σ_{3}^{1} absoluteness and the second uniform indiscernible, Israel Journal of Mathematics 104 (1998), pp. 157-190.