Boolean-valued model

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 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 of elements of M, the model must assign an element of M to the term f(a0,...,an-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 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 of elements of M, the model must assign an element of B to be the truth value . 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 is simply The completeness of the Boolean algebra is required to define truth values for quantified formulas.