Forcing as a Local Method of Accessing Small Extensions
Desmond Lau



Purification of Gaussian States by Photon Subtraction
    Mattia Walschaers
    September 9, 2024
=====================================================



§ ABSTRACT 
Fix a set-theoretic universe V. We look at small extensions of V as generalised degrees of computability over V. We also formalise and investigate the complexity of certain methods one can use to define, in V, subclasses of degrees over V. Finally, we give a nice characterisation of the complexity of forcing within this framework.


thmTheorem[section]
innercustomlemLemma

innercustomdefDefinition

lem[thm]Lemma
prop[thm]Proposition
cor[thm]Corollary
conj[thm]Conjecture
ques[thm]Question
*claimClaim
definition
defi[thm]Definition
remark
*rem*Remark
rem[thm]Remark
ex[thm]Example
ob[thm]Observation
fact[thm]Fact
con[thm]Convention
diff[thm]Difficulty

  
      
      






 
empty



§ INTRODUCTION


Within the set-theoretic universe V, there is (based on the author's work to appear) an intuitive notion of computation that canonically partitions sets into their degrees of constructibility. This lends credence to the belief that generative power over a model of set theory is a surrogate for computational power. When dealing with degrees of constructibility, the relevant model of set theory is L. Switching out L for larger inner models makes sense for coarser degree structures.

What if we swop L for V itself? Doing so will obviously result in degrees that are not subclasses of V. What then do they comprise? With meta-theoretic assumptions mildly stronger than 𝖹𝖥𝖢, we can view V as a countable transitive model of 𝖹𝖥𝖢, from which such degrees can be naturally defined as degrees of small extensions. Vaguely, each degree of small extensions is associated with (or rather, represented by) an outer model W of V generated by a set in W over V: here W is called a small extension of V. These degrees, together with the theory of their ordering, seek to capture the spirit of higher-order computations relative to V, the way higher recursion theory do for computations on sets beyond the domain of classical recursion theory. Figure <ref> illustrates this parallel.



Next, we wish to examine (necessarily non-constructive) methods of definably “accessing” small extensions of V within V, or local methods in short. Set forcing is one such method, and a very well-studied one at that. In an application of set forcing, we pick a partially ordered set — also known as a forcing notion — ℙ∈ V, and use a filter meeting all dense subsets of ℙ in V — termed a ℙ-generic filter over V — to generate an extension of V. So the small extensions of V set forcing brings about via ℙ are precisely those in

    {V[g] : g  is a ℙ-generic filter over  V},

a set definable outside V with ℙ and its dense subsets in V as parameters. Consequently, one can view set forcing as a recipe in V for generating small extensions of V based only on parameters in V. The formal treatment of set forcing inspires a list of desiderata for a local method:

    
  *  it should be definable in V,
    
  *  it should map parameters to descriptions of how those parameters are used to define generators of small extensions, and
    
  *  the generators it produces should depend locally on the parameters used to define them. 


A convenient realisation at this juncture is that a recipe and its parameters (or equivalently, the two components of <ref>) can be bundled up into a theory with constraints in interpretation (TCI). TCIs are basically first-order theories endowed with set constraints that may not be first-order expressible. Like standard first-order theories, TCIs admit models, and whether a set X is a model of a TCI 𝔗 depends locally on X and 𝔗. Defining a local method through the language of TCIs and their models thus provides immediate guarantee of <ref>, and is appealing in both its brevity and robustness.

Accompanying the formalisation of local methods, ought to be a notion of relative complexity, a measure which can be utilised to check if one local method is “more complex” than another. Akin to relative computability, we want to define relative complexity as a transitive binary relation on the class of all local methods. There is actually a straightforward way to do this: we say method Y is more complex than method X iff the small extensions of V picked out by Y are a non-trivial refinement of those picked out by X. Connecting the first-order portion of a TCI with the relative complexity relation we defined, leads to the formulation of a complexity hierarchy — the local method hierarchy — very much in line with more notable hierarchies in theoretical computer science (e.g. the arithmetical and polynomial hierarchies).

Leveraging on a novel forcing framework developed in <cit.>, we are able to show that the method of set forcing is exactly Σ_1 (or equivalently, as we shall see, Π_2) in the local method hierarchy. This is the main takeaway of our work presented here. We follow it up with the analysis of certain witnesses to set forcing being more complex than Π_2.

By applying an analogue of the Cantor-Bendixson derivative on a specific class of forcing notions, we prove that every TCI 𝔗∈Π_2 either singles out V or picks out continuum-many (as evaluated in the meta-theory) small extensions of V. The same is long known to be true for forcing notions: a trivial forcing notion gives V as its sole generic extension, whereas a non-trivial one generates continuum-many generic extensions.

One can think of this work as a rigorous foundation for some of the main ideas found in Section 5 of <cit.>. In fact, consolidated here are many results in said section, having been weaved together into a more philosophically compelling and coherent package. For self-containment, we reproduce the more concise proofs from <cit.>, of as many of these results as possible.  



§ DEGREES OF SMALL EXTENSIONS


Extending a structure through means of adjoining “new” objects is commonly seen in mathematics. Here, “new” just means “existing outside of the structure in question”. For example, a standard course in algebra would talk about field extensions the likes of ℚ[√(2)]. In set theory, the subjects of study are models of set theory, often models of 𝖹𝖥𝖢. For convenience, we usually assume such models are countable and transitive. If a countable transitive model of 𝖹𝖥𝖢 (henceforth, CTM) exists, then extensions of it exist, but due to the complicated closure properties required of a model of 𝖹𝖥𝖢, the proof of their existence is much hairier than that of field extensions. 

It turns out that, whenever U is a CTM and W is an extension of U, we can always find an extension of W that is generated over U by a “small set”. Methods of generating such “small extensions” include, but are not limited to, set forcing. In this section, we compare the multiverse of small extensions with the generic multiverse born from set forcing, under the assumption that both multiverses have the same centre. We also introduce the idea of theories with constraints in interpretation (TCIs) to set things up for the next section. 



 §.§ Small Extensions as Degrees



We avoid the usual meta-theoretic concerns regarding forcing and the set-theoretic multiverse by working in the theory 

    𝖹𝖥𝖢 + “there is a transitive model of 𝖹𝖥𝖢”.
 
The existence of CTMs can be proven in this theory.



Given U and W, we say U is an inner model of W (or equivalently, W is a outer model of U) iff

    
  * U and W are CTMs,
    
  * U ⊂ W, and
    
  * ORD^U = ORD^W.




Let W be an outer model of U. Then W is a small extension of U iff for some x ∈ W, W is the smallest CTM W' satisfying

    
  * U ⊂ W', and
    
  * x ∈ W'.

In this case, we say, equivalently,

    
  * x generates W from U, or
    
  * W is a small extension of U generated by x, or
    
  * W = U[x].



The following observation is trivial.


The binary relations 

    
  * “being an outer model of”, and
    
  * “being a small extension of”

are both transitive.


We know that certain sets in outer models can always be used to generate small extensions.


Let W be an outer model of U, and x ∈𝒫(y) ∩ W for some y ∈ U. Then there is a smallest CTM W' satisfying

    
  * U ⊂ W', and
    
  * x ∈ W'.

In other words, U[x] exists.


There is a simple and useful characterisation of small extensions of a CTM.


Let M be a transitive model of 𝖹𝖥𝖢 and X ∈ M. Then there is a set of ordinals c ∈ M such that if N is any transitive model of 𝖹𝖥𝖢 containing c, then X ∈ N. 



Let Y' be the transitive closure of X (under the membership relation ∈) and set Y := Y' ∪{X}. Then Y is ∈-transitive. Choose a bijection f from a cardinal κ into Y. Use ∈' to denote the unique binary relation R on κ such that

    R(α, β)  f(α) ∈ f(β) .

Now apply Gödel's pairing function to code ∈' as a (necessarily unbounded) subset c of κ. 

To recover X from c, first apply the inverse of the pairing function followed by the Mostowski collapse to get Y. Then X is definable from Y as the unique ∈-maximal element of Y. This decoding process is absolute for transitive models of 𝖹𝖥𝖢 because all its components are.



If W is a small extension of U, then for some ordinal κ∈ U, W is generated from U by an unbounded subset of κ. Furthermore, we can choose κ such that

    (U; ∈) “κ is a cardinal”.




Let x ∈ W be such that W = U[x]. By the proof of Proposition <ref>, for some cardinal κ∈ W there is an unbounded subset c of κ in W coding x. Since U is an inner model of W, κ is also a cardinal in U. By Fact <ref>, U[c] exists. Now, U[c] ⊂ W as c ∈ W; but also W ⊂ U[c] because c can be decoded in U[c] to give x and W = U[x].



Let U be a CTM. The outward multiverse centred at U is the set

    𝐌(U) := {W : W  is an outer model of  U}.

The small outward multiverse centred at U is the set

    𝐌_S(U) := {W : W  is a small extension of  U}.



Clearly, 𝐌_S(U) ⊂𝐌(U). By Jensen's remarkable result on “coding the universe” into a real, 𝐌_S(U) is not that much smaller than 𝐌(U).

[Jensen, <cit.>]
Every CTM has an outer model satisfying 

    “ V = L[r]  for some  r ⊂ω”.




Given a CTM U, (𝐌_S(U), ⊂) is a cofinal subposet of (𝐌(U), ⊂).



Let W ∈𝐌(U). Then by Fact <ref>, there is W' ∈𝐌(U) such that W ⊂ W' and W' satisfies

    “ V = L[r]  for some  r ⊂ω”.

Since L^W' = L^U ⊂ U and indeed W' = L^W'[r] for some real r ∈ W' from the outside, necessarily W' = U[r]. But this means W' ∈𝐌_S(U).


We can characterise members 𝐌_S(U) in a way that is conducive to the discussion of relative computability.


Let U be a CTM. Then

    𝐌_S(U)     = {U[x] : x ∈⋃𝐌(U) ∩𝒫(U)}
        = {U[x] : x ∈⋃𝐌(U) ∩𝒫(ORD^U)}.




By Fact <ref> and Proposition <ref>.


Proposition <ref> gives us a natural reducibility relation on 

    𝐍(U) := ⋃𝐌(U) ∩𝒫(ORD^U)

given a CTM U. 


Let U be a CTM. Define the binary relation ≤_U on 𝐍(U) as follows: for x, y ∈𝐍(U),

    x ≤_U y  U[x] ⊂ U[y] .

Given x, y ∈𝐍(U), write x ≡_U y iff x ≤_U y and y ≤_U x.


One can easily check that ≤_U is a preorder, so taking its quotient by ≡_U results in a partial order we shall denote as (𝒟(U), ≤_𝒟(U)).

The case of (𝒟(U), ≤_𝒟(U)) parallels that of the constructibility degrees, in the sense that the former partial order, like the latter one, is isomorphic to a class of set-theoretic universes under inclusion. Specifically, 

    (𝒟(U), ≤_𝒟(U)) ≅ (𝐌_S(U), ⊂) .
 
This motivates viewing (𝒟(U), ≤_𝒟(U)) as degrees of computability over U. These degrees are necessarily non-constructible (and indeed, non-constructive) if U is not a model of “V = L”. Whereas the “constructible in” relation partially orders a partition of an ∈-model of 𝖹𝖥𝖢 and is definable within said model, the field of (𝒟(U), ≤_𝒟(U)) may not be realisable as a partition of any such model. We thus expect the structure of (𝒟(U), ≤_𝒟(U)) to be much more varied and dependent on U, compared to the structure of the constructibility degrees evaluated in U. Nevertheless, we will attempt to stratify (𝒟(U), ≤_𝒟(U)).

Hereon, we shall analyse and reason about (𝒟(U), ≤_𝒟(U)) by moving to (𝐌_S(U), ⊂), so that we can apply set-theoretic arguments and leverage on set-theoretic techniques.



 §.§ Forcing and the Generic Multiverse


Forcing is a technique invented by Cohen in <cit.> to prove that the continuum hypothesis is independent of 𝖹𝖥𝖢. It has since taken on a life of its own, becoming an indispensable tool in set theory, and even in other branches of logic. The modern treatment of forcing is largely due to Scott, Solovay, Silver, and Rowbottom, as communicated by Shoenfield in <cit.>. We shall give a very brief and high-level introduction to forcing, following the layout found in Section 2.4 of <cit.>.

In a typical application of forcing, we start with a CTM, called the ground model. The usual forcing argument can be rewritten to occur entirely in the ground model with respect to a forcing notion that lives therein. Exactly because of this, we often forget the fact that our ground model is a CTM, or at least we eschew mentioning it. This is also why our ground model is conventionally taken to be V itself. 

Forcing parlance dictates a forcing notion to just be a partial order. The crux of forcing is the analysis of generic filters (which may not exist in V) of a forcing notion ℙ∈ V via the forcing relation ⊩_ℙ defined on ℙ in V. Forcing relations are the trick to reasoning about extensions of V without needing to step out of V.


Let ℙ = (P, ≤_ℙ) be a forcing notion, D ⊂ P and A be any set. We say a subset g of P meets D with respect to ℙ in A iff 
    g ∩{p ∈ P : p ∈ D  or ∀ q  (q ≤_ℙ p  q ∉D)}∩ A ≠∅.
 We say g meets D with respect to ℙ iff g meets D with respect to ℙ in V.



Let ℙ = (P, ≤_ℙ) be a forcing notion and 𝔄 = (A; ∈, X) be a structure in a possibly expanded language of set theory. We say a subset g of P is ℙ-generic over 𝔄 (or g is a ℙ-generic subset over 𝔄) iff g meets D with respect to ℙ in A for all D such that

    
  * D ⊂ P
    
  * D is dense in ℙ, and
    
  * D is definable over 𝔄 with parameters in A.

If in addition, g is a filter on ℙ, then we call g a ℙ-generic filter over 𝔄.



Let ℙ be a forcing notion and 𝔄 be a structure. A (ℙ, 𝔄)-generic object is a set definable from a ℙ-generic filter over 𝔄, with parameters from 𝔄.



Let ℙ = (P, ≤_ℙ) be a forcing notion and X be any set. Then there is a structure 𝔄 = (A; ∈) ∈ V such that in every outer model of V, 

    x  is a  (ℙ, 𝔄) -generic object x  is a  (ℙ, V) -generic object

for all x ⊂ X. In fact, we can choose A to be H(κ) for any κ > |trcl({P, X})|.


Given a forcing notion ℙ = (P, ≤_ℙ) in V, the forcing relation ⊩_ℙ^V is a binary relation that relates members of P with formulas parametrised by members of V^ℙ, where V^ℙ is the class of ℙ-names in V. Both V^ℙ and ⊩_ℙ^V are uniformly definable in V over the class of all forcing notions ℙ. ℙ-names in V are “evaluated at" a ℙ-generic filter g over V to obtain the ℙ-generic extension V[g], which is necessarily a CTM, and thus is a small extension of V. In more formal writing, if g is a ℙ-generic filter over V, then

    V ⊂ V[g] := {ẋ[g] : ẋ∈ V^ℙ},

where ẋ[g] means “x evaluated at g". Of course, this evaluation procedure is done outside V because any such non-trivial g would not exist in V. Even so, the ingenuity of forcing as a technique lies in the amount of knowledge we can deduce about V[g] in V through examining ⊩_ℙ^V alone.


When it is clear that the background universe is V, we suppress mention of V when writing forcing relations in V. This means that given a forcing notion ℙ in V, ⊩_ℙ is used interchangeably with ⊩_ℙ^V.



We call W a forcing extension (or a generic extension) of V iff there exists a forcing notion ℙ in V and a ℙ-generic filter g over V, such that W = V[g].



We write “⊩_ℙϕ" to mean 
    “∀ p  (p ∈ℙ p ⊩_ℙϕ) ”.
 


The next theorem is important enough to be stated here in full, but not relevant enough to the spirit of this section to warrant a reproduction of its proof.


If ℙ is a forcing notion in V, p ∈ℙ, ϕ is a formula with n free variables, and ẋ_1, ..., ẋ_n are ℙ-names in V, then

    
  * 
    [t]
        p ⊩_ℙϕ(ẋ_1, …, ẋ_n) 
   ∀ g  ((g  is ℙ-generic over  V  and  p ∈ g) 
    V[g] ϕ(ẋ_1[g], …, ẋ_n[g])),  and
    
  * 
    [t]
    ∀ g  (     (g  is ℙ-generic over  V  and  V[g] ϕ(ẋ_1[g], …, ẋ_n[g])) 
   ∃ q  (q ⊩_ℙϕ(ẋ_1, …, ẋ_n)  and  q ∈ g)) .



Theorem <ref> intricately connects the forcing relation ⊩_ℙ^V with truth in ℙ-generic extensions and is fundamental to forcing as a technique. Colloquially known as the forcing theorem, it enables us to reason about truth in generic extensions from within the ground model, and often reduces the argument from one about semantic entailment to one pertaining to combinatorial properties of partial orders. For more details about forcing and the proof of the forcing theorem, the reader is encouraged to read Chapter IV of <cit.>. 


Define the relation ≤_F on the set of CTMs as follows:

    M ≤_F N  N  is a forcing extension of  M .




A (full) generic multiverse is any set of CTMs closed under ≤_F.



Let V be a CTM. The (forcing) grounds of V is the set

    {W : V  is a forcing extension of  W}.




Let V be a CTM. The outward generic multiverse centred at V is the set

    𝐌_F(V) := {W : W  is a forcing extension of  V}.

 

The study of generic multiverses, including the coining of the term itself, arguably begins with Woodin in <cit.>. Since then, much has been studied about the structure of standard generic multiverses under ≤_F, with a particularly strong focus on the forcing grounds of fixed CTMs. On the other hand, there has been less interest in the structure of outward generic multiverses under ≤_F, perhaps due to the dearth of low-hanging fruits — a large part of what is known about this structure are essentially theorems about forcing in the traditional sense.

A careful reader might have noticed the overloading of the notation · [·] to represent both small extensions and forcing extensions. This is intentional, for the latter class is subsumed under the former.


For some ℙ∈ V, let g be a ℙ-generic filter over a CTM V. Then V[g] is the smallest CTM W for which

    
  * V ⊂ W, and
    
  * g ∈ W.

As a consequence, 𝐌_F(V) ⊂𝐌_S(V).


It turns out that forcing extensions of a CTM V are downward-closed in 𝐌(V) (and thus, also in 𝐌_S(V)). This is just a rephrasing of the fact below.


Let V ⊂ U ⊂ W be CTMs such that

    
  * W is a forcing extension of V, 
    
  * U is an outer model of V, and
    
  * U is an inner model of W.

Then 

    
  * U is a forcing extension of V, and
    
  * W is a forcing extension of U.



An immediate follow-up question to the previous two facts is, 

    “Must 𝐌_F(V) always equal 𝐌_S(V)?”

There is an easy argument for the answer being “no”, if we assume a sufficiently strong large cardinal axiom in addition to 𝖹𝖥𝖢.


Let 

    𝖳 := 𝖹𝖥𝖢 + “0^♯ exists”.
 
Assume 𝖹𝖥𝖢 + “there is a transitive model of  T ”. Then 𝐌_F(V) ⊊𝐌_S(V) for some CTM V.



Given the hypothesis of the proposition, there is a CTM W satisfying 𝖳. Define 

    V := L^W 
    
        U := L[I]^W ,

where I is an uncountable set of Silver indiscernibles in W witnessing the fact that 0^♯ exists. Then U is a small extension of V generated by I ∈ U but not a forcing extension of V.


By Proposition <ref>, it is consistent that 𝐌_S(V) ∖𝐌_F(V) is non-trivial — and includes at least a cone of (𝐌_S(V), ⊂) — under strong enough assumptions. However, the small outward multiverse example exhibited by the proof of the proposition is undesirable because it is centred at a universe that is by many measures, “too small” (e.g. it has a trivial theory of constructibility degrees). 

A much stronger and much more useful statement would be

    “𝐌_F(V) ≠𝐌_S(V)  for all  V ”.

Let us sketch how this can be true. We start with a universe V, force (with a proper class forcing notion) to an outer model V[G] of V satisfying “V[G] is not a set forcing extension of V”, then apply Fact <ref> to V[G]. The end result is an outer model W of V[G] such that W = L^V[r] for some real r ∈ W. This can even be arranged such that V is a definable class in W. Now if W is a set forcing extension of V, then so are all intermediate outer models of V, including V[G]. But we have just ensured V[G] is not a set forcing extension of V. 

This argument, which includes a proof of Fact <ref>, can be formalised in a conservative second order extension of 𝖹𝖥𝖢 (the second-order portion is needed for proper class forcing), so our meta-theory suffices when V is a CTM. We have thus established — albeit sketchily so — the following.


(<ref>) holds.


In actuality, we can switch V for any U ∈𝐌_S(V) in the argument above and obtain a stronger conclusion.


Given a CTM V,

    (𝐌_S(V) ∖𝐌_F(V), ⊂)

is a cofinal subposet of (𝐌_S(V), ⊂).


Intuitively, Facts <ref> and <ref> tell us that there are many objects inaccessible by forcing. Do these objects have “local first-order properties” not shared by any set in any forcing extension? Much of the rest of this paper aims for a partial answer to the aforementioned question. 



 §.§ Theories with Constraints in Interpretation


Theories with constraints in interpretation (henceforth, TCIs) were conceived in <cit.> as a convenient means of looking at generic objects produced by set-theoretic forcing. 

(Lau, <cit.>)
A first-order theory with constraints in interpretation (first-order TCI) — henceforth, just theory with constraints in interpretation (TCI) — is a tuple (T, σ, 𝒰̇, ϑ), where

    
  * T is a first order theory with signature σ,
    
  * 𝒰̇ is a unary relation symbol not in σ,
    
  * ϑ is a function (the interpretation constraint map) with domain σ∪{𝒰̇}, 
    
  * if x ∈ ran(ϑ), then there is y such that 
    
        
  * either x = (y, 0) or x = (y, 1), and
        
  * if ϑ(𝒰̇) = (z, a), then y ⊂ z^n for some n < ω, and
    
    
  * if ϑ(𝒰̇) = (z, a), then 
    
        
  * z ∩ z^n = ∅ whenever 1 < n < ω, and
        
  * z^m ∩ z^n = ∅ whenever 1 < m < n < ω.
    

We call members of the interpretation constraint map interpretation constraints.

For simplicity's sake, we always assume members of T are in prenex normal form.


(Lau, <cit.>)
Let (T, σ, 𝒰̇, ϑ) be a TCI. We say 
    ℳ := (U; ℐ) ^* (T, σ, 𝒰̇, ϑ)
 — or ℳ models (T, σ, 𝒰̇, ϑ) — iff all of the following holds:

    
  * ℳ is a structure,
    
  * σ is the signature of ℳ,
    
  * ℳ T,
    
  * if ϑ(𝒰̇) = (y, 0), then U ⊂ y,
    
  * if ϑ(𝒰̇) = (y, 1), then U = y, and
    
  * for Ẋ∈σ,
    
        
  * if Ẋ is a constant symbol and ϑ(Ẋ) = (y, z), then ℐ(Ẋ) ∈ y ∩ U,
        
  * if Ẋ is an n-ary relation symbol and ϑ(Ẋ) = (y, 0), then ℐ(Ẋ) ⊂ y ∩ U^n,
        
  * if Ẋ is an n-ary relation symbol and ϑ(Ẋ) = (y, 1), then ℐ(Ẋ) = y ∩ U^n,
        
  * if Ẋ is an n-ary function symbol and ϑ(Ẋ) = (y, 0), then 
    {z ∈ U^n+1 : ℐ(Ẋ)(z _n) = z(n)}⊂ y ∩ U^n+1,  and

        
  * if Ẋ is an n-ary function symbol and ϑ(Ẋ) = (y, 1), then 
    {z ∈ U^n+1 : ℐ(Ẋ)(z _n) = z(n)} = y ∩ U^n+1.

    

We say (T, σ, 𝒰̇, ϑ) has a model if there exists ℳ for which ℳ^* (T, σ, 𝒰̇, ϑ).
  

We can define a notion of complexity on TCIs. This will help us subsequently classify method definitions according to their complexity. 


Let ϕ be a first-order formula over a signature σ. We inductively define what it means for ϕ to be Π_n or Σ_n as n ranges over the natural numbers.

    
  * If n = 0, then ϕ is Π_n iff ϕ is Σ_n iff ϕ is quantifier-free.
    
  *  If n = m + 1 for some m < ω, then 
    
        
  *  ϕ is Π_n iff there is a Σ_m formula φ, a number k < ω, and variable symbols x_1, …, x_k such that 
        
    ϕ = ⌜∀ x_1 …∀ x_k  φ⌝, and

        
  *  ϕ is Σ_n iff there is a Π_m formula φ, a number k < ω, and variable symbols x_1, …, x_k such that 
        
    ϕ = ⌜∀ x_1 …∀ x_k  φ⌝.

    

Note that if k = 0 in <ref><ref> and <ref><ref>, then ϕ is Σ_m and Π_m respectively.


[Lau, <cit.>]
A TCI (T, σ, 𝒰̇, ϑ) is Π_n iff T contains only Π_n sentences.

A TCI (T, σ, 𝒰̇, ϑ) is Σ_n iff T contains only Σ_n sentences.


As we shall see in Proposition <ref>, the existence of models of a TCI need not be absolute between between transitive models of 𝖹𝖥𝖢. There is thus a fundamental difference between model existence of TCIs and that of first-order theories. This should reflect in our definition of what it means for a TCI to be consistent.

[Lau, <cit.>]
A TCI (T, σ, 𝒰̇, ϑ) is consistent iff (T, σ, 𝒰̇, ϑ) has a model in some outer model of V. 


It might seem at first glance, that the the consistency of a TCI is not a first-order property in the language of set theory, since it involves quantifying over all outer models. This is not a real problem because said definition is semantically equivalent to a first-order sentence in V with parameters in V.


Let 𝔗 = (T, σ, 𝒰̇, ϑ) be a TCI. Then 𝔗 is consistent iff 
    ⊩_Col(ω, λ)∃ℳ (“ℳ^* 𝔗"),
 where λ≥ |H(|trcl(𝔗)|^+)|.



This is Lemma 5.25 of <cit.>.


Lemma <ref> gives us a uniform way of checking in V if a TCI is consistent, by appealing to a suitable forcing relation. For ease of expression and reading, we define the abbreviation

    𝔄_𝔗 := (H(|trcl(𝔗)|^+); ∈) .



It is easily verifiable from the definitions of ℒ_𝔗 and 𝔄_𝔗 that ℒ_𝔗∈𝔄_𝔗, so we have [ℒ_𝔗]^< ω∈𝔄_𝔗 as well.


Morally speaking, the consistency of a theory — however it is defined — should be absolute in a strong enough sense. This is the case for first-order theories, any of which consistency is absolute for transitive models of set theory. The following Lemma establishes a similar absoluteness property with regards to the consistency of a TCI.


Let 𝔗 = (T, σ, 𝒰̇, ϑ) be a TCI. Then 𝔗 being consistent is absolute for transitive models of 𝖹𝖥𝖢 sharing the same ordinals.



Let V' and W be transitive models of 𝖹𝖥𝖢 with ORD^V' = ORD^W and 𝔗∈ V' ⊂ W. If 𝔗 is consistent in W, then 𝔗 has a model in some outer model of W. Said outer model is also an outer model of V', so 𝔗 is consistent in V' as well.

Now assume 𝔗 is consistent in V'. Letting 

    λ := |H(|trcl(𝔗)|^+)|
 
evaluated in V', Lemma <ref> gives us 

    ⊩_Col(ω, λ)∃ℳ (“ℳ^* 𝔗")
 
in V'. Note that 

    ℙ := Col(ω, λ)^V'
 
remains a forcing notion in W, so consider g a ℙ-generic filter over W. Necessarily, g is also ℙ-generic over V', and further, V'[g] ⊂ W[g]. In V'[g], 𝔗 is forced to have a model — call it ℳ. Being a model of 𝔗 is absolute for transitive models of 𝖹𝖥𝖢, so ℳ^* 𝔗 holds in W[g] too. Since W[g] is an outer model of W, 𝔗 must be consistent in W.



A triple (𝔗, 𝔄, ℙ) is generically sensible iff 

    
  * 𝔗 is a TCI,
    
  * 𝔄 = (A; ∈, R) is a structure expanding on a transitive model of 𝖹𝖥𝖢 - 𝖯𝗈𝗐𝖾𝗋𝗌𝖾𝗍,
    
  * ℙ is a forcing notion, and
    
  * {𝔗, ℙ}⊂ A.



[Lau, <cit.>]
Given a generically sensible triple (𝔗, 𝔄, ℙ), a (ℙ, 𝔄)-generic model of 𝔗 is a model ℳ of 𝔗 satisfying 

    Σ(𝔗, ℳ) = (⋃ g) ∩ℒ_𝔗
 
for some ℙ-generic filter g over 𝔄. In this case, we say g witnesses ℳ is a (ℙ, 𝔄)-generic model of 𝔗. We say g witnesses a (ℙ, 𝔄)-generic model of 𝔗 iff for some (necessarily unique) ℳ, g witnesses ℳ is a (ℙ, 𝔄)-generic model of 𝔗.

We call ℳ a 𝔄-generic model of 𝔗 iff for some ℙ, (𝔗, 𝔄, ℙ) is generically sensible and ℳ is a (ℙ, 𝔄)-generic model of 𝔗.

We call ℳ a generic model of 𝔗 iff for some 𝔄 and ℙ, (𝔗, 𝔄, ℙ) is generically sensible and ℳ is a (ℙ, 𝔄)-generic model of 𝔗.   


[Lau, <cit.>]

    
  *  If g witnesses ℳ is a (ℙ, V)-generic model of 𝔗, and ⋃ g ⊂ℒ_𝔗, then V[g] = V[ℳ].
    
  *  In the same vein as Observation <ref>, we see that given any consistent Π_2 TCI 𝔗, 
    
    ∀ x  (     x  is a  (ℙ(𝔗), 𝔄_𝔗) -generic model of 𝔗
        x  is a  (ℙ(𝔗), V) -generic model of 𝔗)

   in every outer model of V. As a result, we can safely talk about (ℙ(𝔗), V)-generic models of 𝔗 without the need to quantify over all sets.



Our definition of a generic model is actually born from a nice characterisation of what we expect a generic model to be.


Let 𝔗 be a TCI. If ℳ is a model of 𝔗 in some forcing extension of V, then ℳ is a V-generic model of 𝔗.



This is Lemma 5.30 of <cit.>.




§ LOCAL METHOD DEFINITIONS


If we look at forcing as a way to uniformly describe by intension members of a subset of 𝐍(V) for some CTM V, where the evaluation of intension is done outside V, then we quickly realise that said description can be very simple. We essentially just 

    
  * shortlist a class of structures in V — forcing notions augmented with predicates for their dense subsets — and
    
  * describe how we pick substructures — generic filters — of these structures outside V. 
 
Note also that the description of each substructure 𝔄' involves only information about its associated superstructure 𝔄, so we expect every reasonable universe containing 𝔄 to see that 𝔄' fits the description. This is analogous to (albeit stronger than) the kind of local definablity one would expect the state transition function of a typical machine model of computation to satisfy.



 §.§ Locally Definable Methods of Small Extensions


This idea of generating new structures outside the universe based locally on recipes defined in the universe can be formalised rather conveniently using the language of TCIs. 


Let V be a CTM. A set X ⊂ V is a 𝐌_S(V) method definition of small extensions (henceforth, 𝐌_S(V) method definition) iff it is non-empty and contains only TCIs.



If V is a CTM and 𝔗∈ V is a TCI, then the evaluation of 𝔗, denoted Eval^V(𝔗), is the set

    {V[ℳ] : ∃ W  ∃ℳ (W ∈𝐌(V) ∧ℳ∈ W ∧ℳ^* 𝔗)}.




Let V be a CTM. A set X ⊂ V is a 𝐌_S(V) local method definition of small extensions (henceforth, 𝐌_S(V) local method definition) iff it is a 𝐌_S(V) method definition and X is definable (possibly as a proper class) in V with parameters in V. 


It might not be immediately obvious that whenever there are W and ℳ for which ℳ∈ W ∈𝐌(V) and ℳ^* 𝔗 for some TCI 𝔗∈ V, V[ℳ] must exist. The next proposition shows that one can translate between models of a TCI 𝔗 and subsets of a set associated with 𝔗, in an absolute and uniform manner.


There are formulas ϕ and ψ in the language of set theory with the following properties: 

    
  * ϕ and ψ have two and three free variables respectively,
    
  * ϕ defines a function from the class of all TCIs into the universe,
    
  * ψ defines a function from the class
    
    {(𝔗, ℳ) : 𝔗 is a TCI and ℳ^* 𝔗}

    into the universe,
    
  * ϕ and ψ are absolute for transitive models of 𝖹𝖥𝖢,
    
  *  whenever 𝔗 is a TCI, the relation
    
    R_𝔗 := {(ℳ, x) : ψ(𝔗, ℳ, x)}

    is one-one, 
    
  *  for all 𝔗, ℳ and x, ψ(𝔗, ℳ, x) implies there is ℒ for which ϕ(𝔗, ℒ) and x ⊂ℒ, and




Let 𝔗 be a TCI. Using only information about 𝔗, we will constructively define a set ℒ. Set 

    σ' :=     σ∪{𝒰̇}, and
    
        U :=     the unique  y  for which there exists  z  such that ϑ(𝒰̇) = (y, z).

For Ẋ∈σ', define ℒ(Ẋ) as follows:

    
  * if Ẋ is a constant symbol and ϑ(Ẋ) = (y, z), then 
    ℒ(Ẋ) := {⌜Ẋ = x ⌝ : x ∈ y ∩ U},

    
  * if Ẋ is an n-ary relation symbol and ϑ(Ẋ) = (y, z), then 
    ℒ(Ẋ) := {⌜Ẋ(x) ⌝ : x ∈ y ∩ U^n},  and

    
  * if Ẋ is an n-ary function symbol and ϑ(Ẋ) = (y, z), then 
    ℒ(Ẋ) := {⌜Ẋ(x _n) = x(n) ⌝ : x ∈ y ∩ U^n+1}.


Then 

    ℒ' :=     ⋃{ℒ(Ẋ) : Ẋ∈σ'}, and
    ℒ :=     the closure of ℒ'  under negation.

This construction is Δ_0-definable in the language of set theory with a single parameter, 𝔗, so it is absolute for transitive models of 𝖹𝖥𝖢. Use ϕ to denote this way of defining ℒ from 𝔗.

Next let ℳ = (M; ℐ) be a model of 𝔗. Set 

    U(ℳ) := {⌜𝒰̇(x) ⌝ : x ∈ M}∪{⌜ 𝒰̇(x) ⌝ : x ∈ U ∖ M}.
 
Now define ψ as follows: 

    ψ(𝔗, ℳ, Σ)  (   𝔗 is a TCI and ℳ^* 𝔗 and
       Σ = (U(ℳ) ∪ Diag(ℳ)) ∩ℒ_𝔗) ,
 
where Diag(ℳ) is the atomic diagram of ℳ and ℒ_𝔗 is the unique ℒ for which ϕ(𝔗, ℒ). Verily, ψ is a Δ_1 formula, because the binary relation ^* is Δ_1-definable and the set ℒ_𝔗 is Δ_1-definable with parameter 𝔗. As such, ψ must be absolute for transitive models of 𝖹𝖥𝖢. That <ref> holds is straightforward based on the definition of ψ. 


In the presence of Fact <ref>, Proposition <ref> gives validity to Definition <ref>: the function Eval^V taking TCIs in V to subsets of 𝐌_S(V) actually exists. Fix formulas ϕ and ψ as in Proposition <ref>. Let 

    ℒ_𝔗 :=      the unique ℒ for which ϕ(𝔗, ℒ) , and
    Σ(𝔗, ℳ) :=      the unique  x  for which ψ(𝔗, ℳ, x) .

Given a TCI 𝔗 = (T, σ, 𝒰̇, ϑ) and sets y, z with ϑ(𝒰̇) = (y, z), we should think of ℒ_𝔗 as containing all the possible atomic sentences over σ that involve members of y as parameters. Then for any model ℳ of 𝔗, Σ(𝔗, ℳ) (⊂ℒ_𝔗, by <ref> of Proposition <ref>) can be thought of as the “𝔗-specific atomic diagram”  of ℳ. According to <ref> of Proposition <ref>, we can always recover ℳ in a transitive model of 𝖹𝖥𝖢 from 𝔗 and Σ(𝔗, ℳ) alone. As a consequence, 

    V[ℳ] = V[x]  if  V  is a CTM and ψ(𝔗, ℳ, x)  for some TCI 𝔗∈ V .


Next, observe that we can “cover” the entire small outward multiverse with a local method definition.


Let V be a CTM. There is a 𝐌_S(V) local method definition X containing only Π_0 (= Σ_0) TCIs such that 

    ⋃ ((Eval^V)" X) = 𝐌_S(V) .




Fix a distinguished unary relation symbol 𝒰̇ and let s ∈ V. Define 

    ϑ_s := {(𝒰̇, (s, 0))}
    𝔗_s := (∅, ∅, 𝒰̇, ϑ_s) .

Then 𝔗_s is a Π_0 TCI, and its models in any outer model W of V are exactly the subsets of s in W. We are done by Fact <ref> if we set X := {𝔗_s : s ∈ V}.


We end off this subsection by demonstrating that forcing can be regarded as a local method definition.

Unless stated otherwise, we work within a fixed CTM V for the rest of this section, so that all mentions of 𝐌_S(V) in (local) method definitions can be conveniently suppressed.


Let ℙ = (P, ≤_ℙ) be a partial order. Then there is a TCI 𝔗(ℙ) = (T, σ, 𝒰̇, ϑ) such that for a fixed unary relation symbol Ẋ∈σ, if ℳ is any set in an outer model of V, then

    ℳ^* 𝔗(ℙ) {p : ℳẊ(p)} is a ℙ-generic filter over  V .




This is found in the proof of Theorem 5.34 of <cit.>, but we reproduce it the key portions here. 

Choose 𝒰̇, ≤̇ and Ġ and to be distinct relation symbols of arities 1, 2 and 1 respectively. For each dense subset D of ℙ, choose a fresh unary relation symbol Ḋ. Set σ to be 
    {≤̇, Ġ}∪{Ḋ : D  is a dense subset of ℙ}.
 We define ϑ on {𝒰̇}∪σ as follows:

    ϑ(𝒰̇) :=      (P, 1) 
    ϑ(≤̇) :=      (≤_ℙ, 1) 
    ϑ(Ġ) :=      (P, 0) 
    ϑ(Ḋ) :=      (D, 1)  for each dense subset  D  of ℙ.

Now, have T contain only the sentences

    ⌜∀ p  ∀ q  ∃ r  ((Ġ(p) ∧Ġ(q))  (Ġ(r) ∧≤̇(r, p) ∧≤̇(r, q))) ⌝,
    ⌜∀ p  ∀ q  ((≤̇(p, q) ∧Ġ(p)) Ġ(q)) ⌝, as well as all members of
    {⌜∃ p  (Ġ(p) ∧Ḋ(p)) ⌝ : D  is a dense subset of ℙ}.
 
Let 𝔗(ℙ) := (T, σ, 𝒰̇, ϑ). It is clear from our definition of 𝔗(ℙ) that whenever ℳ^* 𝔗(ℙ), the set {p : ℳẊ(p)} is a ℙ-generic filter over V, and vice versa.



Forcing is expressible as a local method definition.



The proof of Proposition <ref> is constructive, and can be made uniform across all possible ℙ by choosing the symbols 𝒰̇, ≤̇ and Ġ in advance. This allows the function 

    (F : {forcing notions}⟶ V) [ℙ↦𝔗(ℙ)]

to be definable in V. Obviously, dom(F) is definable in V, so ran(F) must be as well. 


Let us choose a definable function F as in the proof of Corollary <ref> and name it 𝔗(·), for later use and reference. Also, we shall use 𝖥𝗀 to denote the local method definition of forcing; in other words,  𝖥𝗀 := ran(𝔗(·)).



 §.§ Complexity of Local Method Definitions


What does it mean for a definition to be complex? Long, overwrought, convoluted. These are just some synonyms that may come to mind. in general, a more complex definition places more requirements on the object, or the class of objects, it defines. In the former scenario, it makes the object it defines a priori less likely to exist; in the latter one, it defines a compratively smaller class of objects. Following this intuition, we formalise a way of comparing between two local method definitions.


Let X, Y be local method definitions of a CTM V. We use 

    
  * X ≤^M_w Y to denote the statement
    
    “for each consistent 𝔗∈ X  there is 𝔗' ∈ Y  such that
    ∅≠Eval^V(𝔗') ⊂Eval^V(𝔗) ”,

    and
    
  * X ≤^M Y to denote the statement
    
    “   there is a function  F : X ⟶ Y  definable in  V  such that
       ∅≠Eval^V(F(𝔗)) ⊂Eval^V(𝔗)  for all consistent 𝔗∈ X ”.

    When said statement is true, we say F witnesses X ≤^M Y.




Let X, Y be local method definitions. We say

    
  * X ≡^M_w Y iff X ≤^M_w Y and Y ≤^M_w X,
    
  * X ≡^M Y iff X ≤^M Y and Y ≤^M X,
    
  * X <^M_w Y iff X ≤^M_w Y and Y ≰^M_w X, and
    
  * X <^M Y iff X ≤^M Y and Y ≰^M X.





    
  * ≤^M_w and ≤^M are transitive relations, so ≡^M_w and ≡^M are equivalence relations.
    
  * ≤^M_w and ≤^M, as subclasses of V, are only definable outside V, for their definitions require quantification over proper subclasses of V. 
    
  * Obviously, X ≤^M Y always implies X ≤^M_w Y, so ≤^M_w is weaker than ≤^M. 



Intuitively, Y is more complex than X as a definition when X ≤^M_w Y or X ≤^M Y, because Y both refines and extends X. Refinement occurs because no matter set a description of X picks out, Y contains a description that picks out a smaller non-empty set. Extension occurs because Y may have a description pick out a set that is not covered by any description of X. The difference between the two relations then boils down to whether a witness to said refinement and extension exists in V.

It would be good if V can decide (albeit not uniformly) whether X ≤^M Y for arbitrary local method definitions X and Y. Unfortunately, there seems to be no straightforward indication of that: it is not clear if V is always privy to proof of X ≤^M Y. For certain pairs (X, Y) though, X ≤^M Y is provable in 𝖹𝖥𝖢, and so V must know it is true.


Let X, Y be local method definitions. If X ⊂ Y, then X ≤^M Y.



The identity map on X is definable in V and witnesses X ≤^M Y.



There is a greatest local method definition with respect to ≤^M.



Let Y be the class of all TCIs. Clearly Y is a local method definition. Moreover, X ⊂ Y for every local method definition X. By Proposition <ref>, X ≤^M Y for every local method definition X.



A local method definition is not smallest with respect to ≤^M iff it contains a consistent TCI.



Clearly, every local method definition containing no consistent TCIs is smallest with respect to ≤^M. For the converse, by Proposition <ref>, it suffices to show that for every x ∈ V, there is a small extension of V not generated by a subset of x. But this is implied by the forcing notion Col(|x|^+, |x|^+)^V adding no subsets of x over V.


We now define a natural hierarchy on the class of TCIs.


For n < ω, we have the following local method definitions:

    Π^𝖬_𝗇 :=     {𝔗 : 𝔗 is a Π_n  TCI}
    Σ^𝖬_𝗇 :=     {𝔗 : 𝔗 is a Σ_n  TCI}.




Let n < ω. Then

    
  * Π^𝖬_𝗇≤^M Π^𝖬_𝗇+1,
    
  * Σ^𝖬_𝗇≤^M Σ^𝖬_𝗇+1,
    
  * Π^𝖬_𝗇≤^M Σ^𝖬_𝗇+1, and
    
  * Σ^𝖬_𝗇≤^M Π^𝖬_𝗇+1.




By Proposition <ref>.


By Proposition <ref>, 

    {Π^𝖬_𝗇 : n < ω}∪{Σ^𝖬_𝗇 : n < ω}

forms a hierarchy of local method definitions with ≤^M-predecessor sets that grow with n. We shall call this the local method hierarchy.

Mathematics and computer science are replete with hierarchies similar to the local method hierarchy, where syntactic forms of defining formulas are used to categorise sets. Examples include the projective, arithmetical and polynomial hierarchies. If we think of TCIs as augmentations of first-order theories with added constraints that are bounded but not first-order definable, then the local method hierarchy segregates TCIs based only on their first-order parts.

It turns out that most of the Π^𝖬_𝗇's are unnecessary in this hierarchy. 


Let n satisfy 1 ≤ n < ω. For every 𝔗∈Π^𝖬_𝗇+1 there are

    
  * 𝔗' ∈Σ^𝖬_𝗇, and
    
  * a formula θ with two free variables,

such that 

    
  * θ is absolute for outer models of V, and
    
  * in every outer model of V, θ defines a bijection from the set of models of 𝔗 into the set of models of 𝔗'.




Let 

    
  * 1 ≤ n < ω,
    
  * 𝔗  = (T, σ, 𝒰̇, ϑ) ∈Π^𝖬_𝗇+1, and 
    
  * ϑ(𝒰̇) = (y, z).
 
We shall first construct 𝔗' ∈Σ^𝖬_𝗇 from 𝔗. Expand the signature σ to σ' by adding 

    
  * a unary relation symbol Ṫ, as well as
    
  * a constant symbol ċ for each c ∈ y, 

all of which are new to σ and distinct from one another. Define ϑ' point-wise as follows:

    ϑ'(𝒰̇) := (y, 1) 
    ϑ'(Ẋ) := (y', 0)  whenever Ẋ∈σ and ϑ(Ẋ) = (y', z') 
    ϑ'(Ṫ) := (y, z) 
    ϑ'(ċ) := ({c}, 0)  for all  c ∈ y .


Next, initialise T^* to be 

    T    ∪{⌜∀ x_1 …∀ x_k  ∃ x_k+1 (Ḟ(x_1, …, x_k) = x_k+1) ⌝
       25mu : Ḟ∈σ is a  k -ary function symbol}.

For each Ẋ∈σ, so that ϑ(Ẋ) is of the form (y', z'), do the following.

    
  * Ẋ is a k-ary function symbol. Without loss of generality, we can assume y' ⊂ y^k+1. Add to T^* every member of the set
    
    {   ⌜Ẋ(ċ_1, …, ċ_k) = ċ_k+1Ṫ(ċ_1) ∧…∧Ṫ(ċ_k+1) ⌝
        : (c_1, …, c_k+1) ∈ y'}.

    If in addition, z' = 1, then also add to T^* every member of the set
    
    {   ⌜Ṫ(ċ_1) ∧…∧Ṫ(ċ_k+1) Ẋ(ċ_1, …, ċ_k) = ċ_k+1⌝
        : (c_1, …, c_k+1) ∈ y'}.

    
  * Ẋ is a k-ary relation symbol. Without loss of generality, we can assume y' ⊂ y^k. Add to T^* every member of the set
    
    {   ⌜Ẋ(ċ_1, …, ċ_k) Ṫ(ċ_1) ∧…∧Ṫ(ċ_k) ⌝
        : (c_1, …, c_k) ∈ y'}.

    If in addition, z' = 1, then also add to T^* every member of the set
    
    {   ⌜Ṫ(ċ_1) ∧…∧Ṫ(ċ_k) Ẋ(ċ_1, …, ċ_k) ⌝
        : (c_1, …, c_k) ∈ y'}.

    
  * Ẋ is a constant symbol. Without loss of generality, we can assume y' ⊂ y. Add to T^* the sentence
    
    ⌜Ṫ(Ẋ) ⌝.


Now T^*, like T, contains only Π_n+1 sentences.

Fix any formula ϕ∈ T^*. Then ϕ is of the form 

    ⌜∀ x_1 …∀ x_k  φ⌝,

where k < ω and φ is a Σ_n formula of which leading quantifier — should it exist — is not a universal quantifier. Note that such k and φ are unique for ϕ. If a∈^k{ċ : c ∈ y}, use ϕ_a to denote the result of running the following procedure on ϕ.

    
  * For each subformula ψ containing at least one quantifier, in descending order of length (which is necessarily linear due to ϕ being in prenex normal form), do as per the cases below.
    
        
  * ψ = ⌜∀ x  ψ' ⌝ for some x and ψ'. In this case, replace ψ' with the string
        
    ⌜ (Ṫ(x) ψ') ⌝.

        
  * ψ = ⌜∃ x  ψ' ⌝ for some x and ψ'. In this case, replace ψ' with the string
        
    ⌜ (Ṫ(x) ∧ψ') ⌝.

    
    
  * For each i such that 1 ≤ i ≤ k, remove all instances of the string ⌜∀ x_i ⌝.
    
  * Substitute a(i - 1) for every instance of x_i whenever 1 ≤ i ≤ k.

It is not hard to verify that the aforementioned procedure is well-defined and produces a Σ_n sentence over σ'. As a result, 

    T_ϕ := {ϕ_a : a∈^k{ċ : c ∈ y}}

is a set of Σ_n sentences over σ'. We set 

    T' := ⋃{T_ϕ : ϕ∈ T^*}.

so that 𝔗' := (T', σ', 𝒰̇, ϑ') ∈Σ^𝖬_𝗇. Then the following hold true in every outer model of V.

    
  *  Given any model ℳ of 𝔗',
    
    (Ṫ^ℳ; σ^ℳ)
 
    is a model of 𝔗. 
    
  *  Every model of 𝔗 can be uniquely and constructively extended and expanded to a model of 𝔗'.

It is clear that the transformations involved in <ref> and <ref> are absolute for outer models of V.


An important upshot of Lemma <ref> is the corollary below.


Π^𝖬_𝗇+1≤^M Σ^𝖬_𝗇 for all n satisfying 1 ≤ n < ω.


We are interested in how 𝖥𝗀 might fit into the local method hierarchy. To that end, let us first make a simple observation.


𝖥𝗀≤^M Σ^𝖬_1.



For all forcing notions ℙ, the TCI 𝔗(ℙ) is always a member of Π^𝖬_2 by the proof of Proposition <ref>. That 𝔗(·) is definable in V makes it a witness to 𝖥𝗀≤^M Π^𝖬_2. Lemma <ref> then implies 𝖥𝗀≤^M Σ^𝖬_1.



Let 𝔗∈ V be a consistent TCI and ℙ = (P, ≤_ℙ) be a forcing notion such that 

    
  *  ≤_ℙ =  ⊃∩ P,
    
  *  every member of P is a finite set, and
    
  *  ⊩_ℙ^V“⋃Ġ⊂ℒ_𝔗 and Ġ witnesses a (ℙ, V̇)-generic model of 𝔗”,  

where Ġ and V̇ are the canonical names for the generic filter on ℙ and for the ground model, respectively. Then ∅≠Eval^V(𝔗(ℙ)) ⊂Eval^V(𝔗).



First, Eval^V(𝔗(ℙ)) is exactly the set of all ℙ-generic extensions of V, so ∅≠Eval^V(𝔗(ℙ)). 

Let U ∈Eval^V(𝔗(ℙ)), so that U = V[g] for some ℙ-generic filter g over V. By <ref>, there is ℳ∈ U such that ℳ^* 𝔗, which implies V[ℳ] ⊂ U and V[ℳ] ∈Eval^V(𝔗). That 

    ⊩_ℙ^V “⋃Ġ⊂ℒ_𝔗”

means ⋃ g is definable from ℳ in any transitive model of 𝖹𝖥𝖢, so ⋃ g ∈ V[ℳ]. To show U ⊂ V[ℳ], it suffices to show g is recoverable from ⋃ g in V[ℳ] with the help of parameters in V. 

We claim g = [⋃ g]^< ω∩ P. Clearly g ⊂ [⋃ g]^< ω∩ P due to <ref>. Next assume p ∈ [⋃ g]^< ω∩ P. Then for each x ∈ p, there must be some q_x ∈ g containing x. As p is a finite set and g is a filter on ℙ, 

    S := {q_x : x ∈ p}

has a common extension, say q, in g. By <ref>, p ⊂⋃ S ⊂ q, so also p ∈ g. This proves our claim as well as the lemma.


Lemma <ref> provides a direction towards proving Σ^𝖬_1≤^M 𝖥𝗀: we can try to define a function F on Σ^𝖬_1 such that whenever 𝔗∈Σ^𝖬_1 is consistent, F(𝔗) = 𝔗(ℙ) for some forcing notion ℙ satisfying the hypothesis of Lemma <ref> in conjunction with 𝔗. 

Putting aside 𝖥𝗀 for a moment, let us consider the local method hierarchy in and of itself. Notice that we have neither proven nor disproven anything about the size of

    {Π^𝖬_𝗇 : n < ω}∪{Σ^𝖬_𝗇 : n < ω} modulo ≡^M ,

or equivalently, 

    {Π^𝖬_1}∪{Σ^𝖬_𝗇 : n < ω} modulo ≡^M ,

besides the obvious fact that it is countable and non-zero. Indeed, there seems to be no easy way of separating the rungs of the hierarchy as yet. This appears in stark contrast with the more renowned arithmetical and projective hierarchies, where separation happens “everywhere”. However, by no means is this a reason to dismiss (our definition of) the hierarchy, or discourage the study thereof. One need not look far to find a well-studied hierarchy of the same ilk with the same “issue”: the polynomial hierarchy, in which separation of any kind is equivalent to 𝖯≠𝖭𝖯. 



    
  * Are there m, n < ω for which Σ^𝖬_𝗆≢^M Σ^𝖬_𝗇?
    
  * Is it true that Π^𝖬_1≤^M Σ^𝖬_0?
    
  * Is there a TCI 𝔗 such that {𝔗}≰^M 𝖥𝗀?





§ CATEGORISING FORCING


In this section, we complete what we started in Subsection <ref>, and associate set forcing with a rung of the local method hierarchy. Additionally, we will study different witnesses to the fact that Π^𝖬_2≤^M 𝖥𝗀.



 §.§ Forcing is Σ-1 (is Π-2)


This subsection is dedicated to showing 𝖥𝗀≡^M Σ^𝖬_1. One direction of the proof is done in Proposition <ref>. For the other direction, we will identify a witness to Π^𝖬_2≤^M 𝖥𝗀. This witness can be defined without referencing any witness to Π^𝖬_2≤^M Σ^𝖬_1.


Let 𝔗∈ V be a TCI. Define 

    P(𝔗) := {p ∈ [ℒ_𝔗]^< ω : ∃ W ∈𝐌(V)  ∃ℳ (ℳ∈ W , ℳ^* 𝔗 and  p ⊂Σ(𝔗, ℳ))}



It may not be clear that P(𝔗) is a member of V for arbitrary 𝔗∈ V. We prove this in the next lemma.


Let 𝔗∈ V be a TCI. Define 

    P'(𝔗) := {p ∈ [ℒ_𝔗]^< ω :  ⊩^V_Col(w, |𝔄_𝔗|)∃ℳ (“ℳ^* 𝔗 and  p ⊂Σ(𝔗, ℳ) ”)}




Let 𝔗∈ V be a TCI. Then P(𝔗) = P'(𝔗), so there is a definition of P(𝔗) uniform over all TCIs 𝔗 in V.



Noting that |𝔄_𝔗| = |trcl(𝔄_𝔗)|, this is essentially the proof of Lemma 3.35 of <cit.> with different nomenclature.



For each TCI 𝔗∈ V, set 

    ℙ(𝔗) := (P(𝔗), ⊃∩ P(𝔗)) .




Now that ℙ(𝔗) has been defined for all TCIs 𝔗, it is clear from Lemma <ref> and Proposition <ref> that Question 5.70 of <cit.> can be answered in the affirmative. In other words, letting

    𝒞 := {𝔗 : 𝔗 is a Σ_1  TCI},

we can conclude the following:

    
  * 𝒞⊊{𝔗 : 𝔗 is a Π_2  TCI}, and
    
  * for each forcing notion ℙ, there is 𝔗∈𝒞 for which
    
        
  * ℙ and ℙ(𝔗) are forcing equivalent, and
        
  * 
        [t]
               {V[ℳ] : ℳ^* 𝔗 in an outer model of  V}
   70mu = {V[g] : g  is ℙ-generic over  V},
    
    so that also
    
    {V[ℳ] : ℳ^* 𝔗 in an outer model of  V}
        = {V[g] : g  is ℙ(𝔗) -generic over  V}.

 


The definable function 𝔗↦𝔗(ℙ(𝔗)), restricted to Π^𝖬_2, will be our witness to Π^𝖬_2≤^M 𝖥𝗀. A trivial observation is that <ref> and <ref> of Proposition <ref> hold for ℙ(𝔗) and P(𝔗) in place of ℙ and P respectively. Furthermore, it is always true that

    ⊩_ℙ(𝔗)⋃Ġ⊂ℒ_𝔗,

so we are left to prove

    ⊩_ℙ(𝔗)“Ġ witnesses a  (ℙ(𝔗), V̇) -generic model of 𝔗”

for every consistent Π_2 TCI 𝔗. In <cit.> this is done by appealing to the more general framework of forcing with language fragments. Fix a consistent Π_2 TCI 𝔗. Let us hereby briefly outline the proof of (<ref>).

In the aforementioned forcing framework, we allow potentially any set to be interpreted as a language, by extending the negation operator from classical first order logic to all sets. In other words, we define a canonical negation function  on V as follows: 

    x := (x) = 
        
            y    if  x = ⌜ y ⌝ for some  y 
    ⌜ x ⌝   otherwise.

A set ℒ is closed under negation iff for each ϕ∈ℒ, ϕ∈ℒ. The aim of the framework is to study certain definable subsets of a set closed under negation from the perspective of a larger structure. 

A structure 𝔄 is ℒ-suitable iff it expands on a model of a sufficiently strong set theory (𝖹𝖥𝖢 - 𝖯𝗈𝗐𝖾𝗋𝗌𝖾𝗍 is more than enough) and ℒ is a definable class in 𝔄. We define the language ℒ^*_𝔄 by enlarging the signature of 𝔄 with members of its base sets as constants and a fresh unary relation symbol ⌜ E ⌝. Morally, ⌜ E ⌝ is to be interpreted as a subset of ℒ when 𝔄 is ℒ-suitable. ℒ^*_𝔄 thus enables us to impose first-order requirements on subsets of ℒ. 

We say “Σ Γ(ℒ, 𝔄)-certifies p” iff 

    
  * ℒ is closed under negation and 𝔄 is ℒ-suitable,
    
  * 𝔄, augmented with the predicate Σ that interprets ⌜ E ⌝, satisfies the theory Γ⊂ℒ^*_𝔄, and
    
  * p ⊂Σ.

Syntactically, it makes sense to talk about Π_n and Σ_n formulas and sentences in ℒ^*_𝔄, although these classes are defined a little differently from their counterparts in a typical set-theoretic context. Such a syntactic classification turns out to have interesting implications on forcing constructions.

There are a few lemmas, in varying degrees of generality, that connect genericity to relations akin to “Γ(ℒ, 𝔄)-certification”. The following is the most relevant to our intended use case.


Let W, λ, 𝔄, ℒ, Γ, P, ℙ and g be such that

    
  * Γ contains only Π_2 ℒ^*_𝔄 sentences,
    
  * |trcl(𝔄)| ≤λ,
    
  * P = {p ∈ [ℒ]^< ω :  ⊩_Col(ω, λ)∃Σ (“Σ Γ(ℒ, 𝔄) -certifies  p")}≠∅,
    
  * ℙ = (P, ⊃∩ P), 
    
  * ℙ is a definable class in 𝔄,
    
  * W is an outer model of V, and
    
  * g ∈ W is a ℙ-generic filter over 𝔄.

Then ⋃ g Γ(ℒ, 𝔄)-certifies ∅.

In particular, if g is ℙ-generic over V, then ⋃ g Γ(ℒ, 𝔄)-certifies ∅ in V[g] = V[⋃ g].



This is (implied by) Lemma 3.39 of <cit.>.


The next lemma allows us to transform an arbitrary Π_2 TCIs into a form amenable with our forcing framework, so that Lemma <ref> can be applied.


For each Π_2 TCI 𝔗 there is Γ_𝔗 such that

    
  *  Γ_𝔗 contains only Π_2 (ℒ_𝔗)^*_𝔄_𝔗 sentences, and
    
  *  for every set x,
    
    ∃ℳ (ℳ^* 𝔗 and Σ(𝔗, ℳ) = x)  x  Γ_𝔗 (ℒ_𝔗, 𝔄_𝔗)-certifies ∅.





This is implied by Lemmas 5.17 and 5.22 of <cit.> (cf. Proposition <ref>).


We can now derive (<ref>) from Lemmas <ref> and <ref>. 


Let 𝔗 = (T, σ, 𝒰̇, ϑ) be a consistent Π_2 TCI. Then every ℙ(𝔗)-generic filter over V witnesses a (ℙ(𝔗), V)-generic model of 𝔗, or equivalently, (<ref>) holds.



We first apply Lemma <ref> to obtain a Γ_𝔗 such that

    
  *  Γ_𝔗 contains only Π_2 (ℒ_𝔗)^*_𝔄_𝔗 sentences, and
    
  * for every set x,
    
    ∃ℳ (ℳ^* 𝔗 and Σ(𝔗, ℳ) = x)  x  Γ_𝔗 (ℒ_𝔗, 𝔄_𝔗)-certifies ∅.


Next, note that

    
    
  * Observation <ref> holds,
    
  * |𝔄_𝔗| = |trcl(𝔄_𝔗)|, and
    
  *  for all x and p,
    
    x  Γ_𝔗 (ℒ_𝔗, 𝔄_𝔗)-certifies  p  (x  Γ_𝔗 (ℒ_𝔗, 𝔄_𝔗)-certifies ∅ and  p ⊂ x) .


Let g be a ℙ(𝔗)-generic filter over V. Then the theorem follows directly from Lemma <ref>, as the hypotheses of said lemma are satisfied with

    
  * V[g] in place of W,
    
  * |𝔄_𝔗| in place of λ,
    
  * 𝔄_𝔗 in place of 𝔄,
    
  * ℒ_𝔗 in place of ℒ,
    
  * Γ_𝔗 in place of Γ,
    
  * P(𝔗) in place of P, and
    
  * ℙ(𝔗) in place of ℙ,

bearing in mind <ref> to <ref>.


It should be emphasised that the proof of Lemma <ref> provides a uniform way of constructing Γ_𝔗 from any TCI 𝔗, such that <ref> of the lemma is satisfied. If in addition, 𝔗 is Π_2, then the Γ_𝔗 constructed also satisfies <ref> of Lemma <ref>. We shall hereby have Γ_𝔗 denote the result of the aforementioned construction with 𝔗 as its starting point.

As a corollary, we observe a rather strong failure of the converse of Proposition <ref>.


There are local definitions X and Y such that X <^M Y and 

    ⋃ ((Eval^V)" Y)  ⊊⋃ ((Eval^V)" X) .




Let 𝖲𝗍 := {𝔗_s : s ∈ V} be as in Proposition <ref>. By (<ref>), 

    ⋃ ((Eval^V)" 𝖥𝗀)  ⊊⋃ ((Eval^V)" 𝖲𝗍) .

Since 𝖲𝗍⊂Π^𝖬_0, by Proposition <ref> and Theorem <ref>, 𝖲𝗍≤^M 𝖥𝗀. We are left to show 𝖥𝗀≰^M 𝖲𝗍. 

Choose any forcing notion ℙ satisfying V ∉Eval^V(𝔗(ℙ)). If s is finite, then Eval^V(𝔗_s) = {V}⊄Eval^V(𝔗(ℙ)). Now assume s is infinite, and let f be a bijection from |s| into s. Apply an argument similar to that through which (<ref>) was justified, to obtain some r ⊂ω such that L^V[r] is an outer model of V, but no outer model of L^V[r] is a forcing extension of V. Then V[f" r] ∈Eval^V(𝔗_s) is an outer model of L^V[r], so Eval^V(𝔗_s) ⊄Eval^V(𝔗(ℙ)). We have thus proved that 𝖥𝗀≰^M_w 𝖲𝗍, and this completes the proof.


The proof of Corollary <ref> intimates that for TCIs with very simple theories, we can always construct a non-generic model. We cannot do the same for all Π_2 TCIs because of Proposition <ref>. Together, they make us wonder if a clear line can be drawn in V. Let 

    NG := {𝔗∈ V :     𝔗 is a Π_2  TCI and
       ∃ W  ∃ℳ∈ W  ∀ x ∈ W  (W  is an outer model of  V  and
       ℳ^* 𝔗 and  x ≇ℳ whenever  x  is a  V -generic model of 𝔗)}.


[Lau, <cit.>]
Is NG definable in V?




 §.§ A Strengthening


In this subsection, we build on Theorem <ref> to achieve a strengthening of the statement “Π^𝖬_2≤^M 𝖥𝗀”. This stronger statement appears in the form of Theorem <ref>. To start, let us recall some definitions and facts from order theory.


Let ℙ = (P, ≤_ℙ) be a forcing notion. A set Q is an upward closed subset of ℙ iff Q ⊂ P and for all p, q ∈ P, 

    (q ∈ Q  and  q ≤_ℙ p)  p ∈ Q .




If ℙ = (P, ≤_ℙ) is a forcing notion and p ∈ P, we let g_p (ℙ) denote the set 
    {q ∈ P : p _ℙ q}.




Let ℙ = (P, ≤_ℙ) be a forcing notion. A member p of P is an atom of ℙ iff 
    ∀ q_1  ∀ q_2  ((q_1 ≤_ℙ p  and  q_2 ≤_ℙ p)  q_1 _ℙ q_2).




If ℙ = (P, ≤_ℙ) is a forcing notion and p is an atom of ℙ, then g_p (ℙ) is a ℙ-generic filter over V.



If D is dense in ℙ, then there is q ∈ D with q ≤_ℙ p. Obviously, q ∈ g_p (ℙ). Therefore g_p (ℙ) is a ℙ-generic subset over V. To see that g_p (ℙ) is a filter, let q_1 and q_2 be members of g_p (ℙ). By the definition of g_p (ℙ), there are r_1 and r_2 such that 

    
  * r_1 ≤_ℙ q_1, 
    
  * r_1 ≤_ℙ p,
    
  * r_2 ≤_ℙ q_2,
    
  * r_2 ≤_ℙ p.

As p is an atom of ℙ, it must be the case that r_1 _ℙ r_2, which means q_1 _ℙ q_2.



A forcing notion ℙ = (P, ≤_ℙ) is atomless iff no member of P is an atom of ℙ.


A non-empty atomless forcing notion gives rise to many forcing extensions.


Let V be a CTM such that

    V “ℙ = (P. ≤_ℙ)  is a non-empty atomless forcing notion”.

Then |Eval^V(𝔗(ℙ))| = 2^ℵ_0.



As all members of Eval^V(𝔗(ℙ)) are countable, each one of them contains only countably many ℙ-generic filters over V. By Proposition <ref>, we just need to show there are 2^ℵ_0 many ℙ-generic filters over V. 

The idea is to construct a Cantor scheme differentiating the generic filters in question. Outside V, there are countably many dense subsets of ℙ, so let {D_n : n < ω} enumerate them. Define members of the set {p_s : s ∈ 2^< ω} such that

    
  *  p_∅∈ P,
    
  * p_s ∈ D_n if |s| = n + 1,
    
  * p_s_0≤_ℙ p_s_1 if s_1 ⊂ s_0, and
    
  *  p_s_0 _ℙ p_s_1 if s_1 ⊄s_0 and s_0 ⊄s_1.

This can be done by induction on the length of s. Choose any condition of ℙ to be p_∅. Assume next that p_s has been defined. Since p_s is not an atom of ℙ, we can find q_0 and q_1 extending p_s in ℙ such that q_0  _ℙ q_1. The density of D_|s| guarantees there are q'_0, q'_1 ∈ D_|s| extending q_0 and q_1 in ℙ, respectively. Set

    p_s^⌢⟨ 0 ⟩ := q'_0 
    
        p_s^⌢⟨ 1 ⟩ := q'_1 .

It is not hard to verify <ref> to <ref> hold for the p_ss defined as such.

Given r ∈ 2^ω, use g_r to denote the set

    {q ∈ P : ∃ n < ω (p_r  n≤_ℙ q)}.

Now g_r is a ℙ-generic filter over V whenever r ∈ 2^ω. If r_0, r_1 ∈ 2^ω and r_0 ≠ r_1, then r_0  n ≠ r_1  n for some n < ω. By <ref> we have p_r_0  n _ℙ p_r_1  n, so g_r_0≠ g_r_1. We are done because obviously, |2^ω| = 2^ℵ_0.


Models of a TCI 𝔗 across all outer models of V can be very complicated. However, there are certain models of which atomic diagrams can be easily read off ℙ(𝔗).

[Lau, <cit.>]
Given a TCI 𝔗 and any ℳ, we say ℳ is a finitely determined model of 𝔗 iff ℳ^* 𝔗 and for some quantifier-free sentence φ with parameters in ℳ, 

    ∀ W  ∀ℳ'  (   (W  is an outer model of  V  and ℳ' ∈ W  and ℳ' ^* 𝔗 and ℳ' φ) 
       ℳ' = ℳ).

In this case, ℳ is finitely determined by φ.


Naturally, all finite models of any TCI are finitely determined. As it turns out, if a TCI is consistent, then all its finitely determined models are already in V


Let 𝔗 be a TCI and ℳ be a finitely determined model of 𝔗 in some outer model of V. Then for some atom p of ℙ(𝔗), Σ(𝔗, ℳ) = g_p (ℙ(𝔗)). In particular, ℳ∈ V.



Let ℳ be finitely determined by φ. Without loss of generality, we can assume φ is the conjunction of a set of literals {l_i : i < n} for some n < ω. This means 
    p := {⌜ E(l_i) ⌝ : i < n}
 is an atom of ℙ(𝔗). Proposition <ref> tells us that g_p (ℙ(𝔗)) is ℙ(𝔗)-generic over V, so necessarily Σ(𝔗, ℳ) = g_p (ℙ(𝔗)) by Theorem <ref>. Then according to Proposition <ref>, ℳ∈ V because g_p (ℙ(𝔗)) ∈ V.


It is possible to have an analogue of Lemma <ref> for models that are “close to being finitely determined”.

[Lau, <cit.>]
Let 𝔗 be a TCI. Inductively define Γ_𝔗^(α), P(𝔗)^(α) and ℙ(𝔗)^(α) for all ordinals α≤ |[ℒ_𝔗]^< ω|^+ as follows:

    Γ_𝔗^(0) :=     Γ_𝔗,
    
        P(𝔗)^(0) :=      P(𝔗) ,
    Γ_𝔗^(α) :=     Γ_𝔗^(α - 1)∪{⌜⋁_x ∈ p ( E(x)) ⌝ : p  is an atom of ℙ(𝔗)^(α - 1)}
       if α is a successor ordinal,
    Γ_𝔗^(α) :=     ⋃_β < αΓ_𝔗^(β)
       if α is a limit ordinal,
    
        P(𝔗)^(α) :=     {p ∈ [ℒ_𝔗]^< ω :  ⊩_Col(ω, |trcl(𝔄_𝔗)|)∃Σ (“Σ Γ_𝔗^(α) (ℒ_𝔗, 𝔄_𝔗)-certifies  p")},
    ℙ(𝔗)^(α) :=      (P(𝔗)^(α), ≤_ℙ(𝔗)) .



By a simple cardinality argument, there must exist some α < |[ℒ_𝔗]^< ω|^+ for which Γ_𝔗^(α) = Γ_𝔗^(α + 1), whence ℙ(𝔗)^(α) = ℙ(𝔗)^(α + 1).

[Lau, <cit.>]
Let Γ_𝔗^⊤ denote the unique Γ such that Γ = Γ_𝔗^(α) = Γ_𝔗^(α + 1) for some α < |[ℒ_𝔗]^< ω|^+. Similarly, ℙ(𝔗)^⊤ = (P(𝔗)^⊤, ≤_ℙ(𝔗)^⊤) shall denote the unique ℙ such that ℙ = ℙ(𝔗)^(α) = ℙ(𝔗)^(α + 1) for some α < |[ℒ_𝔗]^< ω|^+.


It is not hard to see that P(𝔗)^⊤ is an atomless upward closed subset of ℙ(𝔗) and Γ_𝔗⊂Γ_𝔗^⊤.


In constructing the ℙ(𝔗)^(α)'s, we are inductively removing atoms of ℙ(𝔗). These atoms correspond to isolated points in a Stone-type space generated by models of a TCI. By looking at Definition <ref> in this way, we can draw obvious parallels between ℙ(𝔗)^(α) and the α-th-order Cantor-Bendixson derivative of a set. Such parallels culminate in ℙ(𝔗)^⊤ being analogous to the “perfect core” of ℙ(𝔗).


[Lau, <cit.>]
Given a TCI 𝔗 and any ℳ, we say ℳ is an almost finitely determined model of 𝔗 iff ℳ^* 𝔗 and for some α < |[ℒ_𝔗]^< ω|^+ and an atom p of ℙ(𝔗)^(α), 
    p ⊂Σ(𝔗, ℳ).



We have as our next lemma, the promised analogue of Lemma <ref>.


Let 𝔗 be a TCI and ℳ be an almost finitely determined model of 𝔗 in some outer model of V. Then for some α < |[ℒ_𝔗]^< ω|^+ and some atom p of ℙ(𝔗)^(α), Σ(𝔗, ℳ) = g_p (ℙ(𝔗)^(α)). In particular, ℳ∈ V.



Choose any model ℳ of 𝔗 in an outer model of V. It suffices to prove by induction on α≤ |[ℒ_𝔗]^< ω|^+ that

    ∀ q  ∃β≤α ∃ p  (     (q  is an atom of ℙ(𝔗)^(α) and  q ⊂Σ(𝔗, ℳ)) 
        (p  is an atom of ℙ(𝔗)^(β) and Σ(𝔗, ℳ) = g_p (ℙ(𝔗)^(β)))) .

The base case where α = 0 is just Lemma <ref>. For the inductive case, assume 0 < α≤ |[ℒ_𝔗]^< ω|^+. and let q be an atom of ℙ(𝔗)^(α) with q ⊂Σ(𝔗, ℳ). Then by Lemma <ref> and the definition of ℙ(𝔗)^(α), either Σ(𝔗, ℳ) = g_q (ℙ(𝔗)^(α)) or there is β' < α and an atom q' of ℙ(𝔗)^(β') such that q' ⊂Σ(𝔗, ℳ). In the latter case, the inductive hypothesis gives us β≤β' and an atom p of ℙ(𝔗)^(β) for which Σ(𝔗, ℳ) = g_p (ℙ(𝔗)^(β)). Either way we are done.


The way ℙ(𝔗) and ℙ(𝔗)^⊤ are defined from a TCI 𝔗 allows us to establish a nice dichotomy on the (ℙ(𝔗), V)-generic models of 𝔗 when 𝔗 is Π_2.


Let 𝔗 be a Π_2 TCI and ℳ be a (ℙ(𝔗), V)-generic model of 𝔗. Then one of the following must hold:

    
  * ℳ is almost finitely determined.
    
  * ℳ is a (ℙ(𝔗)^⊤, V)-generic model of 𝔗.




Let g be a ℙ(𝔗)-generic filter over V and assume 𝒜∩ g = ∅, where 
    𝒜 := {p : ∃α (α < |[ℒ_𝔗]^< ω|^+  and  p  is an atom of ℙ(𝔗)^(α))}.
 This latter assumption is equivalent to saying that the unique model ℳ of 𝔗 for which ⋃ g = Σ(𝔗, ℳ) is not almost finitely determined. By Theorem <ref>, it suffices to show that g is a ℙ(𝔗)^⊤-generic filter over V. Clearly, ⋃ g Γ_𝔗^⊤ (ℒ_𝔗, 𝔄_𝔗)-certifies p, so g ⊂ℙ(𝔗)^⊤. That ℙ(𝔗)^⊤ is a suborder of ℙ(𝔗) means g is a filter on ℙ(𝔗)^⊤.

To see g is ℙ(𝔗)^⊤-generic over V, let E be predense in ℙ(𝔗)^⊤. Note that if p ∈ℙ(𝔗) is incompatible in ℙ(𝔗) with every member of 𝒜, then p ∈ℙ(𝔗)^⊤. As such, E ∪𝒜 must be predense in ℙ(𝔗). But this implies E ∩ g ≠∅ because g is ℙ(𝔗)-generic and 𝒜∩ g = ∅.


The following is a stronger version of Theorem <ref>.


Let 𝔗 be a Π_2 TCI. Then one of the following must hold.

    
  * All models of 𝔗 are almost finitely determined.
    
  * ℙ(𝔗)^⊤ is non-empty and every ℙ(𝔗)^⊤-generic filter over 𝔄_𝔗 witnesses ℳ is a (ℙ(𝔗)^⊤, 𝔄_𝔗)-generic model of 𝔗 for some ℳ.




Assume not all models of 𝔗 are almost finitely determined, and let ℳ be a model of 𝔗 not almost finitely determined in some outer model of V. Then Σ(𝔗, ℳ) Γ_𝔗^⊤ (ℒ_𝔗, 𝔄_𝔗)-certifies ∅, so ℙ(𝔗)^⊤ is non-empty.

Let g be a ℙ(𝔗)^⊤-generic filter over V. Check that the hypotheses of Lemma <ref> are satisfied when we have 

    
  * V[g] in place of W,
    
  * |𝔄_𝔗| in place of λ,
    
  * 𝔄_𝔗 in place of 𝔄,
    
  * ℒ_𝔗 in place of ℒ,
    
  * Γ_𝔗^⊤ in place of Γ,
    
  * P(𝔗)^⊤ in place of P, and
    
  * ℙ(𝔗)^⊤ in place of ℙ,

A direct application of said lemma, coupled with Lemma <ref> and the knowledge that Γ_𝔗⊂Γ_𝔗^⊤, completes the proof. 


The strengthening we were aiming for can now be proven.


Fix 𝔗^* ∈𝖥𝗀. Then there is F_𝔗^* witnessing Π^𝖬_2≤^M 𝖥𝗀 such that

    
  * F_𝔗^*(𝔗) = 𝔗^* if 𝔗 is inconsistent,
    
  * F_𝔗^*(𝔗) = 𝔗((∅, ∅)) if 𝔗 is consistent and all models of 𝔗 are almost finitely determined, and
    
  * F_𝔗^*(𝔗) = 𝔗(ℙ) for some non-empty atomless forcing notion ℙ if 𝔗 is consistent and not all models of 𝔗 are almost finitely determined.




Define F_𝔗^* point-wise as follows:

    F_𝔗^*(𝔗) :=  
        𝔗^*    if 𝔗 is inconsistent
    𝔗(ℙ(𝔗)^⊤)    otherwise,

noting Lemma <ref>, Theorem <ref> and the fact that ℙ(𝔗)^⊤ = (∅, ∅) if all models of 𝔗 are almost finitely determined.


Notice that any F_𝔗^* satisfying Theorem <ref> must also satisfy

    |Eval^V(𝔗)| = |Eval^V(F_𝔗^*(𝔗))|

for all 𝔗∈ dom(F_𝔗^*). As a corollary, we get a trichotomy for the number of small extensions a Π_2 TCI can pick out.


Let V be a CTM and 𝔗∈ V be a Π_2 TCI. Then

    
  *  Eval^V(𝔗) = ∅ if 𝔗 is inconsistent,
    
  *  Eval^V(𝔗) = {V} if 𝔗 is consistent and all models of 𝔗 are almost finitely determined, and
    
  *  |Eval^V(𝔗)| = 2^ℵ_0 if 𝔗 is consistent and not all models of 𝔗 are almost finitely determined.




<ref> follows from the definition of Eval^V and what it means for a TCI to be (in)consistent. <ref> follows from Lemma <ref> and <ref> from Proposition <ref> and Theorem <ref>.




§ REFERENCES

[heading=none]

