# Forcing for Arbitrary First Order Theories

Forcing is a relative model construction method for models of $ZF$ as a particular first order theory using models of another first order theory (forcing companion) that in this case is the theory of partial orders ($PO$).

Is it possible to develope forcing for other first order theories? In fact I am asking for possible relative model constructions of a first order theory without finite models like $T$ (instead of $ZF$) using models of a "forcing companion" theory like $S$ (instead of $PO$). This model construction method produces countable models of $T$ with special properties using a given model of $T$ and a given model of $S$.

Obviously if we define a uniform "forcing companion theory" $S$ for an arbitrary first order theory $T$ then in many cases when countable models of $T$ are not too board up to isomorphism the "forcing theory of $T$" is just a trivial method and produces no interesting models of $T$. But in this question my focus is on first order theories with wild countable and countable models like $ZF$ and $PA$.

Every references in this frame work is welcome.

-
For starters, see Abraham Robinson, “Forcing in model theory”. –  Emil Jeřábek Feb 14 at 22:10
And also Feferman's Some applications of the notions of forcing and generic sets [Fund. Math. 56. (1964), 325–345]. –  François G. Dorais Feb 15 at 0:09
Searching in MO I found this related post. –  user45939 Feb 15 at 0:28
see also "Forcing in a general setting" by Bowen. Abstract: The author gives a logic-free treatment of some of the basics of forcing in a topological setting. The general scheme is shown to specialize to virtually all known varieties of forcing (set-theoretic, Robinson model-theoretic, etc.). –  Mohammad Golshani Feb 16 at 5:01

One of the most robust ways to understand forcing is via the method of Boolean ultrapowers, and this is a purely model-theoretic construction that makes sense to undertake with any first-order theory whatsoever. One may form the Boolean ultrapower of any graph, group, ring, field, partial order, and indeed of any structure in any first-order language whatsoever.

The general construction of the Boolean ultrapower has classical roots (due in set theory Vopenka, developed also by Solovay, Scott and others including a very nice presentation by Bell, but also as a purely model-theoretic construction by Mansfield and others), and a general introductory account can be found in my paper Well-founded Boolean ultrapowers as large cardinal embeddings, written jointly with Dan Seabold.

One may consider the general class of $\mathbb{B}$-valued models in a given first-order language. Specifically, a $\mathbb{B}$-valued structure in a first-order language (not necessarily set-theoretic) consists of a set of objects $M$, called names, and an assignment $[\![\tau=\sigma]\!]\in\mathbb{B}$ giving the Boolean value that any two names are equal, as well as the Boolean value $[\![R(\vec \sigma)]\!]\in\mathbb{B}$ that a given relation holds at a tuple of names, such that the laws of equality hold with respect to these assignments (and one can also handle function symbols and constants). The basic fact is that the concept of a Boolean-valued model is not particularly connected with set theory, and makes sense for models in any first-order language.

For any such $\mathbb{B}$-valued structure, whether it is group, ring, field, partial order or model of set theory, one may collapse it to a classial structure by taking the quotient by an arbitrary ultrafilter on $\mathbb{B}$. Specifically, if $U\subset\mathbb{B}$ is an ultrafilter (no need for any genericity), then one defines $\sigma=_U\tau$ for names just in case $[\![\sigma=\tau]\!]\in U$. This is an equivalence relation, indeed a congruence, and one defines the structure on the resulting quotient structure $R([\sigma]_U)$ just in case $[\![R(\sigma)]\!]\in U$, which is well-defined because the equality axioms had Boolean value one. In this way, any $\mathbb{B}$-valued structure is transformed into a classical $2$-valued structure by the quotient.

