Boolean valued formulas

If we consider a single-valued relation from propositions to their truth values, taken as Booleans, then we get an especially simple semantics. Let ${{\mathbb{B} }} = \{tt, f\!f\}$ and let $\mathbf{B}\!:\!Prop \times {{\mathbb{B} }} \rightarrow Prop$ such that $P \Leftrightarrow \mathbf{B}(P, tt)$.

In classical mathematics one usually assumes the existence of a function like b, say $\mathbf{b}\!:\!Prop \rightarrow {{\mathbb{B} }}$ where $P \Leftrightarrow \mathbf{b}(P) = tt$ in ${{\mathbb{B} }}$. But since b is not a computable function, this way of describing the situation would not be used in constructive mathematics. Instead we could talk about ``decidable propositions'' or ``boolean propositions.''Boolean proposition

$$BoolProp == \{\langle P, v\rangle : Prop \times {{\mathbb{B} }} \vert P \Leftrightarrow (v = tt~in~{{\mathbb{B} }})\}$$

Then there is a function $\mathbf{b} \in BoolProp \rightarrow {{\mathbb{B} }}$ such that $P \Leftrightarrow\left(\mathbf{b}(P) = tt\ \mbox{in}\ {{\mathbb{B} }}\right)$.

If we interpret formulas as representing elements of pure boolean propositions, then each variable P_i denotes an element of ${{\mathbb{B} }}$. An assignmenttruth assignment $\alpha$ is a mapping of variables into ${{\mathbb{B} }}$, that is, an element of $Variables \rightarrow {\mathbb{B} }$. Given an assignment $\alpha$ we can compute a boolean value for any formula F. Namely

	$V\!alue(F, \alpha) =$	if F is a variable, then $\alpha(F)$
		if F is $(F_1\: op\: F_2)$ then $V\!alue(F_1, \alpha)\: bop\: V\!alue(F_2, \alpha)$

where bop is the boolean operation corresponding to the propositional operator op in the usual way, e.g.

P	Q	P $\&_b$ Q	P $\vee_b$ Q	P $\Rightarrow_b$ Q
tt	tt	tt	tt	tt
ff	tt	ff	tt	tt
tt	ff	ff	tt	ff
ff	ff	ff	ff	tt