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

f : B x B -> B or f : B^2 -> B.  The concrete type takes into

account the qualitative dimensions or the "units" of the case,

which can be explained as follows.

  Let !P! be the set of two values {(p), p} = {not-p, p} ~=~ B

| Let <math>P\!</math> be the set of values <math>\{ \texttt{(} p \texttt{)},~ p \} ~=~ \{ \operatorname{not}~ p,~ p \} ~\cong~ \mathbb{B}.</math>

| Let <math>Q\!</math> be the set of values <math>\{ \texttt{(} q \texttt{)},~ q \} ~=~ \{ \operatorname{not}~ q,~ q \} ~\cong~ \mathbb{B}.</math>

Then interpret the usual propositions about <math>p, q\!</math> as functions of the concrete type <math>f : P \times Q \to \mathbb{B}.</math>

 

Then interpret the usual propositions about p, q

as functions of concrete type f : !P! x !Q! -> B.

We are going to consider various "operators" on these functions.

We are going to consider various "operators" on these functions.

Here, an operator W is a function that takes one function f into

Here, an operator W is a function that takes one function f into