Changes

A function like this has an abstract type and a concrete type.  The abstract type is what we invoke when we write things like <math>f : \mathbb{B} \times \mathbb{B} \to \mathbb{B}</math> or <math>f : \mathbb{B}^2 \to \mathbb{B}.</math>  The concrete type takes into account the qualitative dimensions or the "units" of the case, which can be explained as follows.

A function like this has an abstract type and a concrete type.  The abstract type is what we invoke when we write things like <math>f : \mathbb{B} \times \mathbb{B} \to \mathbb{B}</math> or <math>f : \mathbb{B}^2 \to \mathbb{B}.</math>  The concrete type takes into account the qualitative dimensions or the "units" of the case, which can be explained as follows.

* Let ''X'' be the set of values {(''x''), ''x''} = {not ''x'', ''x''}.

* Let <math>X\!</math> be the set of values <math>\{ (\!|x|\!), x \} = \{ \operatorname{not}\ x, x \}.</math>

* Let ''Y'' be the set of values {(''y''), ''y''} = {not ''y'', ''y''}.

* Let <math>Y\!</math> be the set of values <math>\{ (\!|y|\!), y \} = \{ \operatorname{not}\ y, y \}.</math>

Then interpret the usual propositions about ''x'', ''y'' as functions of the concrete type ''f''&nbsp;:&nbsp;''X''&nbsp;&times;&nbsp;''Y''&nbsp;&rarr;&nbsp;'''B'''.

Then interpret the usual propositions about <math>x, y\!</math> as functions of the concrete type <math>f : X \times Y \to \mathbb{B}.</math>

We are going to consider various "operators" on these functions.  Here, an operator ''F'' is a function that takes one function ''f'' into another function ''Ff''.

We are going to consider various "operators" on these functions.  Here, an operator ''F'' is a function that takes one function ''f'' into another function ''Ff''.