Boolean-valued model

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.

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.

For propositional connectives, this is easy; one simply applies the corresponding Boolean operators to the truth values of the subformulae.

If φ(x) is a formula with free variable x (and possibly other free variables that are suppressed), then 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 VB, which is the Boolean-valued analogue of the von Neumann universe V. (Strictly speaking, VB is a proper class, so we need to reinterpret what it means to be a model appropriately.)

It is also possible to relativize this entire construction to some transitive model M of ZF (or sometimes a fragment thereof).

However, a close examination shows that the definition of ‖∈‖ only depends on ‖∈‖ for elements of smaller rank, so ‖∈‖ and ‖=‖ are well defined functions from VB×VB to B.

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 approach succeeds in assigning a semantics to forcing over V without resorting to fictional generic objects.

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.

So we get an ordinary model of ZF set theory by starting from M, a Boolean algebra B, and an ultrafilter U on B.

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.