key: cord-0641894-p9331w6l authors: Viale, Matteo title: The model-companionship spectrum of set theory, generic absoluteness, and the Continuum problem date: 2021-01-19 journal: nan DOI: nan sha: 934ff2f9f050e4a0ef95b8aae49d06ce12a34e2e doc_id: 641894 cord_uid: p9331w6l We show that for $Pi_2$-properties of second or third order arithmetic as formalized in appropriate natural signatures the apparently weaker notion of forcibility overlaps with the standard notion of consistency (assuming large cardinal axioms). Among such $Pi_2$-properties we mention: the negation of the Continuum hypothesis, Souslin Hypothesis, the negation of Whitehead's conjecture on free groups, the non-existence of outer automorphisms for the Calkin algebra, etc... In particular this gives an a posteriori explanation of the success forcing (and forcing axioms) met in producing models of such properties. Our main results relate generic absoluteness theorems for second order arithmetic, Woodin's axiom $(*)$ and forcing axioms to Robinson's notion of model companionship (as applied to set theory). We also briefly outline in which ways these results provide an argument to refute the Continuum hypothesis. Model completeness, model companionship, and the model companionship spectrum of a theory. Model companionship and model completeness are model theoretic notions introduced by Robinson which give a simple first order characterization of the way algebraically closed fields sits inside the class of rings with no zero-divisors. We start this paper rushing through the main properties of model completess and model companionship (we will later on analyze carefully all these concepts in Section 1). Our aim is to show in a few paragraphs how we can use these notions to reformulate in a simple model-theoretic terminology deep generic absoluteness results for second order arithmetic by Woodin and others, as well as other major results on forcing axioms and Woodin's Axiom ( * ). The key model-theoretic concept we are interested in is that of existentially closed model of a first order theory 1 T : Definition 1. Let τ be a signature and T be a first order theory. M is T -existentialy closed (T -ec) if for any τ -structure N ⊒ M which is a model of T we have that A key non-trivial fact is that M is T -ec if and only if it is T ∀ -ec. It doesn't take long to realize that in signature τ = {+, ·, 0, 1} the τ -theory T of fields has as its class of existentially closed models exactly the algebraically closed fields. Note also that if we let S be the class of rings with no zero-divisors which are not fields, we still have that the S-existentially closed structures are the algebraically closed fields (even if no field is a model of S). Model completeness and model companionship allow to generalize these features of the class of rings with no zero divisors to arbitrary first order theories. Definition 2. Let τ be a first order signature. • A τ -theory T is model complete if any model of T is T -ec. • T is the model companion of a τ -theory S if: -any model of S embeds into a model of T and conversely, -T is model complete. In particular in signature τ = {+, ·, 0, 1}, the theory of algebraically closed fields is model complete and is the model companion both of the theory of fields and of the theory of rings with no zero-divisors which are not fields. We will also need here the following equivalent characterization of model completeness: T is model complete whenever • any theory T admitting quantifier elimination is model complete; • any model complete theory T is the model companion of itself; • two τ -theories T and S which have no model in common can have the same model companion, but the model companion of a theory T if it exists is unique; • if T * is the model companion of T it can be the case that no model of T is a model of T * and conversely; • there are τ -theories T which do not admit a model companion (for example this is the case for the theory of groups in signature τ = {·, 1}). Much in the same way as the algebraic closure of a ring R with no zero-divisors closes off R with respect to solutions to polynomial equations with coefficients in R and which exist in some superring of R which has no zero-divisors (and which does not have to be algebraically closed), for a theory T with model companion T * any model M of T brings to a supermodel N of T * which is obtained by adding (at least) the solutions to the existential formulae with parameters in M which are consistent with the universal fragment of T (in the case of ring with no zero-divisors the key universal property one has to maintain is the non-existence of zero-divisors along with the ring axioms). A key property of model companionship which brought our attention to this notion is the following (see Section 1 for details): Fact 1. Let τ be a first order signature and T be a complete τ -theory with model companion T * . Then T * is axiomatized by T * ∀∃ and TFAE for a Π 2 -sentence ψ for τ : In case T is a companionable non-complete theory, further weak hypothesis on T (which are satisfied by set theory) allow to characterize its model companion T * as the unique theory axiomatized by the Π 2 -sentences which are consistent with the universal fragment of any completion of T (see Lemma 1.21) . Unlike other notions of complexity (such as stability, NIP, simplicity) model companionship and model completeness are very sensitive to the signature in which one formalizes a first order theory T . Notation 1. For a given signature τ , τ * is the signature extending τ with new function symbols 2 f φ and new relation symbols R φ for any τ -formula φ(x 0 , x 1 , . . . , x n ). T τ is the τ * -theory with axioms AX 0 φ := ∀ x[φ( x) ↔ R φ ( x)] AX 1 φ := ∀x 1 , . . . , x n [∃yφ(y, x 1 , . . . , x n ) → φ(f φ (x 1 , . . . , x n ), x 1 , . . . , x n )], as φ ranges over the τ -formulae. It is clear that any τ -structure admits a unique extension to a τ * -model of T τ and any τ -theory T is such T ∪ T τ admits quantifier elimination, hence is model complete and is its own model companion relative to signature τ * . This holds regardless of whether the τ -theory T is model complete or admits a model companion in signature τ (cfr. T being the theory of groups in signature {·, 1}). On the other hand T is stable (simple, NIP) if and only if so is T τ . This is a serious drawback if one wishes to use model companionship to gauge the complexity of a mathematical theory T , since model companionship of T is very much dependent on the signature in which we formalize it: T can trivially be model complete if we formalize it in a rich enough signature. We now introduce a simple trick to render model companionship a useful classification tool for mathematical theories regardless of the signature in which we give their first order axiomatization. Roughly the idea is to consider all possible signatures in which a theory can be formalized and pay attention only to those for which the theory admits a model companion. Definition 3. Let τ be a signature and F τ denote the set of τ -formulae. Given A ⊆ F τ × 2, let τ A be the signature τ ∪ {R φ : (φ, 0) ∈ A} ∪ {f φ : (φ, 1) ∈ A}. A τ -theory T is (A, τ )-companionable if T A = T ∪ AX i φ , : (φ, i) ∈ A admits a model companion for the signature τ A . Given a τ -theory T its τ -companionship spectrum is given by those A ⊆ F τ × {0, 1} such that T is (A, τ )-companionable. Note that F τ × {i} is always in the companionship spectrum of T , but proving that someĀ F τ is such that some A ⊆Ā × 2 is in the companionship spectrum of T is a (possibly highly) non-trivial and informative result on T ; model-companionability for T amounts to say that T is (∅, τ )-companionable. The τ -companionship spectrum of T is non-informative if T is model complete in signature τ : in this case the τ -companionship spectrum of T is P (F τ × 2). Note also that even if T is (∅, τ )-companionable there could be many A ⊆ F τ × 2 such that T is A-companionable and many B ⊆ F τ × 2 such that T is not B-companionable; in principle nothing prevents the families of such As and Bs to be both of size 2 |Fτ | and to produce a complex ordering of the τ -companionship spectrum of T with respect to ⊆. To better grasp the above considerations, let for a τ -theory T C T be the category whose objects are the τ -models of T and whose arrows are the τ -morphisms. NIP, stability, simplicity are properties which consider only the objects in this category, model completeness and model companionship pay also attention to the arrows of this category. We get a much deeper insight on the properties of C T if we are able to detect for which A ⊆ F τ × 2 T A is model companionable: for any A ⊆ F τ × 2 in the passage from C T to C T A we maintain the same class of objects, but the τ A -morphisms (i.e the arrows of C T A ) are just the τ -morphisms between models of T which preseve the formulae in A, hence we are possibly destroying many arrows. Our definition of τ -companionship spectrum of a mathematical theory is apparently dependent on the signature τ in which we formalize it. We may argue that this is not the case, but to uncover why would bring us far afield and we defer this task to another paper. We will in this paper confine our attention to use this notion to analyze first order axiomatizations of set theory enriched with large cardinal axioms. In this case we can certainly say that proving that some A F {∈} × 2 is in the ∈-companionship spectrum of set theory is an informative result: {∈} is a minimal signature in which set theory can be formalized (in the empty signature we certainly cannot formalize it), hence any A ⊆ F {∈} × 2 for which set theory is A-companionable gives non-trivial information on set theory. Moreover we can easily verify that any reasonable ∈-axiomatization of set theory is not model complete for the ∈-signature, hence the ∈-companionship spectrum of set theory is certainly non-trivial. Some of our main results. We can now state in an informative way key parts of our main results. The first non-trivial result states that for any definable cardinal κ there is at least one signature admitting a constant for the cardinal κ such that set theory is companionable for this signature. It is convenient from now on to adopt the following short-hand notation for structures: Theorem 1. Let T ⊇ ZFC be a ∈-theory, and κ be a T -definable cardinal (i.e. such that for some ∈-formula φ κ (x) T proves ∃!x[φ κ (x) ∧ x is a cardinal]). Then there is at least one A κ F ∈ such that lettingĀ κ = A κ × 2: (1) For all models (V, (3) The model companion T * κ of TĀ κ for signature {∈}Ā κ is the {∈}Ā κ -theory common to H V κ + as (V, ∈) ranges over ∈-models of T and κ is the constant of {∈} * given by the formula ∃!x[φ κ (x) ∧ x is a cardinal]. (4) T * κ is also axiomatized by the Π 2 -sentences for {∈}Ā κ which are consistent with S ∀ for any {∈}Ā κ -theory S which is a complete extension of TĀ κ . Note that the above theorem allows to put in the companionship spectrum of any extension of ZFC at least oneĀ κ for each definable cardinal κ such as ω, ω 1 , . . . , ℵ ω , . . . , ℵ ω 1 , . . . , κ, . . . for κ the least inaccessible, measurable, Woodin, supercompact, extendible. . . In case κ = ω, ω 1 we can say much more and prove that for Π 2 -sentences in the appropriate signature forcibility and consistency overlap (assuming large cardinal axioms). This gives an a posteriori explanation of the success forcing has met in proving the consistency of Π 2 -properties (according to the right signature) for second or third order artithmetic: our results show that there are no other means to prove the consistency of such statements. (1) For all models (V, (2) S isĀ i -companionable for both i = 1, 2 3 . (3) The model companion of SĀ 1 is the τĀ 1 -theory common to the models H V [G] ℵ 1 as (V ∈) ranges over ∈-models of S and G is V -generic for some 4 P ∈ V . 3 With very strong large cardinal axioms for the case for TĀ 2 , and no large cardinal axioms in the case for for V [G] a forcing extension of V which models MM ++ and (V, ∈) a ∈-model of S 5 . (5) (SĀ 1 ) ∀ and (SĀ 2 ) ∀ are both invariant across forcing extensions of V for any ∈model (V, ∈) of S (assuming the existence of class many Woodin cardinals in V ). Corollary 1. Assume S extends ZFC with the correct large cardinal axioms. Let X be any amongĀ 1 ,Ā 2 ⊆ F {∈} × 2 as in the previous theorem, and: • S X be the τ X -theory S ∪ AX i φ : (φ, i) ∈ X , • S * X be the model companion theory of S X given by the previous theorem. TFAE for any Π 2 -sentence ψ for τ X : In particular the equivalence of (B) with (C) shows that forcibility and consistency overlap for Π 2 -sentences in signature {∈} X . We complete this introduction outlining a bit more the significance of the above results and trying to get a better insight on what are the signatures What is the right signature for set theory? The ∈-signature is certainly sufficient to give by means of ZFC a first order axiomatization of set theory (with eventually other extra hypothesis such as large cardinal axioms), but we can see rightaway that it is not efficient to formalize many basic set theoretic concepts. Consider for example the notion of ordered pair: on the board we write x = y, z to mean that x is the ordered pair with first component y and second component z. In set theory this concept is formalized by means of Kuratowski's trick stating that x = {{y} , {y, z}}. However the ∈-formula formalizing the above is: It is clear that the meaning of this ∈-formula is hardly decodable with a rapid glance (unlike x = y, z ), moreover just from the point of view of its syntactic complexity it is already Σ 2 . On the other hand we do not regard the notion of ordered pair as a complex or doubtful concept (as is the case for the notion of uncountability, or many of the properties of the continuum such as its correct place in the hierarchy of uncountable cardinals, etc...). Other vary basic notions such as: being a function, a binary relation, the domain or the range of a function, etc.. are formalized already by rather complicated ∈-formulae, both from the point of view of readability for human beings and from the mere computation of their syntactic complexity according to the Levy hierarchy. The standard solution adopted by set theorists (e.g. [13, Chapter IV] ) is to regard as elementary all those properties which can be formalized using ∈-formulae all of whose quantifiers are bounded to range over the elements of some set, i.e. the so called ∆ 0formulae (see [13, Chapter IV, Def. 3.5] ). We henceforth adopt this point of view and let B 0 ⊆ F {∈} be the set of such formulae and denote by τ ST what according to our previous terminology should rather be {∈} B 0 ×2 . For the sake of convenience and also to further outline some very nice syntactic features of ZFC as formalized in τ ST , let us bring to front an explicit axiomatization of T B 0 (which from now on will be denoted by T ST ). • τ ST is the extension of the first order signature {∈} for set theory which is obtained by adjoining predicate symbols R φ of arity n for any ∆ 0 -formula φ(x 1 , . . . , x n ), function symbols of arity k for any ∆ 0 -formula θ(y, x 1 , . . . , x k ) and constant symbols for ω and ∅. • ZFC − is the ∈-theory given by the axioms of ZFC minus the power-set axiom. • T ST is the τ ST -theory given by the axioms ω is the first infinite ordinal (the former is an atomic τ ST -sentence, the latter is expressible as the atomic sentence for τ ST stating that ω is a non-empty limit ordinal all whose elements are successor ordinals or 0). Levy absoluteness and model companionship results for set theory. Kunen's [13, Chapter IV] gives a rather convincing summary of the reasons why it is convenient to formalize set theory using τ ST rather than ∈. We focus here on the role Levy's absoluteness plays in the search of A ⊆ F {∈} × 2 for which set theory is A-companionable. Lemma 1. Let (V, ∈) be a model of ZFC and κ be an infinite cardinal for V . Then Its proof is a trivial variant of the classical result of Levy (which is the above theorem stated just for the signature τ ST ); it is given in [22, Lemma 5.3] . The upshot is that for any model V of ZFC and any signature σ such that This is a first indication that for a ZFCdefinable cardinal κ (e.g. κ = ω, ω 1 , ℵ ω , . . . , more precisely κ being provably in some T ⊇ ZFC the unique solution of an ∈-formula φ κ (x)) if σ κ = τ ST ∪ {κ} and T κ is the σ κ -theory given by ZFC + φ κ (κ), we get that the σ κ -theory common to all of the H V κ + as V ranges over the model of ZFC is not that far from being ZFC-ec, since a model of this theory is always a Σ 1 -substructure of some σ κ -model of ZFC. A second indication that the σ κ -theory of H κ + is close to be the model companion of the σ κ -theory of V is the fact that the Π 2 -sentence for σ κ ∀x∃f : κ → x surjective function is realized in H V κ + for any model V of ZFC (note that by Levy's absoluteness this sentence is consistent with the universal fragment of the σ κ -theory of V , hence by Fact 1 it belongs to the model companion of set theory for σ κ -if such a model companion exists). In particular if some T ⊇ ZFC is σ-companionable for some σ as above, the model companion of T for σ should be the theory of H M κ + for suitably chosen M which are models of set theory. A natural question is: Can we cook up σ ⊇ τ ST ∪ {κ} so that the σ-theory of H κ + is the model companion of the σ-theory of V ? Theorem 1 answer affirmatively to this question for many natural choices of σ and for all definable cardinals κ. Why the continuum is the second uncountable cardinal. Theorem 2 refines Thm. 1 for the cases κ = ω, ω 1 . In these cases our knowledge of the theory of H κ + is much more extensive; moreover most of mathematics can be formalized in H ω 1 (all of second order arithmetic) or in H ω 2 (most of third order arithmetic). We now want to outline briefly why Thm. 2 provides an interesting metamathematical argument in favour of strong forcing axioms and against CH. The considerations of this brief paragraph will be expanded in more details in a forthcoming paper and have been elaborated jointly with Giorgio Venturi. Those who are familiar with forcing axioms know that Martin's maximum and its bounded forms have been instrumental to prove the consistency of a solution of many problems of third order arithmetic which are provably undecidable in ZFC (or even in ZFC supplemented by large cardinal axioms), a sample of these solutions include: the negation of the continuum hypothesis [6, 8, 16, 21, 25] , the negation of Whitehead conjecture on free abelian groups [18] , the non-existence of outer automorphism of the Calkin algebra [7] , the Suslin hypothesis [11] , the existence of a five element basis for uncountable linear order [17] . . . All statements of the above list (with the exception of the non-existence of outer automorphism of the Calkin algebra) and many others can be formalized as Π 2 -sentences in signature τ ω 1 = τ ST ∪ {ω 1 } (where ω 1 is a new constant symbol which is the unique solution of some formula in one free variable defining the first uncountable cardinal). For example ¬CH is formalized by In particular there has been empiric evidence that forcing axioms produce models of set theory which maximize the family of Π 2 -sentences which hold true in H ω 2 for the signature τ ω 1 . Thm. 2 makes this empiric evidence a true mathematical fact: first of all it is important to note here that (sticking to the notation of Thm. 2) {∈}Ā 2 ⊇ τ ω 1 . Now let T be a theory as in the assumption of Thm. 2; take (in signature {∈}Ā 2 ) any Π 2 -sentence ψ which is consistent with S ∀ whenever S is a complete extension of TĀ 2 ; then by (A)⇐⇒(B) of Corollary 1 ψ is in the model companion of TĀ 2 , and Thm. 4(4) (almost) asserts that ψ Hω 2 is derivable from MM ++ . Note that MM ++ is one of the strongest forcing axioms. Another key observation is that (assuming large cardinals) the signature {∈}Ā 2 is such that the universal fragment of set theory as formalized in {∈}Ā 2 is invariant through forcing extensions of V . What this means is that one can and must use forcing to establish whether some Π 2 -sentence ψ is in the model companion of set theory according to {∈}Ā 2 . This is the major improvement of Thm. 2 with respect to Thm. 1: for most of the signatures τĀ κ mentioned in Thm. 1 we cannot just use forcing to establish whether a Π 2 -sentence ψ for this signature is in the model companion of set theory for τĀ κ . Let us develop more on this point because it is in our eyes one of the major advances given by the results of the present paper. Take S ⊇ ZFC; for a given X ⊆ F {∈} × 2 for which we can prove that S X has a model companion in signature {∈} X we would like to show that a certain Π 2 -sentence ψ for {∈} X is in the model companion of S X . Let us first suppose that X is someĀ κ as in Thm. 1. A first observation is that (with the exception of the ∆ 0 -formulae) all the formulae in A κ define subsets of P (κ) n for some for any (V, ∈) which models ZFC. This gives that if (W, {∈} W Aκ ) models (S X ) ∀ , then so does (H W κ + , {∈} W Aκ ). A natural strategy to put ψ in the model companion of S X would then be to start from some complete T ⊇ S and some (V, ∈) model of T ; then force over V that in some , then ψ would be in the model companion of SĀ κ by Thm. 1(4): Levy's absoluteness applied to ( Now starting from any model V of S we may be able to design a forcing in V such that κ + holds if G is V -generic for this forcing, but it may be the case that (SĀ κ ) ∀ fails in as a witness that ψ is in the model companion of SĀ κ . Remark 1 shows that (SĀ κ ) ∀ is not preserved through forcing extensions whenever κ > ω 1 . On the other hand for the signatures τ X for X being theĀ 1 orĀ 2 mentioned in Thm. 2 the above strategy works: the universal fragment of (S X ) ∀ is preserved through the forcing extensions of models of S; hence ψ will be in the model companion of S X if for any model V of S we can design a forcing making true ψ in H V [G] κ + (for κ = ω, ω 1 according to whether ψ is a formula for τĀ 1 or for τĀ 2 ). Summing up one may and should only use forcing to establish the consistency with large cardinals of ψ Hω 2 for any Π 2 -sentence formalizable in signatures τ ω 1 ⊆ {∈}Ā 2 : the strategy we outlined above is efficient (as the many applications of forcing axioms have already shown) and sufficient to compute all Π 2 -sentences which axiomatize the model companion of SĀ 2 , provided S is any set theory satisfying sufficiently strong large cardinal axioms (by Corollary 1 all other means to produce the consistenty of ψ with the universal fragment of S are reducible to forcing). Our take on the above considerations is that if one embraces the standpoint that the universe of sets should be as large as possible, model companionship (in particular Fact 1 -actually its more refined version provided by Lemma 1.21 and used in Thm. 2) gives a simple model theoretic property to instantiate this slogan: all Π 2 -sentences talking about ω 1 (i.e. expressible in signature τ ω 1 ) which are not outward contradictory with the basic properties of ω 1 (i.e. with the universal theory of some model of ZFC+large cardinals in signature τ ω 1 ) should hold true in H ω 2 . This is what Thm. 2 says to be the case in models of strong forcing axioms such as MM ++ . Note that this is exactly parallel to the way one singles out algebraically closed fields from rings with no zero-divisors: in this set-up one is interested to solve polynomial equations while preserving the ring axioms and not adding zero-divisors; the Π 2 -sentences for the signature {+, ·, 0, 1} which are consistent with the ring axioms and the non existence of zero divisors are exactly the axioms of algebraically closed fields. Now coming back to CH we already observed that its negation is a Π 2 -sentence for τ ω 1 (hence also for {∈}Ā 2 ), but we can actually get more. Caicedo and Veličković [6] proved that there is a quantifier free τ ω 1 -formula φ(x, y, z) such that (∀x, y∃zφ(x, y, z)) Hω 2 is forcible (by a proper forcing) over any model of ZFC; moreover if V |= ZFC+(∀x, y∃zφ(x, y, z)) Hω 2 , then V |= 2 ω = ω 2 . In particular if we accept as true large cardinal axioms and we require that the correct axiomatization of set theory maximizes the set of Π 2 -sentences for τ ω 1 which may hold for H ℵ 2 , we are bound to accept that 2 ω = ω 2 holds true. Structure of the paper. It is now a good place to streamline the remainder of this paper and specify what the reader need to know in order to grasp each of its parts. • Section 1 gives a detailed and self-contained account of model companionship; the unique result which we are not able to trace elsewhere in the literature is Lemma 1.21, which isolates a key property of (possibly incomplete) first order theories granting model companionship results; we apply it in later parts of this paper to various (possibly recursive or incomplete) axiomatizations of set theory. Since we expect that many of our readers are not familiar with model companionship, we decided it was worth including here the key results (with proofs) on this notion. The reader familiar with these notions can skim through this section or jump it and refer to its relevant bits when needed elsewhere. • Section 2 proves Theorem 1. • Section 3 proves the results needed to establish item 5 of Thm. 2. We first give a self-contained proof of the form of Woodin's generic absoluteness results for second order arithmetic we employ in this paper. This identifies which subsets of F {∈} can play the role of A 1 for item 5 of Thm. 2. Then we show that the universal theory of V as formalized in a signature extending τ ST with predicates for the non-stationary ideal and for the universally Baire sets cannot be changed using set sized forcing if there are class many Woodin cardinals. This identifies which subsets of F {∈} can play the role of A 2 for item 5 of Thm. 2. • Section 4 deals with Theorem 2 for the signature τĀ 1 . We expand slightly the results of [22] : by taking advantage of Lemma 1.21, we are able here to generalize also to non complete axiomatizations of set theory the model companionship results given in [22] for complete set theories. • Section 5 deals with Theorem 2 for the signature τĀ 2 . • We conclude the paper with a final section with some comments and open questions. Any reader familiar enough with set theory and model theory to follow this introduction can easily grasp the content of Sections 1, 2. The same applies for the results of Section 4 provided one accepts as a black-box Woodin's generic absoluteness results for second order arithmetic given in Section 3. The proofs in Section 3 require familiarity with Woodin's stationary tower forcing and (in its second part, cfr. Section 3.4) also with Woodin's P max -technology. Section 5 can be fully appreciated only by readers familiar with forcing axioms, Woodin's stationary tower forcing, Woodin's P max -technology. Acknowledgements. This paper wouldn't exist without the brilliant idea by Venturi to relate the study of the generic multiverse of set theory to Robinson's model companionship, or without the major breakthrough of Asperò and Schindler establishing that Woodin's axioms ( * ) follows from MM ++ . I'm grateful to Boban Velickovic for many useful discussions on the scopes and limits of the results presented here (the necessity of large cardinal assumptions in the hypothesis of Thm. 3, and Remark 1 are due to him). I'm also grateful to Philipp Schlicht who realized Thm. 1 could be easily established by slightly generalizing the proofs of results occurring in previous drafts of this paper. I've had fruitful discussions on the content of this paper with many people, let me mention and thank David Asperó, Ilijas Farah, Juliette Kennedy, Menachem Magidor, Ralf Schindler, Jouko Vaananen, Andres Villaveces, Hugh Woodin. Clearly none of the persons mentioned here has any responsibility for any error or orror existing in this paper.... It has been important to have the opportunity to present these results in several set theory (or logic) seminars among which those in Toronto, Muenster, Jerusalem, Paris, Bogotà, Chicago, Helsinki, Torino. This research has been performed mostly while on sabbatical in theÉquipe de Logique Mathématique of the University of Paris 7 in the academic year 2019-2020; as long as possible it has been a productive and pleasant experience (until the Covid19 pandemic took place). We present this topic expanding on [20, Sections 3.1-3.2]. We decided to include detailed proofs since the presentation of [20] is (in some occasions) rather sketchy, and the focus is not exactly ours. The first objective is to isolate necessary and sufficient conditions granting that some τ -structure M embeds into some model of some τ -theory T . We expand Notation 3 as follows: T is Π n -separated from S if some Π n -sentence for τ separates T from S. (1) T is not Π 1 -separated from S (i.e. no universal sentence ψ is such that T ⊢ ψ and S ⊢ ¬ψ). Proof. We assume T, S are closed under logical consequences. (2) implies (1): By contraposition we prove ¬(1)→ ¬ (2) . Assume some universal sentence ψ separates T from S. Then for any model of T , all its substructures model ψ, therefore they cannot be models of S. (1) implies (2): By contraposition we prove ¬(2)→ ¬ (1) . Assume that for any model M of S and N of T M ⊑ N . We must show that T is Π 1 -separated from S. Given a τ -structure M = (M, τ M ) which models S, let ∆ 0 (M) be the atomic diagram 6 of M in the signature τ ∪ M . The theory T ∪ ∆ 0 (M) is inconsistent, otherwise M embeds into some model of T : letQ be a τ ∪ M-model of ∆ 0 (M) ∪ T and Q be the τ -structure obtained fromQ omitting the interpretation of the constants not in τ . Clearly Q models T . The interpretation of the constants in τ ∪ M insideQ defines a τ -substructure of Q isomorphic to M. By compactness (since ∆ 0 (M) is closed under finite conjunctions) there is a quantifier free τ -formula ψ M ( x) and a ∈ M <ω such that T +ψ M ( a) is inconsistent. This gives that T ⊢ ¬ψ M ( a). Since a is a family of constants never occurring in T , we get that T ⊢ ∀ x¬ψ M ( x) and M |= ∃ xψ M ( x). The theory By compactness there is a finite set of formulae ψ M 1 . . . ψ M k such that is a conjunction of universal sentences (hence -modulo logical equivalence-universal) derivable from T . Hence ¬ψ separates T from S. The following Lemma shows that models of T ∀ can always be extended to superstructures which model T . (1) M is a τ -model of T ∀ . (2) There exists N ⊒ M which models T . Proof. (2) implies (1) is trivial. Conversely: Proof. If not there are a ∈ M <ω , and a quantifier free τ -formula φ( x, z) such that The latter yields that ∆ 0 (M) ⊢ ∃ x∃ z¬φ( x, z), and therefore also that M |= ∃ x∃ z¬φ( x, z). On the other hand, since the constants a do not appear in any of the sentences in T , we also get that T ⊢ ∀ x∀ zφ( x, z). This is a contradiction since M models T ∀ . By the Claim and Lemma 1.3 some τ ∪ M-modelP of ∆ 0 (M) embeds into some τ ∪ M-modelQ of T . Let Q be the τ -structure obtained fromQ omitting the interpretation of the constants not in τ . Then Q models T and contains a substructure isomorphic to M. The Resurrection Lemma motivates the resurrection axioms introduced by Hamkins and Johnstone in [9] , and their iterated versions introduced by the author and Audrito in [5] . 1.1. Existentially closed structures. The objective is now to isolate the "generic" models of some universal theory T (i.e. all axioms of T are universal sentences). These are described by the T -existentially closed models. Definition 1.6. Given a first order signature τ , let T be any consistent τ -theory. A τ -structure M is T -existentially closed (T -ec) if (1) M can be embedded in a model of T . (2) M ≺ Σ 1 N for all N ⊒ M which are models of T . In general T -ec models need not be models 7 of T , but only of their universal fragment. A standard diagonalization argument shows that for any theory T there are T -ec models, see Lemma 1.9 below or [20, Lemma 3.2.11] . A trivial observation which will come handy in the sequel is the following: Then M is S-ec. (4) Let ∀ x∃ yψ( x, y, a) be a Π 2 -sentence with ψ( x, y, z) quantifier free τ -formula and parameters a in M <ω . Assume it holds in some N ⊒ M which models T ∀ , then it holds in M. (5) Let S be the τ -theory of M. For any Π 2 -sentence ψ in the signature τ TFAE: • ψ holds in some model of S ∀ . • ψ holds in M. (1): There is at least one super-structure of M which models T , and any ψ ∈ T ∀ holds in this superstructure, hence in M. (2): Assume M ⊑ P for some model P of T ∀ . We must argue that M ≺ 1 P. By Lemma 1.4, there is Q ⊒ P which models T . Since M and Q are both models of T and M is T -ec, we get the following diagram: Then any Σ 1 -formula ψ( a) with a ∈ M <ω realized in P holds in Q, and is therefore reflected to M. We are done by Tarski-Vaught's criterion. (3): Assume N ⊑ P for some model of T ∀ P. Let ∆ 0 (P) be the atomic diagram of P in the signature τ ∪ P ∪ M and ∆ 0 (M) be the atomic diagram of M in the same signature 8 . is a consistent τ ∪ M ∪ P-theory. 7 For example let T be the theory of commutative rings with no zero divisors which are not fields in the signature (+, ·, 0, 1). Then the T -ec structures are exactly all the algebraically closed fields, and no T -ec model is a model of T . By Thm. 2.6 (Hω 1 , σ V ω ) is S-ec for S the σω-theory of V , but it is not a model of S: the Π2-sentence asserting that every set has countable transitive closure is true in (Hω 1 , σ V ω ) but denied by S. 8 Proof. Assume not. Find a ∈ (P \ N ) <ω , b ∈ (M \ N ) <ω , c ∈ N <ω and τ -formulae ψ 0 ( x, z), ψ 1 ( y, z) such that: Since the constants appearing in a, b, c are never appearing in sentences of T , we get that Since P models T ∀ , and we get that P |= ∀ y¬ψ 1 ( y, c). being a substructure of P, and so does M since N ≺ 1 M. This contradicts , and Q is the τ -structure obtained forgetting the constant symbols not in τ , we get that: • P and M are both substructures of Q containing N as a common substructure; We can now conclude that if a Σ 1 -formula ψ( c) for τ ∪ N with parameters in N holds in P, it holds in Q as well (since Q ⊒ P), and therefore also in N (since N ≺ 1 Q). In particular a structure is T -ec if and only if it is T ∀ -ec, and a T -ec structure realizes all Π 2 -sentences which are consistent with its Π 1 -theory. We now show that any structure M can always be extended to a T -ec structure for any T which is not separated from the Π 1 -theory of M. Proof. Given a model M of T , we construct an ascending chain of T ∀ -models as follows. Enumerate all quantifier free τ -formulae as {φ α (y, such that π 2 (α) ≤ α for all α < κ and for each ξ < |τ |, and η, β < κ there are unboundedly many α < κ such that π(α) = (ξ, η, β). ) is a consistent τ ∪M β -theory; if so let M β+1 have size κ and realize this theory. At limit stages γ, let M γ be the direct limit of the chain of τ -structures {M β : β < γ}. Then all M ξ are models of T ∀ , and at some stage β ≤ κ M β is T ∀ -ec (hence also T -ec), since all existential τ -formulae with parameters in some M η will be considered along the construction, and realized along the way if this is possible, and all M η are always models of T ∀ (at limit stages the ascending chain of T ∀ -models remains a T ∀ -model). Compare the above construction with the standard consistency proofs of bounded forcing axioms as given for example in [3, Section 2] . In the latter case to preserve T ∀ at limit stages we use iteration theorems 9 . Definition 1.11. A τ -theory T is Π n -complete, if it is consistent and for any Π n -sentence either φ ∈ T or ¬φ ∈ T . By Proposition 1.8.5 we get: In particular any model of the Kaiser hull of a Π 1 -complete T realizes simultaneously all Π 2 -sentences which are individually consistent with T ∀ . For theories T of interests to us their Kaiser hull can be described in the same terms, but the proof is much more delicate. We start with the following weaker property which holds for arbitrary theories: Fact 1.13. Given a τ -theory T , its Kaiser hull KH(T ) contains the set of Π 2 -sentences ψ for τ such that for all complete S ⊇ T , S ∀ ∪ {ψ} is consistent. Proof. Assume ψ is a Π 2 -sentence such that for all complete S ⊇ T , S ∀ ∪ {ψ} is consistent. We must show that ψ holds in all T -ec models. Fix M an existentially closed model for T (it exists by Lemma 1.9); we must show that M |= ψ. Let N ⊒ M be a model of T and S be the τ -theory of N . Then S is a complete theory and M |= S ∀ since M ≺ 1 N (being T -ec). Since S ⊇ T , M is also S-ec (by Fact 1.7). Since S ∀ ∪ {ψ} is consistent, and S ∀ is Π 1 -complete, we obtain that M models ψ, being an S ∀ -ec model, and using Fact 1.12. We will show in Lemma 1.21 that the set of Π 2 -sentences described in the Fact provides an equivalent characterization of the Kaiser hull for many theories admitting a model companion, among which the axiomatizations of set theory considered in this paper. 9 Assume G is V -generic for a forcing which is a limit of an iteration of length ω of forcings {Pn : n < ω}. is not given by the union of H , hence a subtler argument is needed to maintain that H It is possible (depending on the choice of the theory T ) that there are models of the Kaiser hull of T which are not T -ec. Robinson has come up with two model theoretic properties (model completeness and model companionship) which describe the case in which the models of the Kaiser hull of T are exactly the class of T -ec models (even in case T is not a complete theory). Remark that theories admitting quantifier elimination are automatically model complete. On the other hand model complete theories need not be complete 10 . However for theories T which are Π 1 -complete, model completeness entails completeness: any two models of a Π 1 -complete, model complete T share the same Π 1 -theory, therefore if Since they are both models of T , model completeness entails that M 1 ≺ M 2 . Remark that (d) (or (c)) shows that being a model complete τ -theory T is expressible by a ∆ 0 (τ, T )-property in any model of ZFC, hence it is absolute with respect to forcing. Proof. Let Γ be the set of universal τ -formulae θ( x) such that Note that Γ is closed under finite conjunctions and disjunctions. Let if this is the case, by compactness, a finite subset Γ 0 ( c) of Γ( c) is such that (since the constants c do not appear in T ). θ( x) ∈ Γ is a universal formula witnessing (c) for φ( x). So we prove (1): The key step is to prove the following: Assume the Claim holds and let N realize the above theory. Then . . , c n ), and we are done. So we are left with the proof of the Claim. Proof. Let ψ( x, y) be a quantifier free τ -formula such that ψ( c, a) ∈ ∆ 0 (M) for some a ∈ M. Clearly M models ∃ yψ( c, y). Then the universal formula ¬∃ yψ( c, y) ∈ Γ( c), since M models its negation and Γ( c) at the same time. This gives that We conclude that T ∪ {φ( c) ∧ ψ( c, a)} is consistent for any tuple a 1 , . . . , a k ∈ M and formula ψ such that M models ψ( c, a) (since c, a are constants never appearing in the formulae of T ). This We prove by induction on n that Π n -formulae and Σ n -formulae are Tequivalent to a Π 1 -formula. (c) gives the base case n = 1 of the induction for Σ 1 -formulae and (trivially) for Π 1 -formulae. Assuming we have proved the implication for all Σ n formulae for some fixed n > 0, we obtain it for Π n+1 -formulae ∀ xψ( x, y) (with ψ( x, y) Σ n ) applying the inductive assumptions to ψ( x, y); next we observe that a Σ n+1 -formula is equivalent to the negation of a Π n+1 -formula, which is in turn equivalent to the negation of a universal formula (by what we already argued), which is equivalent to an existential formula, and thus equivalent to a universal formula (by (c)). an existential formula (since its negation is T -equivalent to a universal formula). This gives that M ≺ N whenever M ⊑ N are models of T , since truth of universal formulae is inherited by substructures, while truth of existential formulae pass to superstructures. We will also need the following: Fact 1.16. Let τ be a signature and T a model complete τ -theory. Let σ ⊇ τ be a signature and T * ⊇ T a σ-theory such that every σ-formula is T * -equivalent to a τ -formula. Then T * is model complete. Proof. By the model completeness of T and the assumptions on T * we get that every σ-formula is equivalent to a Π 1 -formula for τ ⊆ σ. We conclude by Robinson's test. Later on we will show that in most cases model complete theories maximize the family of Π 2 -sentences compatible with any Π 1 -completion of their universal fragment. This will be part of a broad family of properties for first order theories which require a new concept in order to be properly formulated, that of model companionship. Model completeness comes in pairs with another fundamental concept which generalizes to arbitrary first order theories the relation existing between algebraically closed fields and commutative rings without zero-divisors. As a matter of fact, the case described below occurs when T * is the theory of algebraically closed fields and T is the theory of commutative rings with no zero divisors. Definition 1.17. Given two theories T and T * in the same language τ , T * is the model companion of T if the following conditions holds: (1) Each model of T can be extended to a model of T * . (2) Each model of T * can be extended to a model of T . (3) T * is model complete. Different theories can have the same model companion, for example the theory of fields and the theory of commutative rings with no zero-divisors which are not fields both have the theory of algebraically closed fields as their model companion. Proof. (1) By Lemma 1.4. (2) By Robinson's test 1.15 T * is the theory realized exactly by the T * -ec models; by An immediate by-product of the above Theorem is that the model companion of a theory does not necessarily exist, but, if it does, it is unique and is its Kaiser hull. Moreover T * is the unique model companion of T and is characterized by the property of being the unique model complete theory S such that S ∀ = T ∀ . Proof. For quantifier free formulae ψ( x, y) and φ( x, z) the assertion Let T * * be the theory given by the Π 2 -consequences of T * . Since T * is model complete, by Robinson's test 1.15(c), for any Again by Robinson's test 1.15(c) T * * is model complete. Now assume S is a model complete theory such that S ∀ = T ∀ . Clearly T * ∀ = T ∀ = S ∀ . By Robinson's test 1.15(b) and Proposition 1.8(2), S ∀ holds exactly in the T ∀ -ec models, but these are exactly the models of T * . Hence T * = S. This shows that any model complete theory is axiomatized by its Π 2 -consequences, that the model companion T * of T is unique, that T * is also the Kaiser hull of T (being axiomatized by the Π 2 -sentences which hold in all T -ec-models), and is characterized by the property of being the unique model complete theory S such that T ∀ = S ∀ . Thm. 1.19 provides an equivalent characterization of model companion theories (which is expressible by a ∆ 0 -property in parameters T and T * , hence absolute for transitive models of ZFC). Note also that Robinson's test 1.15(d) gives an explicit axiomatization of a model complete theory T : Proof. First of all T * = AX T ψ : ψ a τ -formula is a model complete theory, since T * satisfies Robinson's test 1.15(d). Let S = T * + T ∀ . Note that S is also model complete (by Robinson's test 1.15(d)). Moreover S ⊆ T (since AX T ψ ∈ T for all Σ 1 -formulae ψ), and S ∀ ⊇ T ∀ (since T ∀ is certainly among the universal consequences of S). We conclude that S ∀ = T ∀ . Therefore S is the model companion of T . S = T by uniqueness of the model companion. We use the following criteria for model companionship in the proofs of Theorems 2.6, 4.4, 5. Proof. By assumption T 0 is consistent with any finite subset of T ∀ ; hence, by compactness, T * = T 0 + T ∀ is consistent. By Fact 1.16 T * is model complete. (1) We need to show that any model of T * embeds into a model of T and conversely. Assume N models T * . Then N models T ∀ . By Lemma 1.4 there exists M ⊒ N which models T . Conversely let M model T and S be the τ -theory of M. By assumption (and compactness) there is N which models T 0 + S ∀ (but this N may not be a superstructure of M). Let S * be the τ -theory of N . Assume the Claim holds, then M is a τ -substructure of a model of S * ⊇ T * and we are done. Since none of the constant in a occurs in τ , we get that (2) Assume ψ ∈ T * and S is a Π 1 -complete extension of T , we must show that S ∀ +ψ is consistent: by assumption there is N which models T 0 +S ∀ = T 0 +T ∀ +S ∀ = T * +S ∀ , and we are done. Conversely assume R ∀ + ψ is consistent whenever R is a Π 1complete extension of T . We must show that ψ ∈ T * : pick M model of T * and let S be its theory. The assumptions of the Lemma (and compactness) grant that (3) can be proved for all theories T admitting a model companion: following the notation of the Lemma, it is conceivable that some τ -theory T has a model companion T * , but there is some universal τ -sentence θ such that for any model M of T + θ any superstructure of M which models T * kills the truth of θ. In this case some Π 2 -sentence in the Kaiser hull of T is inconsistent with the universal fragment of T + θ. Note also that if T * is the model companion of T and θ is a universal sentence such that 1.5. Is model companionship a tameness notion? As we already outlined in the introduction model completeness and model companionship are "tameness" notion for first order theories which must be handled with care. We spell out the details in this small section. Proposition 1.23. Given a signature τ consider the signature τ * which adds an n-ary predicate symbol R φ for any τ -formula φ(x 1 , . . . , x n ) with displayed free variables. Let T τ be the following τ * -theory: Then any τ -structure N admits a unique extension to a τ * -structure N * which models T τ . Moreover every τ * -formula is T τ -equivalent to an atomic τ * -formula. In particular for any τ -model N , the algebras of its τ -definable subsets and of the τ * -definable subsets of N * are the same. Therefore for any consistent τ -theory T , T ∪ T τ is consistent and admits quantifier elemination, hence is model complete. Proof. By an easy induction one can prove that any Another simple inductive argument brings that any τ * -formula φ( x) is T τ -equivalent to the τ -formula obtained by replacing all symbols R ψ ( x) occurring in φ by the τ -formula ψ( x). Combining these observations together we get that any τ * -formula is equivalent to an atomic τ * -formula. T τ forces the M * -interpretation of any relation symbol Observe that the expansion of the language from τ to τ * behaves well with respect to several model theoretic notions of tameness distinct from model completeness: for example T is a stable τ -theory if and only if so is the τ * -theory T ∪ T τ , the same holds for NIP-theories, or for o-minimal theories, or for κ-categorical theories. The passage from τ -structures to τ * -structures which model T τ can have effects on the embeddability relation; for example assume M ⊑ N is a non-elementary embedding of τ -structures; then M * ⊑ N * : if the non-atomic τ -formula φ( a) in parameter a ∈ M <ω holds in M and does not hold in N , the atomic τ * -formula R φ ( a) holds in M * and does not hold in N * . However if T is a model complete τ -theory, then for M ⊑ N τ -models of T , we get that M ≺ N ; this entails that M * ⊑ N * , which (by the quantifier elimination of T ∪ T τ ) gives that M * ≺ N * . In particular for a model complete τ -theory T and M, N τ -models of T , M ⊑ N if and only if M * ⊑ N * . Let us now investigate the case of model companionship. If T is the model companion of S with S = T in the signature τ , T ∪ T τ and S ∪ T τ are both model complete theories in the signature τ * . But T ∪ T τ cannot be the model companion of S ∪ T τ , by uniqueness of the model companion, since each of these theories is the model companion of itself and they are distinct. Moreover if T and S are also complete, no τ * -model of S ∪ T τ can embed into a τ * -model of T ∪ T τ : since T is the model companion of S and S = T , T ∀ = S ∀ and there is some 1.6. Summing up. The results of this section gives that for any τ -theory T : • The universal fragment of T describes the family of substructures of models of T , and (in most cases, e.g. if T is Π 1 -complete) the T -ec models realize all Π 2sentences which are "absolutely" consistent with T ∀ (i.e. consistent with the universal fragment of any extension of T ). • Model companionship and model completeness describe (almost all) the cases in which the family of Π 2 -sentences which are "absolutely" consistent with T (as defined in the previous item) describes the elementary class given by the T -ec structures. • One can always extend τ to a signature τ * so that T has a conservative extension to a τ * -theory T * which is model complete, but this process may be completely uninformative since it may completely destroy the substructure relation existing between τ -models of T (unless T is already model complete). • On the other hand for certain theories T (as the axiomatizations of set theory considered in the present paper), one can unfold their "tameness" by carefully extending τ to a signature τ * in which only certain τ -formulae are made equivalent to atomic τ * -formulae. In the new signature T can be extended to a conservative extension T * which has a model companionT , while this process has mild consequences on the τ * -substructure relation for models of T * ∀ (i.e. for the pairs of interest of τ -models M 0 ⊑ M 1 of a suitable fragment of T , their unique extensions to τ * -models M * i are still models of T * ∀ and maintain that M * 0 ⊑ M * 1 also for τ * ). This gives useful structural information on the web of relations existing between τ * -models of T * ∀ (as outlined by Theorems 2.6, 4.4, 5). • Our conclusion is that model completeness and model companionship are tameness properties of elementary classes E defined by a theory T rather than of the theory T itself: these model-theoretic notions outline certain regularity patterns for the substructure relation on models of E, patterns which may be unfolded only when passing to a signature distinct from the one in which E is first axiomatized (much the same way as it occurs for Birkhoff's characterization of algebraic varieties in terms of universal theories). • The results of the present paper shows that if we consider set theory together with large cardinal axioms as formalized in the signature σ ω , σ ω,NSω 1 , σ ω 1 , we obtain (until now unexpected) tameness properties for this first order theory, properties which couple perfectly with well known (or at least published) generic absoluteness results. The notion of companionship spectrum gives a model theoretic criterium for selecting these signatures out of the continuum many signatures which produce definable extensions of ZFC. Moreover the common practice of set theory (independently of our results) motivate the choice of signatures for set theory made in the present paper (signatures which belong to the companionship spectrum of set theory), and our results validate it. In this section we prove Thm. 1 The following piece of notation will be used all along this section and supplements Notations 1, 3: • σ ST is the signature containing a predicate symbol S φ of arity n for any ∈-formula φ with n-many free variables. • T κ is the σ ST ∪ {κ}-theory given by the axioms as ψ ranges over the ∈-formulae. 2.1. By-interpretability of the first order theory of H κ + with the first order theory of P (κ). Let's compare the first order theory of the structure (P (κ) , S V φ : φ an atomic τ ST -formula) with that of the τ ST -theory of H κ + in models of ZFC ST . We will show that they are ZFC τ STprovably by-interpretable with a by-interpetation translating H κ + in a Π 1 -definable subset of P κ 2 and atomic predicates into Σ 1 -relations over this set. This result is the key to the proof of Thm. 1 and is just outlining the model theoretic consequences of the well-known fact that sets can be coded by well-founded extensional graphs. Definition 2.3. Given a ∈ H κ + , R ∈ P κ 2 codes a, if R codes a well-founded extensional relation on some α ≤ κ with top element 0 so that the transitive collapse mapping of (α, R) maps 0 to a. • WFE κ is the set of R ∈ P (κ) which are a well founded extensional relation with domain α ≤ κ and top element 0. • Cod κ : WFE κ → H κ + is the map assigning a to R if and only if R codes a. The following theorem shows that the structure (H κ + , ∈) is interpreted by means of "imaginaries" in the structure (P (κ) , τ V ST ) by means of: • a universal τ ST ∪{κ}-formula (with quantifiers ranging over subsets of κ <ω ) defining a set WFE κ ⊆ P κ 2 . • an equivalence relation ∼ = κ on WFE κ defined by an existential τ ST ∪ {κ}-formula (with quantifiers ranging over subsets of κ <ω ) • A binary relation E κ on WFE κ invariant under ∼ = κ representing the ∈-relation as the extension of an existential τ ST ∪ {κ}-formula (with quantifiers ranging over subsets of κ <ω ) 11 . Theorem 2.4. Assume ZFC − κ . The following holds 12 : (1) The map Cod κ and WFE κ are defined by ZFC − κ -provably ∆ 1 -properties in parameter κ. Moreover Cod κ : WFE κ → H κ + is surjective (provably in ZFC − κ ), and WFE κ is defined by a universal τ ST ∪ {κ}-formula with quantifiers ranging over subsets of κ <ω . (2) There are existential τ ST ∪ {κ}-formulae (with quantifiers ranging over subsets of κ <ω ), φ ∈ , φ = such that for all R, S ∈ WFE κ , φ = (R, S) if and only if Cod κ (R) = Cod κ (S) and φ ∈ (R, S) if and only if Cod κ (R) ∈ Cod κ (S). In particular letting we prove the results for a transitive model (N, ∈) which is then extended to a structure (N, τ N ST , κ N ) which models ZFC − κ , and whose domain contains H κ + . The reader can verify by itself that the argument is modular and works for any other model of ZFC − κ (transitive or ill-founded, containing the "true" H κ + or not). (1) This is proved in details in [13, Chapter IV] . To define WFE κ by a universal τ ST ∪ {κ}-property over subsets of κ and Cod κ by a ∆ 1 -property for τ ST ∪ {κ} over H κ + , we proceed as follows: • R is an extensional relation with domain contained in κ and top element 0 is defined by the τ ST ∪ {κ}-atomic formula ψ EXT (R) ZFC − κ -provably equivalent to the ∆ 0 (κ)-formula: Then Cod κ (R) = a can be defined either by the existential τ ST ∪{κ}-formula 13 In particular we get that S φ= (R, S) holds in H κ + for R, S ∈ WFE κ if and only if Cod κ (R) = Cod κ (S). 13 Given an R such that ψEXT(R) holds, R is a well founded relation holds in a model of ZFC − κ if and only if Codκ is defined on R. In the theory ZFC − κ , WFEκ can be defined using a universal property by a τ ST ∪ {κ}-formula quantifying only over subsets of κ. On the other hand if we allow arbitrary quantification over elements of H κ + , we can express the well-foundedness of R also using the existential formula ∃G ψ Codκ (G, R). This is why WFEκ is defined by a universal τ ST ∪ {κ}-property in the structure (P (κ) , τ V ST , κ), while the graph of Codκ can be defined by a ∆1-property for τ ST ∪ {κ} in the structure Similarly one can express Cod κ (R) ∈ Cod κ (S) by the Σ 1 -property φ ∈ in τ κ stating that (Ext(R), R) is isomorphic to (pred S (α), S) for some α ∈ κ with α S 0, where pred S (α) is given by the elements of Ext(S) which are connected by a finite path to α. Moreover letting ∼ = κ ⊆ WFE 2 κ denote the isomorphism relation between elements of WFE κ and E κ ⊆ WFE 2 κ denote the relation which translates into the ∈-relation via Cod κ , it is clear that ∼ = κ is a congruence relation over E κ , i.e.: if This gives that the structure (WFE κ /∼ =κ , E κ /∼ =κ ) is isomorphic to (H κ + , ∈) via the map [R] → Cod κ (R) (where WFE κ /∼ =κ is the set of equivalence classes of ∼ = κ and the quotient relation This isomorphism is defined via the map Cod κ , which is by itself defined by a Model completeness for the theory of H κ + . Theorem 2.5. Any σ κ -theory T extending Proof. To simplify notation, we conform to the assumption of the previous theorem, i.e. we assume that the model (N, ∈) which is uniquely extended to a model of ZFC * − κ + every set has size κ on which we work is a transitive superstructure of H κ + . The statement every set has size κ is satisified by a ZFC − κ -model (N, τ V ST , κ) with N ⊇ H + κ if and only if N = H κ + . From now on we proceed assuming this equality. By Robinson's test 1.15 it suffices to show that for all ∈-formulae φ( x) ZFC − κ + every set has size κ ⊢ ∀ x (φ( x) ↔ ψ φ ( x)), for some universal σ κ -formula ψ φ . We will first define a recursive map φ → θ φ which maps Σ n -formulae φ for {∈, κ} quantifying over all elements of H κ + to Σ n+1 -formulae θ φ for τ ST ∪ {κ} whose quantifier range just over subsets of κ <ω . The proof of the previous theorem gave τ ST ∪ {κ}-formulae θ x=y , θ x∈y such that . Specifically (following the notation of that proof) y) . Now for any {∈, κ}-formula ψ( x), we proceed to define the τ ST ∪ {κ}-formula θ ψ ( x) letting: An easy induction on the complexity of the τ ST ∪ {κ}-formulae θ φ ( x) gives that for any {∈, κ}-definable subset A of (H κ + ) n which is the extension of some {∈, κ}-formula φ(x 1 , . . . , x n ) with the further property that S Now every σ κ -formula is ZFC * − κ -equivalent to a {∈, κ}-formula 15 . Therefore we can extend φ → θ φ assigning to any σ κ -formula φ( x) the formula θ ψ ( x) for some {∈, κ}-formula ψ( x) which is ZFC * − κ -equivalent to φ( x). Then for any {∈, κ}-formula φ(x 1 , . . . , x n ) H κ + |= φ(a 1 , . . . , a n ) if and only if with Cod κ (R i ) = a i for i = 1, . . . , n if and only if if and only if Since this argument can be repeated verbatim for any model of ZFC * − κ +every set has size κ, and any σ κ -formula is ZFC * − κ -equivalent to a {∈, κ}-formula, we have proved the following: But Cod κ (y) = x is expressible by an existential τ ST ∪ {κ}-formula provably in ZFC − κ ⊆ ZFC * − κ , therefore is a universal σ κ -formula, and we are done. Proof of Thm. 1. Conforming to the notation of Thm. 1, it is clear that σ κ is a signature of the form {∈}Ā κ whenever κ is a T -definable cardinal for some T extending ZFC. Therefore the following result completes the proof of Thm. 1. Theorem 2.6. Assume T ⊇ ZFC * κ is a σ κ -theory. Then T has a model companion T * . Moreover for any Π 2 -sentence ψ for σ κ , TFAE: (1) ψ ∈ T * ; (2) T ⊢ ψ H κ + ; (3) For all universal σ κ -sentences θ, T + θ is consistent if and only if so is T ∀ + θ + ψ. 14 It is also clear from our argument that the map φ → θ φ is recursive (and a careful inspection reveals that it maps a Σn-formula to a Σn+1-formula). 15 The map assigning to any σκ-formula a ZFC * − κ -equivalent {∈, κ}-formula can also be chosen to be recursive. Proof. By Thm. 2.5, any σ κ -theory extending ZFC * − κ + every set has size κ is model complete. Therefore so is κ + models ZFC * − κ +every set has size κ for any M which models T . We must now show that T * ∀ = T ∀ . Assume T * |= θ for some universal sentece θ. Then H M κ + |= θ for any model M of T . Since H M κ + ≺ 1 M for any such M, we get that any such M models θ as well. Therefore T * ∀ ⊆ T ∀ . Appealing again to Levy absoluteness, by a similar argument, we get that T ∀ ⊆ T * ∀ . We now show that T * is the set of Π 2 -sentences φ such that: For all Π 1 -sentences φ for τ , T +θ is consistent if and only if so is T ∀ +φ+θ. We prove it establishing that T and T * satisfy the assumption of Lemma 1.21 i.e. for any Π 1 -sentence θ for σ κ T + θ is consistent if and only if so is T * + θ. So assume T + θ is consistent for some Π 1 -sentence θ, we must show that T * + θ is also consistent, but this is immediate: by Levy absoluteness if M models θ, so does H M κ + . Conversely assume T + θ is inconsistent for some Π 1 -sentence θ. Then T |= ¬θ. Again by Levy absoluteness if M models T , H M κ + |= ¬θ. Hence ¬θ ∈ T * by definition, and θ is inconsistent with T * . Remark 2.7. Note that the family of models H M κ + : M |= T we used to define T * may not be an elementary class for σ κ . Thm. 2.6 can be proved for many other signatures other than σ κ . It suffices that the signature in question adds new predicates just for definable subsets of P (κ) n , and also that it adds family of predicates which are closed under definability (i.e. projections, complementation, finite unions, permutations) and under the map Cod κ . Under these assumptions we can still use Lemma 1 and Fact 1.13 to argue for the evident variations of the proof of Thm. 2.6 to this set up. However linking these model companionship results to generic absoluteness as we do in Theorem 2 requires much more care in the definition of the signature. We will pursue this matter in more details in the next sections. A weak version of Theorem 2 for third order arithmetic. We can prove a weak version of Thm. 2 for the theory of H ℵ 2 appealing to the generic absoluteness results of [4, 5, 23] which establish the invariance of the theory of H ℵ 2 in models of strong forcing axioms with respect to stationary set preserving forcings preserving these axioms. Let ZFC * ω 1 ⊇ ZFC ST be the σ ω 1 = σ ω ∪ {κ}-theory obtained adding axioms which force in each of its σ ω 1 -models κ to be interpreted by the first uncountable cardinal, and each predicate symbol S φ to be interpreted as the subset of P (ω <ω 1 ) n defined by φ P(ω <ω 1 ) (x 1 , . . . , x n ). Theorem 2.8. Let T be a σ ω 1 -theory extending ZFC * ω 1 + MM +++ + there are class many superhuge cardinals. TFAE for any Π 2 -sentence ψ for σ ω 1 : (1) S ∀ + ψ is consistent for all complete S extending T ; (2) T proves that some stationary set preserving forcing notion P forces ψḢ ω 2 + MM +++ ; (3) T ⊢ ψ Hω 2 . See Remarks 2.9(2) for some information on MM +++ , and 2.9(1) for informations on superhugeness. The proof of Theorem 2.8 is a trivial variation of the proof of Theorem 2.6: one can choose the theory T to be inconsistent with MM ++ without hampering its conclusion (for example T could satisfy CH, a statement denied by MM ++ ), and because Corollary 1(C) holds for all forcing notions P unlike Thm. 2.8 (2) . The key point separating these two results is that the signature σ ω 1 is too expressive and renders many statements incompatible with forcing axioms formalizable by existential (or even atomic) σ ω 1 -sentences (for example such is the case for CH). (5) A key distinction between the signature σ ω 1 and the signature {∈}Ā 2 considered in Thm. 2 is that for any T ⊇ ZFC+appropriate large cardinals CH cannot be Tequivalent to a Σ 1 -sentence for {∈}Ā 2 because CH is a statement which can change its truth value across forcing extensions, while the universal {∈}Ā 2 -sentences maintain the same truth value across all forcing extensions of a model of T , by Thm. 2(5). On the other hand CH is ZFC ω 1 -equivalent to an atomic σ ω 1 -sentence. ¬CH is the simplest example of the type of Π 2 -sentences which exemplifies why Thm. 2.8(2) is much weaker than Thm. 2, and why Thm. 2 for the signature {∈}Ā 2 needs a different (and as we will see much more sophisticated) proof strategy than the one we use here to establish Theorems 2.6 and 2.8. We collect here generic absoluteness results results needed to prove Thm. 2. We prove all these results working in "standard" models of ZFC, i.e. we assume the models are well-founded. This is a practice we already adopted in Section 2. We leave to the reader to remove this unnecessary assumption. 3.1. Universally Baire sets and generic absoluteness for second order number theory. We recall here the properties of universally Baire sets and the generic absoluteness results for second order number theory we need to prove Thm. 2. Notation 3.1. A ⊆ n∈ω P (κ) n is projectively closed if it is closed under projections, finite unions, complementation, and permutations (if σ : n → n is a permutation and A ⊆ P (κ) n ,σ[A] = (a σ(0) , . . . , a σ(n−1 ) : (a 0 , . . . , a n−1 ) ∈ A ). Otherwise said, A is the class of lightface definable subsets of some signature on P (κ). Universally Baire sets. Assuming large cardinals there is a very large sample of projectively closed families of subsets of P (ω) which are are "simple", hence it is natural to consider elements of these families as atomic predicates. The exact definition of what is meant by a "simple" subset of 2 ω is captured by the notion of universally Baire set. Given a topological space (X, τ ), A ⊆ X is nowhere dense if its closure has a dense complement, meager if it is the countable union of nowhere dense sets, with the Baire property if it has meager symmetric difference with an open set. Recall that (X, τ ) is Polish if τ is a completely metrizable, separable topology on X. UB denotes the family of universally Baire subsets of X for some Polish space X. We adopt the convention that UB denotes the class of universally Baire sets and of all elements of n∈ω+1 (2 ω ) n (since the singleton of such elements are universally Baire sets). The theorem below outlines three simple examples of projectively closed families of universally Baire sets containing 2 ω . To proceed further we now list the standard facts about universally Baire sets we will need: Hence it is not restrictive to focus just on universally Baire subsets of 2 ω and of its countable products, which is what we will do in the sequel. Generic absoluteness for second order number theory. The following generic absoluteness result is the key to establish Thm. 2(5) for the signature A 1 . We decide to include a full proof of Woodin's generic absoluteness results for second order number theory we use in this paper. The version we need follows readily from [15, Thm. 3.1.2] and the assumptions that there exists class many Woodin limits of Woodin; here we reduce these large cardinal assumptions to the existence of class many Woodin cardinals, while providing an alternative approach to the proof of some of these result. The theorem below is an improvement of [24, Thm. 3.1]. Theorem 3.5. Assume in V there are class many Woodin cardinals. Let A ∈ V be a family of universally Baire sets of V and τ A = τ ST ∪ A. Let G be V -generic for some forcing notion P ∈ V . Then We proceed by induction on n to prove the following stronger assertion: This proves the base case of the induction. We prove the successor step. Assume that for any G V -generic for some forcing P ∈ V and H V [G]-generic for some FixḠ andH as in the assumptions of the Claim as witnessed by forcingsP ∈ V and Q ∈ V [Ḡ]. We want to show that Let γ be a Woodin cardinal of V such thatP * Q ∈ V γ (whereQ ∈ V P is chosen so thaṫ Q G =Q). Then γ is Woodin also in V [Ḡ]. Let K be V [Ḡ]-generic for 16 Hence we have the following diagram: Let φ ≡ ∃xψ(x) be any Σ n+1 formula for τ A with parameters in H the formula φ holds also in (H . Since φ is arbitrary, this shows that concluding the proof of the inductive step forḠ andH. Since we have class many Woodin, this argument is modular inḠ,H as in the assumptions of the inductive step, because we can always find some Woodin cardinal γ of V which remains Woodin in V [Ḡ] and is of size larger than the poset in V [Ḡ] for whichH is V [Ḡ]-generic. The proof of the inductive step is completed. Generic invariance for the universal fragment of the theory of V with predicates for the non-stationary ideal and for universally Baire sets. The results of this section are the key to establish Thm. 2(5) for the signature A 1 . The proofs require some familiarity with the basics of the P max -technology and with Woodin's stationary tower forcing. Notation 3.6. • τ NS ω 1 is the signature τ ST ∪ {ω 1 } ∪ {NS ω 1 } with ω 1 a constant symbol, NS ω 1 a unary predicate symbol. • T NS ω 1 is the τ NS ω 1 -theory given by T ST together with the axioms ω 1 is the first uncountable cardinal, The following is the key to establish Thm. 2(5) for the signature A 2 . Theorem 3. Assume (V, ∈) models ZFC+ there are class many Woodin cardinals. Then the Π 1 -theory of V for the language τ NS ω 1 ∪ UB V is invariant under set sized forcings 17 . Asperó and Veličkovic provided the following basic counterexample to the conclusion of the theorem if large cardinal assumptions are dropped. Remark 3.7. Let φ(y) be the ∆ 1 -property in τ NSω 1 ∃y(y = ω 1 ∧ L y+1 |= y = ω 1 ). Then L models this property, while the property fails in any forcing extension of L which collapses ω L 1 to become countable. In order to prove the Theorem we need to recall some basic terminology and facts about iterations of countable structures. • each j αα is the identity mapping, • each j αα+1 is the ultrapower embedding induced by G α , • for each limit ordinal β ≤ γ, M β is the direct limit of the system {M α , j αδ : α ≤ δ < β}, and for each α < β, j αβ is the induced embedding. We adopt the convention to denote an iteration J just by j αβ : α ≤ β ≤ γ , we also stipulate that if X denotes the domain of j 0α , X α or j 0α (X) will denote the domain of j αβ for any α ≤ β ≤ γ. [14, Thm. 4.10] ). 18 A result of Shelah whose outline can be found in [19, Chapter XVI] , or [25] , or in an handout of Schindler available on his webpage. This gives that X γ ⊑ Ult(V, G) for τ NSω 1 ∪ UB V . Since V δ [g] |= ¬φ, so does X γ , by elementarity. But ¬φ is a Σ 1 -sentence, hence it is upward absolute for superstructures, therefore Ult(V, G) |= ¬φ. This is a contradiction, since Ult(V, G) is elementarily equivalent to V for τ NS ω 1 ∪ UB V , and V |= φ. A similar argument shows that if V models a Σ 1 -sentence φ for τ NS ω 1 ∪ UB V this will remain true in all of its generic extensions: Assume V [h] |= ¬φ for some h V -generic for some forcing notion P ∈ V . Let γ > |P | be a Woodin cardinal, and let g be V -generic for 19 T γ with h ∈ V [g] and crit(j g ) = ω V 1 (hence there is in g some stationary set of V γ concentrating on countable sets). Then V [g] |= φ since: Assume τ is a projective signature for S ⊇ ZFC τ . A ⊆ F τ is S-projectively closed if: (A) A is closed under logical equivalence; (B) for any (V, τ ) model of S, any formula in A defines a subset of ((2 ω ) V ) k for some k ∈ ω; (C) in any model (V, τ ) of S, if B is a definable subset of ((2 ω ) V ) k in the structure (1) The family of lightface definable projective sets of reals. 19 Tγ is the full stationary tower of height γ whose conditions are stationary sets in Vγ , denoted as P<γ in [15] , see in particular [15, Section 2.5]. (2) l-UB T , i.e. the ∈-formulae defining subsets of (2 ω ) k (as k varies in the natural numbers) which T proves to be the extension of some ∈-formula relativized to L(UB) (the smallest transitive model of ZF containing all the ordinals and the universally Baire sets). ST ) models the existence of class many Woodin cardinals, X ≺ (V θ , ∈) for a large enough θ, and T X is the τ ST ∪ (UB V ∩ X)-theory of V , one also get that τ ST ∪ (UB V ∩ X) is a projective signature for T X and UB V ∩ X is T X -projectively closed (where a universally Baire subset of (2 ω ) k is considered a predicate symbol of arity k; note that X = V θ -i.e. UB V ∩ X = UB V -is possible). Theorem 4.4. Let τ ⊇ τ ST and S be a τ -theory extending ZFC τ such that τ is a projective signature for S. Let A ⊆ F τ be an S-projectively closed family for τ and Then SĀ has as its model companion in signature τĀ It is clear that the above theorem combined with the results of Section 3 proves Thm. 2 and Corollary 1 for A 1 . More precisely: Corollary 4.5. Let S ⊇ ZFC+there are class many Woodin cardinals be a ∈-theory. Then for any A ⊆ F ∈ projectively closed for S and such that φ defines a universally Baire set of reals for any φ in A not a ∆ 0 -formula, lettingĀ = A × {0, 1}, S + TĀ has as model companion the Π 2 -sentences ψ for {∈}Ā such that By Levy's absoluteness Lemma 1, since A includes just formulae definining subsets of (2 ω ) k and the same occurs for the symbols of τ \ τ ST in models of S, share the same Π 1 -theory for the signature τĀ. Therefore (by the useful characterization of model companionship given in Lemma 1.21) it suffices to prove that S * is model complete, where S * is the τĀ-theory common to (H ω 1 , τ V , R V ψ , f V ψ : ψ ∈ A) as (V, τ V ) range over models of S. By Robinson's test (Lemma 1.15(c)), it suffices to show that any existential τĀ-formula is S * -equivalent to a universal τĀ-formula. Let ψ 1 , . . . , ψ k be the formulae in A such that some R ψ i or some f ψ i appears in φ. Let ψ(x 1 , . . . , x n ) be the formula φ(Cod ω (x 1 ), . . . , Cod ω (x n )). Since Cod ω (x) = y is a ∆ 1 -definable predicate in the structure (H ω 1 , τ ST ), we get that ψ(x 1 , . . . , x n ) in A since its extension is a subset of (2 ω ) k in the structure . Now for any a 1 , . . . , a n ∈ H ω 1 : (a 1 , . . . , a n ) if and only if Cod ω (r i ) = a i → R ψ (r 1 , . . . , r n ). This yields that S * ⊢ ∀x 1 , . . . , x n (φ(x 1 , . . . , x n ) ↔ θ ψ (x 1 , . . . , x n )). where θ φ (x 1 , . . . , x n ) is the Π 1 -formula in the predicate R ψ ∈ τĀ It is also convenient to reformulate these notion is a more semantic way which is handy when dealing with a fixed complete first order axiomatization of set theory. Definition 4.6. Let A ⊆ n∈ω P (ω) n . A is H ω 1 -closed if any definable subset of P (ω) n for some n ∈ ω in the structure It is immediate to check that if T is the theory of (V, ∈) and A is a family of universlly Baire subsets of V , A is projectively closed for T for the signature τ ST ∪ A if and only if it is H ω 1 -closed. We get the following: Theorem 4.7. Assume (V, ∈) models ZFC+there are class many Woodin cardinals. Let A ⊆ UB V be H ω 1 -closed and τ A = τ ST ∪ A be the signature in which each element of A contained in P (ω) k is a predicate symbol of arity k. Then for any G V -generic for some Proof. The assumptions grant that ST , A : A V [G] ∈ A) (by Thm. 3.5 and by Lemma 1 applied in V [G]). Now the theory of H V ω 1 in signature τ A is complete and model complete, and is also the τ A -theory of H V [G] ω 1 . We conclude that it is the model companion of the τ A -theory of V [G]. It is also easy to check that ω 1 -closed. Let UB denote the family of universally Baire sets, and L(UB) denote the smallest transitive model of ZF which contains UB (see for details Section 3.2). Our first result shows that in models of large cardinal axioms admitting a strong form of sharp for UB (what is here called MAX(UB)), a strong form of Woodin's axiom ( * ) (what is here called ( * )-UB) can be equivalently formulated as the assertion that the theory of H ℵ 2 is the model companion of the theory of V in a signature admitting a predicate symbol for the non-stationary ideal on ω 1 and predicates for each universally Baire set. (2) NS ω 1 is precipitous 20 and the τ NSω 1 ∪ UB-theory of V has as model companion the τ NSω 1 ∪ UB-theory of H ω 2 . (1) implies (2) does not need the supercompact cardinal. We give rightaway the definitions of MAX(UB) and ( * )-UB. There are class many Woodin cardinals in V , and for all G V -generic for some forcing notion P ∈ V : (1) Any subset of ( -generic for some forcing notion Q ∈ V [G]. Then 21 : We now turn to the definition of ( * )-UB, a natural maximal strengthening of Woodin's axiom ( * ). Key to all results of this section is an analysis of the properties of generic extensions by P max of L(UB). In this analysis MAX(UB) is used to argue (among other things) that all sets of reals definable in L(UB) are universally Baire, so that most of the results established in [14] on the properties of P max for L(R) can be also asserted for L(UB). We will use various forms of Woodin's axiom ( * ) each stating that NS ω 1 is saturated together with the existence of P max -filters meeting certain families of dense subsets of P max definable in L(UB). However in this paper we do not define the P max -forcing. The reason is that in the proof of all our results, we will use equivalent characterizations of the proper forms of ( * ) which do not mention at all P max . We will give at the proper stage the relevant definitions. Meanwhile we assume the reader is familiar with P max or can accept as a blackbox its existence as a certain forcing notion; our reference on this topic is [14] . Definition 5. Let A be a family of dense subsets of P max . • ( * )-A holds if NS ω 1 is saturated 22 and there exists a filter G on P max meeting all the dense sets in A. • ( * )-UB holds if NS ω 1 is saturated and there exists an L(UB)-generic filter G on P max . Woodin's definition of ( * ) [14, Def. 7.5] is equivalent to ( * )-A+there are class many Woodin cardinals for A the family of dense subsets of P max existing in L(R). An objection to Thm. 4 is that it subsumes the Platonist standpoint that there exists a definite universe of sets. At the prize of introducing another bit of notation, we can prove a version of Thm. 4 which makes perfect sense also to a formalist and from which we immediately derive Thm. 2 and Corollary 1 for a certain recursive set of ∈-formulae A 2 . Another key point is that we stick to the formulation of Pmax as in [14] so to be able in its proof to quote verbatim from [14] all the relevant results on Pmax-preconditions we will use. It is however possible to develop Pmax focusing on Woodin's countable tower rather than on the precipitousness of NSω 1 to develop the notion of Pmax-precondition. Following this approach in all its scopes, one should be able to reformulate Thm. 4(2) omitting the request that NSω 1 is precipitous. We do not explore this venue any further. 21 • σ ST is the signature containing a predicate symbol S φ of arity n for any ∈-formula φ with n-many free variables. • T l-UB is the σ ST -theory given by the axioms as ψ ranges over the ∈-formulae. • Accordingly we define ZFC * l-UB , ZFC * l-UB,NSω 1 . A key observation is that ZFC − ST , ZFC − Then T has a model companion T * . Moreover TFAE for any for any Π 2 -sentence ψ for σ ω,NSω 1 : is a forcing extension of V , and V [G] |= ( * )-UB. (C) T proves 23 ∃P (P is a stationary set preserving partial order ∧ P ψḢ ω 2 ). (D) T proves ∃P (P is a partial order ∧ P ψḢ ω 2 ). ) |= T and ψ is ∀x∃y φ(x, y) with φ quantifier free σ ω,NSω 1 -formula, then for all 24 a ∈ H V ω 2 ∃yφ(a, y) is honestly consistent according to V . (G) For any complete theory S ⊇ T, S ∀ ∪ {ψ} is consistent. 23Ḣ ω 2 denotes a canonical P -name for Hω 2 as computed in generic extension by P . 24 See Def. 5.16 for the notion of honest consistency. Note that even if T |= CH, ¬CH is in T * (for example by (E) above). In particular the model companion T * of T may have models whose theory of H ℵ 2 is completely unrelated to that of models of T . Moreover recall again that CH is not expressible as a Π 1 -property in σ ω,NSω 1 for T : it is not preserved by forcing, while T ∀ is. The rest of this section is devoted to proof of Theorems 4 and 5. Crucial to their proof is the recent breakthrough of Asperó and Schindler [2] establishing that ( * )-UB follows from MM ++ . First of all it is convenient to detail more on MAX(UB) and its use in our proofs. . From now on we will need in several occasions that MAX(UB) holds in V (recall Def. 4). We will always explicitly state where this assumption is used, hence if a statement does not mention it in the hypothesis, the assumption is not needed for its thesis. We will use both properties of MAX(UB) crucially: (1) is used in the proof of Lemma 5.8; (2) in the proof of Fact 5.10. Similarly they are essentially used in Remark 5.13. Specifically we will need MAX(UB) to prove that certain subsets of H ω 1 simply definable using an existential formula quantifying over UB are coded by a universally Baire set, and that this coding is absolute between generic extensions, i.e. if It is useful to outline what is the different expressive power of the structures ( . The latter can be seen as a second order extension of H ω 1 , where we also allow formulae to quantify over the family of universally Baire subsets of 2 ω ; in the former quantifiers only range over elements of H ω 1 , but we can use the universally Baire subsets of H ω 1 as parameters. This is in exact analogy between the comprehension scheme for the Morse-Kelley axiomatization of set theory (where formulae with quantifiers ranging over classes are allowed) and the comprehension scheme for Gödel-Bernays axiomatization of set theory (where just formulae using classes as parameters and quantifiers ranging only over sets are allowed). To appreciate the difference between the two set-up, note that that the axiom of determinacy for universally Baire sets is expressible in For all A ⊆ 2 ω there is a winning strategy for one of the players in the game with payoff A, while in There is a winning strategy for some player in the game with payoff A as A ranges over the universally Baire sets. We will crucially use the stronger expressive power of the structure (H ω 1 ∪ UB, τ ST ) to define certain universally Baire sets as the extension in (H ω 1 ∪ UB, τ V ST ) of lightface Σ 1 -properties (according to the Levy hierarchy); properties which require an existential quantifier ranging over all universally Baire sets. A streamline of the proofs of Theorems 4, 5. Let us give a general outline of these proofs before getting into details. From now on we assume the reader is familiar with the basic theory of P max as exposed in [14] . Notation 5.1. For a given family of universally Baire sets A, τ A is the signature τ ST ∪ A, τ A,NSω 1 is the signature τ NS ω 1 ∪ A. The key point is to prove (just on the basis that (V, ∈) |= MAX(UB) + ( * )-UB) the model completeness of the τ UB,NSω 1 -theory of H ω 2 assuming ( * )-UB. To do so we use Robinson's test and we show the following: Assuming MAX(UB) there is a special universally Baire setD UB,NSω 1 defined by an ∈-formula (in no parameters) relativized to L(UB) coding a family of P max -preconditions with the following fundamental property: For any τ UB,NSω 1 -formula ψ(x 1 , . . . , x n ) mentioning the universally Baire predicates B 1 , . . . , B k , there is an algorithmic procedure which finds a universal τ UB,NSω 1 -formula θ ψ (x 1 , . . . , x n ) mentioning just the universally Baire predicates B 1 , . . . , B k ,D UB,NSω 1 such that whenever G is L(UB)-generic for P max . Moreover the definition ofD UB,NSω 1 and the computation of θ ψ (x 1 , . . . , x n ) from ψ(x 1 , . . . , x n ) are just based on the assumption that (V, ∈) is a model of MAX(UB), hence can be replicated mutatis-mutandis in any model of ZFC + MAX(UB). We will need that (V, ∈) is a model of MAX(UB) + ( * )-UB just to argue that in V there is an L(UB)-generic filter G for P max such that 26 H Since in all our arguments we will only use that (V, ∈) is a model of MAX(UB) and (in some of them also of ( * )-UB), we will be in the position to conclude easily for the truth of Theorem 4 and 5. We condense the above information in the following: There is an ∈-formula φ UB,NSω 1 (x) in one free variable such that: (1) ZFC * l-UB + MAX(UB) proves that S φ UB,NSω 1 is universally Baire. There is a recursive procedure assigning to any existential formula φ(x 1 , . . . , whereĠ ∈ L(UB) is the canonical P max -name for the generic filter. 26 It is this part of our argument where the result of Asperò and Schindler establishing the consistency of ( * )-UB relative to a supercompact is used in an essential way. We will address again the role of Asperò and Schindler's result in all our proofs in some closing remarks. Proofs of Thm. 5, and of (1)→(2) of Thm. 4. Theorem 5, (1)→(2) of Theorem 4 are immediate corollaries of the above theorem combined with Asperò and Schindler's proof that MM ++ implies ( * )-UB, and with Theorem 3. We start with the proof of (1)→(2) of Thm. 4 assuming Thm. 5.2 and Thm. 3: Proof. Assume (V, ∈) models ( * )-UB. Then there is a P max -filter G ∈ V such that H is a Σ 1 -elementary substructure of V also according to the signature τ UB,NSω 1 . We conclude (by Thm. 1.19) , since the two theories share the same Π 1 -fragment. The proof of the converse implication requires more information onD UB,NSω 1 then what is conveyed in Thm. 5.2. We defer it to a later stage. We now prove Thm. 5: We start showing that T and T * satisfy the assumptions of Lemma 1.21. This immediately gives (A)⇐⇒(G) for T and T * . We must show: • T * is model complete. • T * is the model companion of T . • For any universal sentence θ, T + θ is consistent if and only if so is and T * + θ. Again with the same recipe described above we can prove that for any universal sentence θ, T + θ is consistent if and only if so is and T * + θ. We leave the details to the reader. What we will do first is to sketch a different proof of Thm. 4.4. This will give us the key intuition on how to defineD UB,NSω 1 . . The setup described above is quite easy to realize (for example M could the transitive collapse of some countable X ≺ V θ for some large enough θ); in particular for any a ∈ H ω 1 and B 1 , . . . , B k ∈ UB, we can find M countable transitive model of a suitable fragment of ZFC with a ∈ H M ω 1 and UB M ⊇ {B 1 , . . . , B k } countable and H ω 1 -closed family of UB-sets in V , such that: is able to compute correctly whether B M encodes a set UB M such that the pair (UB M , M ) satisfies the above list of requirements; here we use crucially the fact that being a model complete theory is a ∆ 0 -property, and also that 27 MAX(UB) implies that the same assumption used in the cited theorem for L(R) holds for L(UB). 28 Recall Def. 4.6. it is possible to encode the structure (H V ω 1 , τ V UB M ) in a single universally Baire set 29 (for example WFE ω × B M ). In particular (H ω 1 ∪ UB, ∈) correctly computes the set D UB of M ∈ H ω 1 such that there exists a universally Baire set B M = UB M with the property that the pair (M, UB M ) realizes the above set of requirements. By MAX(UB),D UB = Cod −1 ω [D UB ] is a universally Baire setD UB . Note moreover thatD UB is defined by a ∈-formula φ UB (x) in no extra parameters; in particular for any model W = (W, E) of ZFC + MAX(UB), we can defineD UB in W and all its properties outlined above will hold relativized to W. For fixed universally Baire sets B 1 , . . . , B k the set D UB,B 1 ,...,B k of M ∈ D UB such that there is a witness UB M of M ∈ D UB with B 1 , . . . , B k ∈ UB M is also definable in ..,B k is universally Baire (note as well thatD UB,B 1 ,...,B k belongs to any L(UB)-closed family A containing B 1 , . . . , B k ). Now take any Σ 1 -formula φ( x) for τ UB mentioning just the universally Baire predicates B 1 , . . . , B k . It doesn't take long to realize that for all a in H ω 1 ..,B k is universally Baire, so the above can be formulated also as: The latter is a Π 1 -sentence in the universally Baire parameterD UB,B 1 ,...,B k . This is exactly a proof that Robinson's test applies to the τ UB V -first order theory of H V ω 1 assuming MAX(UB); i.e. we have briefly sketched a different (and much more convoluted) proof of the conclusion of Thm. 4.4 (using as hypothesis Thm. 4.4 itself). What we gained however is an insight on how to prove Theorem 5.2. We will consider the set D NSω 1 ,UB of M ∈ D UB such that: • (M, NS M ω 1 ) is a P max -precondition which is B-iterable for all B ∈ UB M (according to [14, Def. 4 . It will take a certain effort to prove that assuming ( * )-UB: • for any A ∈ H ω 2 and B ∈ UB, we can find M ∈ D NSω 1 ,UB with B ∈ UB M , a ∈ H M ω 2 , and an iteration J = {j αβ : But this effort will pay off since we will then be able to prove the model completeness of the theory (H ω 2 , τ V NSω 1 ∪ UB V ) using Robinson's test with Cod −1 ω [D NSω 1 ,UB ] in the place ofD UB and replicating in the new setting what was sketched before for (H ω 1 , τ V UB V ). We now get into the details. Notation 5.4. Given a countable family A = {B n : n ∈ ω} of universally Baire sets with each B n ⊆ (2 ω ) kn , we say that B A = n∈ω B n ⊆ n (2 ω ) kn is a code for {B n : n ∈ ω}. Clearly B A is a universally Baire subset of the Polish space n (2 ω ) kn . Definition 5.5. T UB is the ∈-theory of (H ω 1 , τ UB ). A transitive model of ZFC (M, ∈) is UB-correct if there is an H ω 1 -closed (in V ) family UB M of universally Baire sets in V such that: • The map gets the same truth value in (V, ∈) and in (H ω 1 ∪ UB, ∈). We conclude that D UB has the same extension in (V, ∈) and in (H ω 1 ∪ UB, ∈). By MAX(UB)D UB is universally Baire. The existence of class many Woodin cardinals grants that we can always find 31 a universally Baire uniformization of the universally Baire relation onD UB × 2 ω given by the pairs r, B such that B = {B n : n ∈ ω} witnesses Cod ω (r) ∈ D UB . The same argument can be replicated forĒ UB,B 1 ,...,B k . Lemma 5.8. Assume NS ω 1 is precipitous and there are class many Woodin cardinals in V . Let δ be an inaccessible cardinal in V and G be V -generic for Coll(ω, δ). . Then by standard results on iterations (see [14, Lemma 1.5, Lemma 1.6]) J extends uniquely to an iterationJ of V in V [G] such that •j αβ is a proper extension of j αβ for all α ≤ β ≤ γ (i.e. lettingV α =j 0α (V ), we have that j 0α (V δ ) is the rank initial segments of elements ofV α of rank less than j 0α (δ)). •J is a well defined iteration of transitive structures. In particular this shows that V δ is iterable in V [G]. Now fix B ∈ UB V . We must argue that j 0α (B) = B V [G] ∩j 0α (V ). To simplfy notation we assume B ⊆ 2 ω . Let (T B , S B ) be the pair of trees selected in V to define B V [G] . Thenj 0α (V ) |= (j 0α (T B ),j 0α (S B )) projects to complements; clearlyj 0α [T B ] ⊆j 0α (T B ),j 0α [S B ] ⊆j 0α (S B ). Let p : (γ ×2) ω → 2 ω be the projection map. This gives that Similarly By elementarityj 0α ((2 ω ) V \ B) ∪j 0α (B) = (2 ω ) ∩j 0α (V ). These three conditions can be met only if Since J and B were chosen arbitrarily, we conclude that Proof. The assumptions grant that whenever G is Coll(ω, δ) By [14, Lemma 2.8] , for any iterable . UB V ), we get that for every iterable M ∈ H ω 1 and B ∈ UB V ). The conclusion follows. Let M ≥ N be both UB-correct structures, with UB N a witness of N being UB-correct such thatD UB ∈ UB N . Then ]. Therefore N models that there is a countable set UB N M = B N n : n ∈ ω ∈ N coded by the universally Baire set in N B N UB M = n∈ω B N n such that A ∩ M : A ∈ UB N M ∈ M defines the family of universally Baire sets according to M , and such that N models that M is B N iterable for all B N ∈ UB N M . Now N models that n∈ω B N n is a universally Baire set on the appropriate product space. Therefore there is B ∈ UB N such that B ∩ N = n∈ω B N n . Clearly UB N M is computable from B ∩ N . Since we conclude that in V B = n∈ω B n codes a set UB M = {B n : n ∈ ω} witnessing that M is UB-correct. This gives that UB M ⊆ UB N . Therefore (H N ω 1 , τ N UB M ) is also a model of T UB M . By model completeness of T UB M we conclude that , as was to be shown. 5.5. Three characterizations of ( * )-UB. Recall that for a family A of universally Baire sets τ A,NSω 1 = τ ω 1 ∪ A. Assume an iterable N ≥ M is UB-correct with witness UB N such that Then for all iterations . Remark 5.13. A crucial observation is that "x is (NS ω 1 , UB)-ec" is a property correctly definable in (H ω 1 ∪ UB, ∈). Therefore (assuming MAX(UB)) Theorem 5.14. Assume V models MAX(UB). The following are equivalent: (1) Woodin's axiom ( * )-UB holds (i.e. NS ω 1 is saturated, and there is an L(UB)generic filter G for P max such that L(UB)[G] ⊇ P (ω 1 ) V ). (3) NS ω 1 is precipitous and for all A ∈ H ω 2 , B ∈ UB, there is an (NS ω 1 , UB)-ec M with witness UB M , and an iteration J = {j αβ : α ≤ β ≤ ω 1 } of M such that: Theorem 5.14 is the key to the proofs of Theorem 5.2 and to the missing implication in the proof of Theorem 4. Let E B 1 ,...,B k consists of the set of M ∈ D NSω 1 ,UB such that: • M is B j -iterable for all j = 1, . . . , k; • there is UB M witnessing M ∈ D NSω 1 ,UB with B j ∈ UB M for all j. Let alsoĒ B 1 ,...,B k = Cod −1 ω [E B 1 ,...,B k ]. Then T B 1 ,...,B k ,NSω 1 proves thatĒ B 1 ,...,B k is universally Baire. Moreover let T B 1 ,...,B k ,Ē B 1 ,...,B k ,NSω 1 be the natural extension of T B 1 ,...,B k ,NSω 1 adding a predicate symbol forĒ B 1 ,...,B k and the axiom forcing its intepretation to be its definition. Then T B 1 ,...,B k ,Ē B 1 ,...,B k ,NSω 1 models that every Σ 1 -formula φ( x) for the signature τ NS ω 1 ∪ {B 1 , . . . , B k } is equivalent to a Π 1 -formula ψ( x) in the signature τ NS ω 1 ∪ B 1 , . . . , B k ,Ē B 1 ,...,B k . Proof.Ē B 1 ,...,B k is universally Baire by MAX(UB), since E B 1 ,...,B k is definable in (H ω 1 ∪ UB, ∈) with parameters the universally Baire sets B 1 , . . . , B k ,D NS ω 1 ,UB . Given any Σ 1 -formula φ( x) for τ NS ω 1 ∪ {B 1 , . . . , B k } mentioning the universally Baire predicates B 1 , . . . , B k , we want to find a universal formula ψ( x) such that T {B1,...,Bk,ĒB 1 ,...,B k },NSω 1 |= ∀ x(φ( x) ↔ ψ( x)). Let ψ( x) be the formula asserting: For all M ∈ E B 1 ,...,B k , for all iterations J = {j α β : α ≤ β ≤ ω 1 } of M such that: • x = j 0ω 1 ( a) for some a ∈ M , • NS Now the model completeness of T NSω 1 ,UB -grants that any of its models (among which H V ω 2 ) is (T NSω 1 ,UB ) ∀ -ec. This gives that: Therefore any Π 2 -property for τ UB,NSω 1 with parameters in H V ω 2 which holds in Hence in H V ω 2 it holds characterization (3) of ( * )-UB given by Thm. 5.14 and we are done. Theorem 5.17. Assume V models NS ω 1 is precipitous and MAX(UB) holds. TFAE: • ( * )-UB holds in V . • Whenever φ( x) is a Σ 1 -formula for τ UB,NSω 1 in free variables x, and A ∈ H V ω 2 , φ( A) is honestly consistent if and only if it is true in H V ω 2 . We use Schindler and Asperó characterization of ( * )-UB to prove the equivalences of the three items of Thm. 5.14 (the proofs of these implications import key ideas from [2, Lemma 3.2]). We must show that j 0γ : H V ω 2 → H N ω 2 is Σ 1 -elementary for τ NSω 1 ,UB V between (H V ω 2 , τ V ST , UB V , NS V ω 1 ) and (H N ω 2 , τ N ST , B V [G] ∩ N : B ∈ UB V , NS N ω 1 ). Let φ(a) be a Σ 1 -formula for τ NSω 1 ,UB V in parameter a ∈ H V ω 2 with B 1 , . . . , B k ∈ UB V the universally Baire predicates occurring in φ such that 0γ (a) ). We must show that . Remark that the iteration J extends to an iterationJ = j α,β : α ≤ β ≤ γ = (ω 1 ) N of V exactly as already done in the proof of Lemma 5.8. Using -iterable and which realizes φ(j 0γ (a)) holds true as witnessed by N . The following is a key observation: Let J = j αβ : α ≤ β ≤ γ = ω N 1 ∈ H N ω 2 be an iteration witnessing N ≤ V δ . Now for any A ∈ P (ω 1 ) V and B ∈ UB V Since V δ is (NS ω 1 , UB V [G] )-ec in V [G] we get that j 0γ ↾ H V ω 2 is Σ 1 -elementary between H V ω 2 and H N ω 2 for τ NSω 1 ,UB V . There exists an (NS V ω 1 , UB V )-ec structure M with B ∈ UB M and an iterationJ = j αβ : α ≤ β ≤ (ω 1 ) V of M such thatj 0ω 1 (a) = A and Assume φ(A) is honestly consistent for some Σ 1 -property φ(x) in the language τ UB,NSω 1 and A ∈ P (ω 1 ) V . Let B 1 , . . . , B k be the universally Baire predicates in UB mentioned in φ(x). By (3) which project to complement in V [H] and such that B = p[T B ]. Now sincej 0,γ [T B ] ⊆j 0,γ (T B ) andj 0,γ [S B ] ⊆ j 0,γ (S B ), we get that • (2 ω ) V [H] = p is also the projection ofj 0,γ (T B ) and the pair (j 0,γ (T B ),j 0,γ (S B )) projects to complement in V But this pair belongs toM , and (by elementarity ofj 0γ ) B )) projects to complements for Coll(ω, η) Therefore in V [H] s ∈ j 0γ (B)M [H] if and only if s ∈ p ∧ ∀α ∈ β ∈ ω 2 (α ∈ lim(C β ) → C α = C β ∩ α)∧ < δ) whenever δ is Mahlo. In particular the Π 1 -theory for τ ω 2 of any forcing extension V [G] of V can be destroyed in a further forcing extension V [G][H] assuming mild large cardinals. Suppose now we want to find A 3 ⊆ F ∈ so to be able to extend Thm. 2 by: • assuming as base theory ZFC+suitable large cardinal axioms • replacing H ℵ 2 with H ℵ 3 in all statements of the theorem pertaining to A 3 , • requiring that τ ω 2 ⊆ {∈}Ā the universal {∈}Ā 3 -theory of H ℵ 3 Bounded martin's maximum with an asterisk MM ++ implies ( * ) Bounded forcing axioms and the continuum Category forcings. In preparation Absoluteness via resurrection The bounded proper forcing axiom and well orderings of the reals All automorphisms of the Calkin algebra are inner Martin's maximum, saturated ideals, and nonregular ultrafilters Resurrection axioms and uplifting cardinals The third millennium edition, revised and expanded The fine structure of the constructible hierarchy Classical descriptive set theory Set theory Forcing over models of determinacy The stationary tower Set mapping reflection A five element basis for the uncountable linear orders Infinite abelian groups, Whitehead problem and some constructions Perspectives in Mathematical Logic A course in model theory Generic absoluteness and the continuum The model companions of set theory Category forcings, M M +++ , and generic absoluteness for the theory of strong forcing axioms Martin's maximum revisited The axiom of determinacy, forcing axioms, and the nonstationary ideal both realize the theory T UB V of H V ω 1 in this language: on the one hand, τM [H] UB V ) (the leftmost ≺ holds since j 0,γ : V →M is elementary, the rightmost ≺ holds sinceM models MAX(UB)); on the other handSince T UB V is model complete, we get that HM-iterable and which realizes φ(j 0γ (a)). By homogeneity of Coll(ω, η), inM we get that any condition in Coll(ω, η) forces:There exists a τ NSω 1 ,B,-iterable and which realizes φ(j 0γ (a)). By elementarity ofj 0γ we get that in V it holds that:There exists an η > δ such that any condition in Coll(ω, η) forces: "There exists a countable super structureN of V δ with respect to τ NSω 1 ,{B,-iterable and which realizes φ(a)" This procedure can be repeated for any B ∈ UB V , showing that φ(a) is honestly consistent in V .By Schindler and Asperó characterization of ( * ) we obtain that φ(a) holds in (3): Our assumptions grants that the setST , UB V ), and the latter is first order expressible in the predicateD UB ∈ UB V , we get thatThis gives that(since j 0ω 1 (a) = A), and therefore that Do we really need MAX(UB) to establish Thm. 2? It is not at all clear whether the chain of equivalences for ( * )-UB given in Thm. 5 could be proved without appealing to MAX(UB). What we can for sure say is that the equivalence between forcibility and consistency as given by items (D) and (G) of Thm. 5 holds for the signature τ ω 1 and its Π 2 -sentences ψ.More precisely:Theorem 6. Consider any τ ω 1 -theory S extending ZFC ST +ω 1 is the first uncountable cardinal + there are class many supercompact cardinals and which is preserved by any forcing (e.g. S itself or S + T ∀ for any T extending S).Then the Kaiser hull of S is equivalently given by those Π 2 -sentences ψ for τ ω 1 satysfying items (D) or (G) of Thm. 5.Proof. First assume that S proves that ψ Hω 2 is forcible; given a model V of S, by collapsing a supercompact of V to countable one gets some V [G] which models S + MAX(UB) and satisfies the same universal sentence for τ ω 1 as V (by Thm. 3). Hence by forcing over V [G] (which is still a model of S), we get to some V [H] which models ψ Hω 2 + MAX(UB) + S and satisfies the same universal sentence for τ ω 1 as V [G]. Hence we get that ψ is consistent with the universal fragment of any τ ω 1 -completion of S. Now assume ψ is consistent with the universal fragment of any completion of S: Any τ ω 1 -model V of S can be extended (using forcing) to a τ ω 1 -model V [G] of S + MAX(UB)+ ( * )-UB which satisfies the same τ ω 1 -universal sentences of V (again by Thm. 3). Since τ ω 1 ⊆ σ l-UB,NSω 1 and any τ ω 1 -model W of S admits a unique extension to σ l-UB,NSω 1model which interprets correctly the new predicate symbols, we get that ψ is in the model companion of the σ l-UB,NSω 1 -theory of V [G], and also that this model companion is theω 2 . By the equivalence of (B) and (G) of Thm. 5 we get that HUsing a similar argument (and appealing to Lemma 1.21 for the unique extension of S to σ l-UB,NSω 1 which inteprets correctly the new predicate symbols) one can also prove that these Π 2 -sentences ψ for τ ω 1 axiomatize the Kaiser hull of S. We leave the details to the reader.The above argument is not restricted to τ ω 1 and S, but holds mutatis mutandis for many other signatures contained in σ ω,NSω 1 and theories extending ZFC with large cardinals; we leave the details to the reader.Let us also note that for S as above CH cannot be S-equivalent to a Σ 1 -sentence for τ ω 1 , because CH is a statement which can change its truth value across forcing extensions, while the universal τ ω 1 -sentences maintain the same truth value across all forcing extensions of a model of T by Thm. 3.