We introduce and consider the inner-model reflection principle, which asserts that whenever a statement \varphi(a) in the first-order language of set theory is true in the set-theoretic universe V, then it is also true in a proper inner model W \subset A. A stronger principle, the ground-model reflection principle, asserts that any such \varphi(a) true in V is also true in some non-trivial ground model of the universe with respect to set forcing. These principles each express a form of width (...) reflection in contrast to the usual height reflection of the Lévy–Montague reflection theorem. They are each equiconsistent with ZFC and indeed \Pi_2-conservative over ZFC, being forceable by class forcing while preserving any desired rank-initial segment of the universe. Furthermore, the inner-model reflection principle is a consequence of the existence of sufficient large cardinals, and lightface formulations of the reflection principles follow from the maximality principle MP and from the inner-model hypothesis IMH. We also consider some questions concerning the expressibility of the principles. (shrink)

In so-called full second-order logic, the second-order variables range over all subsets and relations of the domain in question. In so-called Henkin second-order logic, every model is endowed with a set of subsets and relations which will serve as the range of the second-order variables. In our Boolean-valued second-order logic, the second-order variables range over all Boolean-valued subsets and relations on the domain. We show that under large cardinal assumptions Boolean-valued second-order logic is more robust than full second-order logic. Its (...) validity is absolute under forcing, and its Hanf and Löwenheim numbers are smaller than those of full second-order logic. (shrink)

We describe the inner models with representatives in all equivalence classes of thin equivalence relations in a given projective pointclass of even level assuming projective determinacy. The main result shows that these models are characterized by their correctness and the property that they correctly compute the tree from the appropriate scale. The main step towards this characterization shows that the tree from a scale can be reconstructed in a generic extension of an iterate of a mouse. We then construct models (...) with this property as generic extensions of iterates of mice under the assumption that the corresponding projective ordinal is below ω2ω2. On the way, we consider several related problems, including the question when forcing does not add equivalence classes to thin projective equivalence relations. For instance, we show that if every set has a sharp, then reasonable forcing does not add equivalence classes to thin provably View the MathML source Δ1/3 equivalence relations, and generalize this to all projective levels. (shrink)

We extend the core model induction technique to a choiceless context, and we exploit it to show that each one of the following two hypotheses individually implies that , the Axiom of Determinacy, holds in the of a generic extension of : every uncountable cardinal is singular, and every infinite successor cardinal is weakly compact and every uncountable limit cardinal is singular.

We establish natural criteria under which normally iterable premice are iterable for stacks of normal trees. Let Ω be a regular uncountable cardinal. Let m < ω and M be an m-sound premouse and Σ be...

Building on the work of Schimmerling [Coherent sequences and threads, Adv. Math.216 89–117] and Steel [PFA implies AD L, J. Symbolic Logic70 1255–1296], we show that the failure of square principle at a singular strong limit cardinal implies that there is a nontame mouse. The proof presented is the first inductive step beyond L of the core model induction that is aimed at getting a model of ADℝ + "Θ is regular" from the failure of square at a singular strong (...) limit cardinal or PFA. (shrink)

We prove the following result which is due to the third author. Let [Formula: see text]. If [Formula: see text] determinacy and [Formula: see text] determinacy both hold true and there is no [Formula: see text]-definable [Formula: see text]-sequence of pairwise distinct reals, then [Formula: see text] exists and is [Formula: see text]-iterable. The proof yields that [Formula: see text] determinacy implies that [Formula: see text] exists and is [Formula: see text]-iterable for all reals [Formula: see text]. A consequence is (...) the Determinacy Transfer Theorem for arbitrary [Formula: see text], namely the statement that [Formula: see text] determinacy implies [Formula: see text] determinacy. (shrink)

We prove the following result which is due to the third author. Let [Formula: see text]. If [Formula: see text] determinacy and [Formula: see text] determinacy both hold true and there is no [Formula: see text]-definable [Formula: see text]-sequence of pairwise distinct reals, then [Formula: see text] exists and is [Formula: see text]-iterable. The proof yields that [Formula: see text] determinacy implies that [Formula: see text] exists and is [Formula: see text]-iterable for all reals [Formula: see text]. A consequence is (...) the Determinacy Transfer Theorem for arbitrary [Formula: see text], namely the statement that [Formula: see text] determinacy implies [Formula: see text] determinacy. (shrink)