In mathematical logic, a Boolean-valued model is a generalization of the ordinary Tarskian notion of structure from model theory. In a Boolean-valued model, the truth values of propositions are not limited to "true" and "false", but instead take values in some fixed complete Boolean algebra.

Boolean-valued models were introduced by Dana Scott, Robert M. Solovay, and Petr Vopěnka in the 1960s in order to help understand Paul Cohen's method of forcing. They are also related to Heyting algebra semantics in intuitionistic logic.

Fix a complete Boolean algebra B^[1] and a first-order language L; the signature of L will consist of a collection of constant symbols, function symbols, and relation symbols.

A Boolean-valued model for the language L consists of a universe M, which is a set of elements (or names), together with interpretations for the symbols. Specifically, the model must assign to each constant symbol of L an element of M, and to each n-ary function symbol f of L and each n-tuple ⟨a₀,...,a_n-1⟩ of elements of M, the model must assign an element of M to the term f(a₀,...,a_n-1).

Interpretation of the atomic formulas of L is more complicated. To each pair a and b of elements of M, the model must assign a truth value ‖a = b‖ to the expression a = b; this truth value is taken from the Boolean algebra B. Similarly, for each n-ary relation symbol R of L and each n-tuple ⟨a₀,...,a_n-1⟩ of elements of M, the model must assign an element of B to be the truth value ‖R(a₀,...,a_n-1)‖.

The truth values of the atomic formulas can be used to reconstruct the truth values of more complicated formulas, using the structure of the Boolean algebra. For propositional connectives, this is easy; one simply applies the corresponding Boolean operators to the truth values of the subformulae. For example, if φ(x) and ψ(y,z) are formulas with one and two free variables, respectively, and if a, b, c are elements of the model's universe to be substituted for x, y, and z, then the truth value of

${\displaystyle \phi (a)\land \psi (b,c)}$

is simply

${\displaystyle \|\phi (a)\land \psi (b,c)\|=\|\phi (a)\|\ \land \ \|\psi (b,c)\|}$

The completeness of the Boolean algebra is required to define truth values for quantified formulas. If φ(x) is a formula with free variable x (and possibly other free variables that are suppressed), then

${\displaystyle \|\exists x\phi (x)\|=\bigvee _{a\in M}\|\phi (a)\|,}$

where the right-hand side is to be understood as the supremum in B of the set of all truth values ||φ(a)|| as a ranges over M.

The truth value of a formula is an element of the complete Boolean algebra B.

Given a complete Boolean algebra B^[1] there is a Boolean-valued model denoted by V^B, which is the Boolean-valued analogue of the von Neumann universe V. (Strictly speaking, V^B is a proper class, so we need to reinterpret what it means to be a model appropriately.) Informally, the elements of V^B are "Boolean-valued sets". Given an ordinary set A, every set either is or is not a member; but given a Boolean-valued set, every set has a certain, fixed membership degree in A.

The elements of the Boolean-valued set, in turn, are also Boolean-valued sets, whose elements are also Boolean-valued sets, and so on. In order to obtain a non-circular definition of Boolean-valued set, they are defined inductively in a hierarchy similar to the cumulative hierarchy. For each ordinal α of V, the set V^B_α is defined as follows.

• V^B₀ is the empty set.
• V^B_α+1 is the set of all functions from V^B_α to B. (Such a function represents a subset of V^B_α; if f is such a function, then for any x ∈ V^B_α, the value f(x) is the membership degree of x in the set.)
• If α is a limit ordinal, V^B_α is the union of V^B_β for β < α.

The class V^B is defined to be the union of all sets V^B_α.

It is also possible to relativize this entire construction to some transitive model M of ZF (or sometimes a fragment thereof). The Boolean-valued model M^B is obtained by applying the above construction inside M. The restriction to transitive models is not serious, as the Mostowski collapsing theorem implies that every "reasonable" (well-founded, extensional) model is isomorphic to a transitive one. (If the model M is not transitive things get messier, as M′s interpretation of what it means to be a "function" or an "ordinal" may differ from the "external" interpretation.)

