A gentle introduction to Boolean-valued model theory

This is an excerpt from my book-in-progress on diverse elementary topics in logic, from the chapter on model theory.  My view is that Boolean-valued models should be elevated to the status of a standard core topic of elementary model theory, adjacent to the ultrapower construction. The theory of Boolean-valued models is both beautiful and accessible, both generalizing and explaining the ultrapower method, while also partaking of deeper philosophical issues concerning multi-valued truth.

Boolean-valued models

Let us extend our familiar model concept from classical predicate logic to the comparatively fantastic realm of multi-valued predicate logic. We seek a multi-valued-truth concept of model, with a domain of individuals of some kind and interpretations for the relations, functions, and constants from a first-order language, but in which the truths of the model are not necessarily black and white, but exhibit their truth values in a given multi-valued logic. Let us focus especially on the case of Boolean-valued models, using a complete Boolean algebra $\newcommand\B{\mathbb{B}}\B$, since this case has been particularly well developed and successful; the set-theoretic method of forcing, for example, amounts to using $\B$-valued models of set theory with carefully chosen complete Boolean algebras $\B$ and has been used impressively to establish a sweeping set-theoretic independence phenomenon, showing that numerous set-theoretic principles such as the axiom of choice and the continuum hypothesis are independent of the other axioms of set theory.

The main idea of Boolean-valued models, however, is applicable with any theory, not just set theory, and there are Boolean-valued graphs, Boolean-valued orders, Boolean-valued groups, rings, and fields. So let us develop a little of this theory, keeping in mind that the basic construction and ideas also often work fruitfully with other multi-valued logics, not just Boolean algebras.

Definition of Boolean-valued models

We defined in an earlier section what it means to be a model in classical first-order predicate logic—one specifies the domain of the model, a set of individuals that will constitute the universe of the model over which all the quantifiers will range, and then provides interpretations on that domain for each relation symbol, function symbol, and constant symbol in the language. For each relation symbol $R$, for example, and any suitable tuple of individuals $a,b$ from the domain, one specifies whether $R(a,b)$ is to hold or fail in the model.