Thus, we have a generalization of the classical ultrapower construction from ultrapowers on a power set algebra to arbitrary ultrapowers on a complete Boolean algebra, and this is known as the Boolean ultrapower. Specifically, if you have a first-order structure $\cal M=\langle M,\ldots\rangle$ and a complete Boolean algebra $\mathbb{B}$, then consider the set of spanning functions $f:D\to M$, where $D$ is any open dense set in $\mathbb{B}$. Define $[\![R(f)]\!]=\bigvee\{b\in\mathbb{B}\mid R(f(b))\}$, and this produces a Boolean-valued model. If $U\subset\mathbb{B}$ is an ultrafilter in $\mathbb{B}$, define $f=_Ug$ for two spanning functions $f:D\to M$, $g:E\to m$, if $\bigvee\{b\in\mathbb{B}\mid f(b)=g(b)\}\in U$, and let ${\cal M}^{\downarrow\mathbb{B}}/U$. This is an equivalence relation, and we may consider the set of spanning functions modulo this relation, denoted $M^{\downarrow\mathbb{B}}/U$. For any relation $R$ in the language, we define the interpretation of $R$ on this structure by $R([f]_U)$ holds if and only if $\bigvee\{b\mid {\cal M}\models R(f(b))\}\in U$. One may similarly handle constants and functions as explained in the paper. If $U\subset\mathbb{B}$ is an ultrafilter, then the corresponding Boolean ultrapower map is the map $x\mapsto[c_x]_U$, where $c_x$ is the constant map on $\mathbb{B}$ with value $x$. This is a generalization of the ordinary ultrapower construction from ultrafilters on power set algebras to ultafilters on arbitrary complete Boolean algebras.

The connection with forcing is that for any complete Boolean algebra $\mathbb{B}$, we may construct the $\mathbb{B}$-valued model $V^{\mathbb{B}}$, whose objects are the $\mathbb{B}$-names with Boolean-valued truth defined in the usual forcing manner. If $U\subset\mathbb{B}$ is any ultrafilter (not necessarily generic in any sense), then one gets an elementary embedding $j:V\to \check V_U\subset \check V_U[[\dot G]_U]\cong V^{\mathbb{B}}/U$, which is precisely the Boolean ultrapower map of $V$ into the ground model of the Boolean extension $V^{\mathbb{B}}/U$ quotiented by the ultrafilter $U$.

-
One should think of the Boolean ultrapower construction as a generalization of the ultrapower construction, which might be thought of as an averaging method, a method of producing homogeneous non-special models, rather than special models. –  Joel David Hamkins Feb 15 at 0:42
The idea of interpreting forcing in Boolean valued version in order to generalize it to an arbitrary first order theory is very interesting. Did you construct any special model of a first order theory using this method before? By "special" I mean something like a special group, graph, field, etc. For example can we think about producing counterexamples using this kind of forcing for essential problems like finding a field which refutes Zilber's tricotomy conjecture in a different way from Hrushovski construction, etc? –  user45939 Feb 15 at 0:42
Oh! I think I used the word "special" in an inappropriate way here. I didn't mean special models in the model theoretic sense. I meant a model with a special property as same as set theory that we use forcing to produce models of ZF with special properties. –  user45939 Feb 15 at 0:47
Thus we can interpret set theoretic forcing as a kind of ultraproduct. So the case seems a bit strange because using large cardinal assumptions one can form another form of ultraproducts of the universe too. Is there any direct relevance between Boolean valued forcing ultraproducts and large cardinal ultraproducts of the universe here? –  user45939 Feb 15 at 0:58
Well, that is exactly what my paper with Dan Seabold is about: Well-founded Boolean ultrapowers as large cardinal embeddings jdh.hamkins.org/boolean-ultrapowers. –  Joel David Hamkins Feb 15 at 1:10

Adrian Mathias has been working on forcing over models of a weak fragment of set theory, of which he says:

"...we give a treatment of set forcing appropriate for working over models of a theory PROVI which may plausibly claim to be the weakest set theory supporting a smooth theory of set forcing, and of which the minimal model is Jensen's $J_\omega$."

See his papers here: https://www.dpmms.cam.ac.uk/~ardm/

-