Once the elements of V^B have been defined as above, it is necessary to define B-valued relations of equality and membership on V^B. Here a B-valued relation on V^B is a function from V^B × V^B to B. To avoid confusion with the usual equality and membership, these are denoted by ‖x = y‖ and ‖x ∈ y‖ for x and y in V^B. They are defined as follows:

‖x ∈ y‖ is defined to be Σ_{t ∈ Dom(y)} ‖x = t‖ ∧ y(t)   ("x is in y if it is equal to something in y").

‖x = y‖ is defined to be ‖x ⊆ y‖∧‖y ⊆ x‖   ("x equals y if x and y are both subsets of each other"), where

‖x ⊆ y‖ is defined to be Π_{t ∈ Dom(x)} x(t) ⇒ ‖t ∈ y‖   ("x is a subset of y if all elements of x are in y")

The symbols Σ and Π denote the least upper bound and greatest lower bound operations, respectively, in the complete Boolean algebra B. At first sight the definitions above appear to be circular: ‖∈‖ depends on ‖=‖, which depends on ‖⊆‖, which depends on ‖∈‖. However, a close examination shows that the definition of ‖∈‖ only depends on ‖∈‖ for elements of smaller rank, so ‖∈‖ and ‖=‖ are well defined functions from V^B×V^B to B.

It can be shown that the B-valued relations ‖∈‖ and ‖=‖ on V^B make V^B into a Boolean-valued model of set theory. Each sentence of first-order set theory with no free variables has a truth value in B; it must be shown that the axioms for equality and all the axioms of ZF set theory (written without free variables) have truth value 1 (the largest element of B). This proof is straightforward, but it is long because there are many different axioms that need to be checked.

Set theorists use a technique called forcing to obtain independence results and to construct models of set theory for other purposes. The method was originally developed by Paul Cohen but has been greatly extended since then. In one form, forcing "adds to the universe" a generic subset of a poset, the poset being designed to impose interesting properties on the newly added object. The wrinkle is that (for interesting posets) it can be proved that there simply is no such generic subset of the poset. There are three usual ways of dealing with this:

• syntactic forcing A forcing relation ${\displaystyle p\Vdash \phi }$ is defined between elements p of the poset and formulas φ of the forcing language. This relation is defined syntactically and has no semantics; that is, no model is ever produced. Rather, starting with the assumption that ZFC (or some other axiomatization of set theory) proves the independent statement, one shows that ZFC must also be able to prove a contradiction. However, the forcing is "over V"; that is, it is not necessary to start with a countable transitive model. See Kunen (1980) for an exposition of this method.
• countable transitive models One starts with a countable transitive model M of as much of set theory as is needed for the desired purpose, and that contains the poset. Then there do exist filters on the poset that are generic over M; that is, that meet all dense open subsets of the poset that happen also to be elements of M.
• fictional generic objects Commonly, set theorists will simply pretend that the poset has a subset that is generic over all of V. This generic object, in nontrivial cases, cannot be an element of V, and therefore "does not really exist". (Of course, it is a point of philosophical contention whether any sets "really exist", but that is outside the scope of the current discussion.) With a little practice this method is useful and reliable, but it can be philosophically unsatisfying.

Boolean-valued models can be used to give semantics to syntactic forcing; the price paid is that the semantics is not 2-valued ("true or false"), but assigns truth values from some complete Boolean algebra. Given a forcing poset P, there is a corresponding complete Boolean algebra B, often obtained as the collection of regular open subsets of P, where the topology on P is defined by declaring all lower sets open (and all upper sets closed). (Other approaches to constructing B are discussed below.)

Now the order on B (after removing the zero element) can replace P for forcing purposes, and the forcing relation can be interpreted semantically by saying that, for p an element of B and φ a formula of the forcing language,

${\displaystyle p\Vdash \phi \iff p\leq ||\phi ||}$

where ||φ|| is the truth value of φ in V^B.

This approach succeeds in assigning a semantics to forcing over V without resorting to fictional generic objects. The disadvantages are that the semantics is not 2-valued, and that the combinatorics of B are often more complicated than those of the underlying poset P.