The main idea for defining what it means to be a model in multi-valued predicate logic is to replace these classical yes-or-no atomic truths with multi-valued atomic truth assertions. Specifically, for any Boolean algebra $\B$, a $\B$-valued model $\mathcal{M}$ in the language $\mathcal{L}$ consists of a domain $M$, whose elements are called names, and an assignment of $\B$-valued truth values for all the simple atomic formulas using parameters from that domain:$\newcommand\boolval[1]{[\![#1]\!]}$\begin{eqnarray*}
% \nonumber % Remove numbering (before each equation)
s=t&\mapsto& \boolval{s=t} \\
R(s_0,\ldots,s_n) &\mapsto& \boolval{R(s_0,\ldots,s_n)} \\
y=f(s_0,\ldots,s_n) &\mapsto& \boolval{y=f(s_0,\ldots,s_n)}
\end{eqnarray*}
The double-bracketed expressions here $\boolval{\varphi}$ denote an element of the Boolean algebra $\B$—one thinks of $\boolval{\varphi}$ as the $\B$-truth value of $\varphi$ in the model, and the model is defined by specifying these values for the simple atomic formulas.

We shall insist in any Boolean-valued model that the atomic truth values obey the laws of equality:
$$\begin{array}{rcl}
\boolval{s=s} &=& 1\\
\boolval{s=t} &=& \boolval{t=s}\\
\boolval{s=t}\wedge\boolval{t=u} &\leq& \boolval{s=u}\\
\bigwedge_{i<n}\boolval{s_i=t_i}\wedge\boolval{R(\vec s)} &\leq & \boolval{R(\vec t)}.\end{array}$$And if the language includes functions symbols, then we also insist on the functionality axioms:
$$\begin{array}{rcl}
\bigwedge_{i<n}\boolval{s_i=t_i}\wedge\boolval{y=f(\vec s)} &\leq& \boolval{y=f(\vec t)}\\
\bigvee_{t\in M}\boolval{t=f(\vec s)} &=& 1\\
\boolval{t_0=f(\vec s)}\wedge\boolval{t_1=f(\vec s)} &\leq& \boolval{t_0=t_1}.\\
\end{array}$$
These requirements assert respectively in the Boolean-valued context that the equality axiom holds for function application, that the function takes on some value, and that the function takes on at most one value. In effect, the Boolean-valued model treatment of functions regards them as as defined by their graph relations, and these functionality axioms ensure that the relation has the features that would be expected of such a graph relation.

In summary, a $\B$-valued model is a domain of names together with $\B$-valued truth assignments for the simple atomic assertions about those names, which obey the equality and functionality axioms.

Boolean-valued equality

The nature of equality in the Boolean-valued setting offers an interesting departure from the usual classical treatment that is worth discussing explicitly. Namely, in classical predicate logic with equality, distinct elements of the domain are taken to represent distinct individuals in the model—the assertion $a=b$ is true in the model only when $a$ and $b$ are identical as elements of the domain. In the Boolean-valued setting, however, we want to relax this in order to allow equality assertions to have an intermediate Boolean value. For this reason, distinct elements of the domain can no longer be taken to represent definitely distinct individuals, since the equality assertion $\boolval{a=b}$ might have some nonzero or intermediate degree of truth. The elements of the domain of a Boolean-valued model are allowed in effect a bit of indecision or indeterminacy about who they are and whether they might be identical. This is why we think of the elements of the domain as names for individuals, rather than as the individuals themselves. Two different names can have an intermediate truth-value possibility of naming the same or different individuals.

Extending to Boolean-valued truth

By definition, every $\B$-valued model provides $\B$-valued truth assertions for the simple atomic formulas. We now extend these Boolean-valued truth assignments to all assertions of the language through the following natural recursion:
$$\begin{array}{rcl}
\boolval{\varphi\wedge\psi} &=& \boolval{\varphi}\wedge\boolval{\psi}\\
\boolval{\neg\varphi} &=& \neg\boolval{\varphi}\\
\boolval{\exists x\,\varphi(x,\vec s)} &=& \bigvee_{t\in M}\boolval{\varphi(t,\vec s)},\text{ if this supremum exists in }\B\\
\end{array}$$
On the right-hand side, we make the logical calculations in each case using the operations of the Boolean algebra $\B$. In the existential case, the supremum may range over an infinite set of Boolean values, if the domain of the model is infinite, and so this supremum might not be realized as an element of $\B$, if it is not complete. This is precisely why one commonly considers $\B$-valued models especially in the case of a complete Boolean algebra $\B$—the completeness of $\B$ ensures that this supremum exists and so the recursion has a solution.

The reader may check by induction on $\varphi$ that the general equality axiom now has Boolean value one.
$$\boolval{\vec s=\vec t\wedge \varphi(\vec s)\implies\varphi(\vec t)}=1$$
The Boolean-valued structure $\mathcal{M}$ is full if for every formula $\varphi(x,\vec x)$ in $\mathcal{L}$ and $\vec s$ in $M$, there is some $t\in M$ such that $\boolval{\exists x\,\varphi(x,\vec s)}=\boolval{\varphi(t,\vec s)}$. That is, a model is full when it is rich enough with names that the Boolean value of every existential statement is realized by a particular witness, reducing the infinitary supremum in the recursive definition to a single largest element.

A simple example

For every natural number $n\geq 3$ let $C_n$ be the graph on $n$ vertices forming an $n$-cycle with edge relation $x\sim y$. So we have a triangle $C_3$, a square $C_4$, a pentagon $C_5$, and so on. Let $\B=P(\set{n\in\newcommand\N{\mathbb{N}}\N\mid n\geq 3})$ be the power set of these indices, which forms a complete Boolean algebra. We define a $\B$-valued graph model $\mathcal{C}$ as follows. We take as names the sequences $a=\langle a_n\rangle_{n\geq 3}$ with $a_n\in C_n$ for every $n$.

We define the equality and $\sim$ edge relations on these names as follows:
\begin{eqnarray*}
\boolval{a=b}&=&\set{n\mid a_n=b_n} \\
\boolval{a\sim b}&=&\set{n\mid C_n\newcommand\satisfies{\models}\satisfies a_n\sim b_n}.
\end{eqnarray*}
Thus, two names are equal exactly to extent that they have the same coordinates, and two names are connected by the edge relation $\sim$ exactly to the extent to that this is true on the coordinates. It is now easy to verify the equality axioms, since $a\sim b$ is true to at least the extent that $a’\sim b’$, $a=a’$, and $b=b’$ are true, since if $a_n=a’_n$, $b_n=b’_n$, and $a’_n\sim b’_n$ in $C_n$, then also $a_n\sim b_n$. So this is a $\B$-valued graph model.

So we have a Boolean-valued graph. Is it connected? Does that question make sense? Of course, we don’t have an actual graph here, but only a $\B$-valued graph, and so in principle we only know how to compute the Boolean value of statements that are expressible in the language of graph theory. Since connectivity is not formally expressible, except in the bounded finite cases, this question might not be sensible.

Let me argue that it is indeterminate whether this graph is a complete graph with every pair of distinct nodes connected by an edge. After all, $C_3$ is the complete graph on three vertices, and it will follow from the theorem below that the Boolean value of the statement $\forall x,y\,(x=y\vee x\sim y)$ contains the element $3$ and therefore this Boolean value is not zero. Meanwhile, the assertion that the graph is not complete, however, also gets a nonzero Boolean value, since every $C_n$ except $C_3$ has distinct nodes with no edge between them. In a robust sense, the graph-theoretic truths of $\mathcal{C}$ combine the truths of all the various graphs $C_n$.

Note also that as $n$ increases, the graphs $C_n$ have nodes that are increasingly far apart. Fix any name $\langle a\rangle_{n\geq 3}$ and choose $\langle b\rangle_{n\geq 3}$ such that the distance between $a_n$ and $b_n$ in $C_n$ is not bounded by any particular uniform bound. In $\mathcal{C}$, it follows that $a$ and $b$ have no particular definite finite distance, and this can be viewed as a sense in which $\mathcal{C}$ is not connected.

A combination of many models

Let us flesh out the previous example with a more general analysis. Suppose we have a family of models $\set{M_i\mid i\in I}$ in a common language $\mathcal{L}$. Let $\B=P(I)$ be the power set of the set of indices $I$, a complete Boolean algebra. We define a $\B$-valued model $\mathcal{M}$ as follows. The set of names will be precisely the product of the models $M=\prod_i M_i$, which is to say, the $I$-tuples $s=\langle s_i\mid i\in I\rangle$ with $s_i\in M_i$ for every $i\in I$, and the simple atomic truth values are defined like this:
\begin{eqnarray*}
\boolval{s=t}&=&\set{i\in I\mid s_i=t_i} \\
\boolval{R(s,\ldots,t)}&=&\set{i\in I\mid M_i\satisfies R(s_i,\dots,t_i)}\\
\boolval{u=f(s,\ldots,t)} &=& \set{i\in I\mid M_i\satisfies u_i=f(s_i,\dots,t_i)}.
\end{eqnarray*}
One can now prove the equality and functionality axioms, and so this is a $\B$-valued model.

Theorem. The Boolean-valued model $\mathcal{M}$ described above is full, and Boolean-valued truth can be computed coordinatewise:
$$\boolval{\varphi(s,\dots,t)}=\set{i\in I\mid M_i\satisfies\varphi(s_i,\dots,t_i)}.$$

Proof. We prove this by induction on $\varphi$, for assertions using only simple atomic formulas, $\wedge$, $\neg$, and $\exists$. The simple atomic case is part of what it means to be a Boolean-valued model. If the theorem is true for $\varphi$, then it will be true for $\neg\varphi$, since negation in $\B$ is complementation in $I$, as follows:
$$\boolval{\neg\varphi}=\neg\boolval{\varphi}=I-\set{i\in I\mid M_i\satisfies\varphi}=\set{i\in I\mid M_i\satisfies\neg\varphi}.$$
If the theorem is true for $\varphi$ and $\psi$, then it will be true for $\varphi\wedge\psi$ as follows:
\begin{eqnarray*}
\boolval{\varphi\wedge\psi} &=& \boolval{\varphi}\wedge\boolval{\psi} \\
&=& \set{i\in I\mid M_i\satisfies\varphi}\cap\set{i\in I\mid M_i\satisfies\psi}\\
&=& \set{i\in I\mid M_i\satisfies\varphi\wedge\psi}.
\end{eqnarray*}
For the quantifier case $\exists x\, \varphi(x,s,\dots,t)$, choose $u_i\in M_i$ for which $M_i\satisfies\varphi(u_i,s_i,\dots,t_i)$, if possible. It follows that
$$\set{i\in I\mid M_i\satisfies\exists x\,\varphi(x,s_i,\dots,t_i)}=\set{i\in I\mid M_i\satisfies\varphi(u_i,s_i,\dots,t_i)},$$
and from this it follows that $\boolval{\varphi(v,s,\dots,t)}\leq\boolval{\varphi(u,s,\dots,t)}$, since whenever $v_i$ succeeds as a witness then so also will $u_i$. Consequently, the model is full, and we see that
\begin{eqnarray*}
\boolval{\exists x\,\varphi(x,s,\dots,t)} &=& \bigvee_{v\in M}\boolval{\varphi(v,s,\dots,t)}\\
&=& \boolval{\varphi(u,s,\dots,t)}\\
&=& \set{i\in I\mid M_i\satisfies\exists x\,\varphi(x,s_i,\dots,t_i)},
\end{eqnarray*}
as desired. $\Box$

Boolean ultrapowers

Every Boolean-valued model can be transformed into a classical model, a $2$-valued model, by means of a simple quotient construction. Suppose that $\mathcal{M}$ is a $\B$-valued model for some Boolean algebra $\B$ and that $\mu\newcommand\of{\subseteq}\of\B$ is an ultrafilter on the Boolean algebra.

Define an equivalence relation $=_\mu$ on the set of names by
$$a=_\mu b\quad\text{ if and only if }\quad \boolval{a=b}\in\mu.$$
The quotient structure $\mathcal{M}/\mu$ will consist of equivalence classes $[a]_\mu$ of names by this equivalence relation. We define the atomic truths of the quotient structure similarly by reference to whether these truths hold with a value in $\mu$. Namely,
$$R^{\mathcal{M}/\mu}([a]_\mu,\ldots,[b]_\mu)\quad\text{ if and only if }\quad \boolval{R(a,\dots,b)}\in\mu.$$
For function symbols $f$, we define
$$[c]_\mu=f([a]_\mu,\dots,[b]_\mu)\quad\text{ if and only if }\quad \boolval{c=f(a,\dots,b)}\in\mu.$$
These definitions are well-defined modulo $=_\mu$ precisely because of the equality axiom properties of the Boolean-valued model $\mathcal{M}$. For example, if $a=_\mu a’$, then $\boolval{a=a’}\in\mu$, but $\boolval{a=a’}\wedge\boolval{R(a)}\leq \boolval{R(a’)}$ by the equality axiom, and so if $\boolval{R(a)}$ is in $\mu$, then so will be $\boolval{R(a’)}$.

We defined atomic truth in the quotient structure by reference to the truth value being $\mu$-large. In fact, this reduction will continue for all truth assertions in the quotient structure, which we prove as follows.

Theorem. (Łoś theorem for Boolean ultrapowers)
Suppose that $\mathcal{M}$ is a full $\B$-valued model for a Boolean algebra $\B$, and that $\mu\of\B$ is an ultrafilter. Then a statement is true in the Boolean quotient structure $\mathcal{M}/\mu$ if and only if the Boolean value of the statement is in $\mu$.
$$\mathcal{M}/\mu\satisfies\varphi([a]_\mu,\dots,[b]_\mu)\quad\text{ if and only if }\quad\boolval{\varphi(a,\dots,b)}\in\mu.$$

Proof. We prove this by induction on $\varphi$. The simple atomic case holds by the definition of the quotient structure. Boolean connectives $\wedge$, $\neg$ follow easily using that $\mu$ is a filter and that it is an ultrafilter. Consider the quantifier case $\exists x\, \varphi(a,\dots,b,x)$, where by induction the theorem holds for $\varphi$ itself. If the quotient structure satisfies the existential $\mathcal{M}/\mu\satisfies\exists x\,\varphi([a],\dots,[b],x)$, then there is a name $c$ for which it satisfies $\varphi([a],\dots,[b],[c])$, and so by induction $\boolval{\varphi(a,\dots,b,c)}\in\mu$, in which case also $\boolval{\exists x\,\varphi(a,\dots,b,x)}\in\mu$, since this latter Boolean value is at least as great as the former. Conversely, if $\boolval{\exists x\,\varphi(a,\dots,b,x)}\in\mu$, then by fullness this existential Boolean value is realized by some name $c$, and so $\boolval{\varphi(a,\dots,b,c)}\in\mu$, which by induction implies that the quotient satisfies $\varphi([a],\dots,[b],[c])$ and consequently also $\exists x\,\varphi([a],\dots,[b],x)$, as desired. $\Box$

Note how fullness was used in the existential case of the inductive argument.

Boolean ultrapowers, the Bukovský-Dehornoy phenomenon, and iterated ultrapowers

  • G. Fuchs and J. D. Hamkins, “The Bukovský-Dehornoy phenomenon for Boolean ultrapowers,” ArXiv e-prints, 2017. (Under review)  
    @ARTICLE{FuchsHamkins:TheBukovskyDehornoyPhenomenonForBooleanUltrapowers,
    AUTHOR = {Gunter Fuchs and Joel David Hamkins},
    TITLE = {The {Bukovsk\'y-Dehornoy} phenomenon for {Boolean} ultrapowers},
    JOURNAL = {ArXiv e-prints},
    YEAR = {2017},
    volume = {},
    number = {},
    pages = {},
    month = {},
    note = {Under review},
    abstract = {},
    keywords = {under-review},
    source = {},
    eprint = {1707.06702},
    archivePrefix = {arXiv},
    primaryClass = {math.LO},
    url = {http://wp.me/p5M0LV-1zz},
    }

Abstract. We show that while the length $\omega$ iterated ultrapower by a normal ultrafilter is a Boolean ultrapower by the Boolean algebra of Příkrý forcing, it is consistent that no iteration of length greater than $\omega$ (of the same ultrafilter and its images) is a Boolean ultrapower. For longer iterations, where different ultrafilters are used, this is possible, though, and we give Magidor forcing and a generalization of Příkrý forcing as examples. We refer to the discovery that the intersection of the finite iterates of the universe by a normal measure is the same as the generic extension of the direct limit model by the critical sequence as the Bukovský-Dehornoy phenomenon, and we develop a criterion (the existence of a simple skeleton) for when a version of this phenomenon holds in the context of Boolean ultrapowers.

Tutorial on Boolean ultrapowers, BLAST 2015, Las Cruces, NM

I shall give a tutorial lecture series on Boolean ultrapowers, two or three lectures, at the BLAST conference in Las Cruces, New Mexico, January 5-9, 2015.  (The big AMS meeting in San Antonio, reportedly a quick flight, begins on the 10th.)

BLAST is a conference series focusing on

B = Boolean Algebras
L = Lattices, Algebraic and Quantum Logic
A = Universal Algebra
S = Set Theory
T = Set-theoretic and Point-free Topology

In this tutorial, I shall give a general introduction to the Boolean ultrapower construction.

Organ Mountains, NM, with snow

Boolean ultrapowers generalize the classical ultrapower construction on a power-set algebra to the context of an ultrafilter on an arbitrary complete Boolean algebra. Introduced by Vopěnka as a means of undertaking forcing constructions internally to ZFC, the method has many connections with forcing. Nevertheless, the Boolean ultrapower construction stands on its own as a general model-theoretic construction technique, and historically, researchers have come to the Boolean ultrapower concept from both set theory and model theory.  An emerging interest in Boolean ultrapowers arises from a focus on well-founded Boolean ultrapowers as large cardinal embeddings.

In this tutorial, we shall see that the Boolean ultrapower construction reveals that two central set-theoretic techniques–forcing and classical ultrapowers–are facets of a single underlying construction, namely, the Boolean ultrapower.  I shall provide a thorough introduction to the Boolean ultrapower construction, assuming only an elementary graduate student-level familiarity with set theory and the classical ultrapower and forcing techniques.

Article | Tutorial lecture notes  | Blast 2015BLAST 2013 | Boolean ultrapowers tutorial at YSTW Bonn, 2011

Inner models with large cardinal features usually obtained by forcing

  • A. W.~Apter, V. Gitman, and J. D. Hamkins, “Inner models with large cardinal features usually obtained by forcing,” Archive for Math.~Logic, vol. 51, pp. 257-283, 2012.  
    @article {ApterGitmanHamkins2012:InnerModelsWithLargeCardinals,
    author = {Arthur W.~Apter and Victoria Gitman and Joel David Hamkins},
    affiliation = {Mathematics, The Graduate Center of the City University of New York, 365 Fifth Avenue, New York, NY 10016, USA},
    title = {Inner models with large cardinal features usually obtained by forcing},
    journal = {Archive for Math.~Logic},
    publisher = {Springer},
    issn = {0933-5846},
    keyword = {},
    pages = {257--283},
    volume = {51},
    issue = {3},
    url = {http://jdh.hamkins.org/innermodels},
    eprint = {1111.0856},
    archivePrefix = {arXiv},
    primaryClass = {math.LO},
    doi = {10.1007/s00153-011-0264-5},
    note = {},
    year = {2012},
    }

We construct a variety of inner models exhibiting features usually obtained by forcing over universes with large cardinals. For example, if there is a supercompact cardinal, then there is an inner model with a Laver indestructible supercompact cardinal. If there is a supercompact cardinal, then there is an inner model with a supercompact cardinal $\kappa$ for which $2^\kappa=\kappa^+$, another for which $2^\kappa=\kappa^{++}$ and another in which the least strongly compact cardinal is supercompact. If there is a strongly compact cardinal, then there is an inner model with a strongly compact cardinal, for which the measurable cardinals are bounded below it and another inner model $W$ with a strongly compact cardinal $\kappa$, such that $H_{\kappa^+}^V\subseteq HOD^W$. Similar facts hold for supercompact, measurable and strongly Ramsey cardinals. If a cardinal is supercompact up to a weakly iterable cardinal, then there is an inner model of the Proper Forcing Axiom and another inner model with a supercompact cardinal in which GCH+V=HOD holds. Under the same hypothesis, there is an inner model with level by level equivalence between strong compactness and supercompactness, and indeed, another in which there is level by level inequivalence between strong compactness and supercompactness. If a cardinal is strongly compact up to a weakly iterable cardinal, then there is an inner model in which the least measurable cardinal is strongly compact. If there is a weakly iterable limit $\delta$ of ${\lt}\delta$-supercompact cardinals, then there is an inner model with a proper class of Laver-indestructible supercompact cardinals. We describe three general proof methods, which can be used to prove many similar results.

An introduction to Boolean ultrapowers, Bonn, 2011

A four-lecture tutorial on the topic of Boolean ultrapowers at the Young Set Theory Workshop at the Hausdorff Center for Mathematics in Königswinter near Bonn, Germany,  March 21-25, 2011.

Boolean ultrapowers generalize the classical ultrapower construction on a power-set algebra to the context of an ultrafilter on an arbitrary complete Boolean algebra. Closely related to forcing and particularly to the use of Boolean-valued models in forcing, Boolean ultrapowers were introduced by Vopenka in order to carry out forcing as an internal ZFC construction, rather than as a meta-theoretic argument as in Cohen’s approach. An emerging interest in Boolean ultrapowers has arisen from a focus on the well-founded Boolean ultrapowers as large cardinal embeddings.

Historically, researchers have come to the Boolean ultrapower concept from two directions, from set theory and from model theory. Exemplifying the set-theoretic perspective, Bell’s classic (1985) exposition emphasizes the Boolean-valued model $V^{\mathbb{B}}$ and its quotients $V^{\mathbb{B}}/U$, rather than the Boolean ultrapower $V_U$ itself, which is not considered there. Mansfield (1970), in contrast, gives a purely algebraic, forcing-free account of the Boolean ultrapower, emphasizing its potential as a model-theoretic technique, while lacking the accompanying generic objects.

The unifying view I will explore in this tutorial is that the well-founded Boolean ultrapowers reveal the two central concerns of set-theoretic research–forcing and large cardinals–to be two aspects of a single underlying construction, the Boolean ultrapower, whose consequent close connections might be more fruitfully explored. I will provide a thorough introduction to the Boolean ultrapower construction, while assuming only an elementary graduate student-level familiarity with set theory and the classical ultrapower and forcing techniques.

ArticleAbstract | Lecture Notes