A simple proof of Σ1 correctness of K 3 Ralf Schindler 2 0 0 Institut fu¨r Formale Logik, Universita¨t Wien, 1090 Wien, Austria 2 n [email protected] a J http://www.logic.univie.ac.at/∼rds/ 9 The purpose of the present paper is to present a simple proof of the ] O following result, which is due to John Steel. L . Theorem 0.1 (Steel 1993, [2, Theorem 7.9]) Let A ⊂ R be Π1. Suppose h 2 t that there is some x ∈ A such that (x†)# exists. Suppose also that there is a m no inner model with a Woodin cardinal. There is then an iterable lightface [ premouse M such that A∩M =6 ∅. 1 v We take our statement of Theorem 0.1 and Steel’s statement of [2, The- 7 orem 7.9] to be basically just linguistic variants of each other. 6 0 Our proof of Theorem 0.1 is purely combinatorial in contrast to the proof 1 given in [2, §7.D]. The latter one uses methods from descriptive set theory, 0 2 for instance the Martin-Solovay tree and the Kunen-Martin theorem. We 0 shall be able to avoid any serious use of descriptive set theory, except for / h Shoenfield absoluteness. We believe that the argument to follow might help t a showing the right correctness results for higher core models. m The arguments given below would in fact enable us to prove the stronger : v version of Theorem 0.1 in which “(x†)# exists” is replaced by “x† exists” (or i X even by something slightly less). The key problem that still remains open, r however, is how to prove the version of Theorem 0.1 in which “(x†)# exists” a is replaced by “x# exists.” As for prerequisites, an acquaintance with [2, §§1-6 and p. 58] will cer- tainly 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. 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 ED 6= ∅ and there is some ν < ξ with ED 6= ∅ and ν ≥ crit(ED)+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 car- dinal.” We then let KD denote Steel’s core model of height Ω, as being constructed inside D. [2, §§1-5] give the recipe for how to construct KD. We remark that the ultrapower of D by its top extender doesn’t have to be well-founded for KD to provably exist. Definition 0.5 Let A be a transitive model of ZFC. Then by KA we denote the model which is recursively constructed inside A in the manner of [2, §6], if it exists (otherwise we let KA 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 KD in the sense of Definition 0.4 is identical with KD||Ω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 ∈ R:Φ(y)}, where Φ(−) is Π1. By the hypotheses, we know that KL[x†] exists (cf. [2, p. 58]). 2 Let us write K = KL[x†]. 2 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 • σ:KD → MT ||α is elementary for some α ≤ MT ∩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 ∅ =6 p[T] ⊂ A. This will establish Theorem 0.1. Claim 1. [T] 6= ∅ (in V, and hence in K). Proof. Set D = x†. Let (U,T ′) denote the coiteration of KD with K, which exists inside L[x†]. (We here use the fact that KD is iterable in L[x†].) We’ll have that πU :KD → MT′||α for some α ≤ MT′ ∩ OR. However, 0∞ ∞ ∞ 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′) → MT . As τ ↾ D∪{D} = id, we then have ∞ ∞ that ϕ◦τ−1(πU ):KD → MT ||ϕ(α), 0∞ ∞ where we understand that ϕ(α) = MT ∩OR if α = MT′∩OR (a case which ∞ ∞ actually never comes up). Setting σ = ϕ ◦ τ−1(πU ), we’ll thus have that 0∞ (x,D,T,σ) ∈ [T]. (cid:3) (Claim 1) Claim 2. p[T] ⊂ A. Proof. Let (y,D,T,σ) ∈ [T]. Let ν < D ∩OR be such that ED 6= ∅, ν crit(ED) = κD, and ν ≥ (κD)+D. Let us write E = ED. By Shoenfield ν ν absoluteness itwillsufficetoprovethatD||ΩD isiterablebyU anditsimages. Let (D ,π :i ≤ j ≤ γ) be a putative iteration of D||ΩD, where γ < ω and i ij 1 π :D → D foralli < γ. We have toprove thatD iswell-founded. ii+1 i π0i(E) i+1 γ For i < γ let us write E for π (E). i 0i 3 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 ≤ j ≤ γ) is then i ij the direct limit of (D ,π :i ≤ j < γ). i ij We shall, for each δ < γ, recursively construct an iteration tree T δ of length β +1 onKD, andwe shall inductively verify that the following clauses δ hold true: (a) Ti = Tδ ↾ β +1 for all i ≤ δ, δ i (b) MTδ = KDδ, and δ βδ (c) πTδ = π ↾ KDi for all i ≤ δ. δ βiβδ iδ However, this is a straightforward task. To get started, let us apply [1, Corollary3.1]insideD togetaniterationtreeU onKD withMU = KUlt(D;E) ∞ and πU = π ↾ KD. Notice that we may expand the model D||ΩD by a 0∞ 01 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 ≤ j ≤ γ) as an i ij iteration of (D||ΩD;U) rather than of D||ΩD. For i < γ we’ll write π (U) 0i for the image of U under π , which is well-defined by the amenability of 0i (D||ΩD;U). We’ll have that D = (D||ΩD;U) |= “MU = KUlt(V;E), and 0 ∞ πU = π ↾ K.” 0∞ E Letusnowconstruct(T δ:δ < γ). Tocommence, weletT 0 betrivial. (a) , 0 (b) , and (c) are trivially true. Now suppose that Tδ has been constructed 0 0 for some δ < γ. We may then simply let T δ+1 be the concatenation of T δ with π (U). The elementarity of the map π gives that 0δ 0δ D |= “Mπ0i(U) = KUlt(V;Ei), and δ ∞ ππ0i(U) = π ↾ K.” 0∞ Ei (a) , (b) , and (c) will then be evident. Finally, let δ < γ be a limit δ+1 δ+1 δ+1 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 < δ}. As (b) and (c) hold for all i i i 4 i < δ we’ll have that KDδ = MT′ and πT′ = π ↾ KDi for all i < δ. We may b βib iδ thus let Tδ be that extension of T′ which adds the branch b as well as the final model MU′. Then (a) , (b) , and (c) are evident. b δ δ δ 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 KD is iterable (in L[x†], and hence in V). The model MU∗ is thus well-founded. As (c) holds for all δ < γ, we now have an b δ ∈-isomorphism between the ordinals of D and the ones of MU∗. Therefore, γ b D is well-founded, too. γ (cid:3) (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. (cid:3) (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. 5