One interpretation of forcing starts with a countable transitive model M of ZF set theory, a partially ordered set P, and a "generic" subset G of P, and constructs a new model of ZF set theory from these objects. (The conditions that the model be countable and transitive simplify some technical problems, but are not essential.) Cohen's construction can be carried out using Boolean-valued models as follows.

• Construct a complete Boolean algebra B as the complete Boolean algebra "generated by" the poset P.
• Construct an ultrafilter U on B (or equivalently a homomorphism from B to the Boolean algebra {true, false}) from the generic subset G of P.
• Use the homomorphism from B to {true, false} to turn the Boolean-valued model M^B of the section above into an ordinary model of ZF.

We now explain these steps in more detail.

For any poset P there is a complete Boolean algebra B and a map e from P to B⁺ (the non-zero elements of B) such that the image is dense, e(p)≤e(q) whenever p≤q, and e(p)e(q)=0 whenever p and q are incompatible. This Boolean algebra is unique up to isomorphism. It can be constructed as the algebra of regular open sets in the topological space of P (with underlying set P, and a base given by the sets U_p of elements q with q≤p).

The map from the poset P to the complete Boolean algebra B is not injective in general. The map is injective if and only if P has the following property: if every r≤p is compatible with q, then p≤q.

The ultrafilter U on B is defined to be the set of elements b of B that are greater than some element of (the image of) G. Given an ultrafilter U on a Boolean algebra, we get a homomorphism to {true, false} by mapping U to true and its complement to false. Conversely, given such a homomorphism, the inverse image of true is an ultrafilter, so ultrafilters are essentially the same as homomorphisms to {true, false}. (Algebraists might prefer to use maximal ideals instead of ultrafilters: the complement of an ultrafilter is a maximal ideal, and conversely the complement of a maximal ideal is an ultrafilter.)

If g is a homomorphism from a Boolean algebra B to a Boolean algebra C and M^B is any B-valued model of ZF (or of any other theory for that matter) we can turn M^B into a C -valued model by applying the homomorphism g to the value of all formulas. In particular if C is {true, false} we get a {true, false}-valued model. This is almost the same as an ordinary model: in fact we get an ordinary model on the set of equivalence classes under || = || of a {true, false}-valued model. So we get an ordinary model of ZF set theory by starting from M, a Boolean algebra B, and an ultrafilter U on B. (The model of ZF constructed like this is not transitive. In practice one applies the Mostowski collapsing theorem to turn this into a transitive model.)

We have seen that forcing can be done using Boolean-valued models, by constructing a Boolean algebra with ultrafilter from a poset with a generic subset. It is also possible to go back the other way: given a Boolean algebra B, we can form a poset P of all the nonzero elements of B, and a generic ultrafilter on B restricts to a generic set on P. So the techniques of forcing and Boolean-valued models are essentially equivalent.

• Bell, J. L. (1985) Boolean-Valued Models and Independence Proofs in Set Theory, Oxford. ISBN 0-19-853241-5
• Grishin, V.N. (2001) [1994], "Boolean-valued model", Encyclopedia of Mathematics, EMS Press
• Jech, Thomas (2002). Set theory, third millennium edition (revised and expanded). Springer. ISBN 3-540-44085-2. OCLC 174929965.
• Kunen, Kenneth (1980). Set Theory: An Introduction to Independence Proofs. North-Holland. ISBN 0-444-85401-0. OCLC 12808956.
• Kusraev, A. G. and S. S. Kutateladze (1999). Boolean Valued Analysis. Kluwer Academic Publishers. ISBN 0-7923-5921-6. OCLC 41967176. Contains an account of Boolean-valued models and applications to Riesz spaces, Banach spaces and algebras.
• Manin, Yu. I. (1977). A Course in Mathematical Logic. Springer. ISBN 0-387-90243-0. OCLC 2797938. Contains an account of forcing and Boolean-valued models written for mathematicians who are not set theorists.
• Rosser, J. Barkley (1969). Simplified Independence Proofs, Boolean valued models of set theory. Academic Press.