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.

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

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

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

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 <math>\operatorname{F}</math> is a function that takes one function <math>f\!</math> into another function <math>\operatorname{F}f.</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.

The first couple of operators that we need to consider are logical analogues

The first couple of operators that we need to consider are logical analogues

of those that occur in the classical "finite difference calculus", namely:

of those that occur in the classical "finite difference calculus", namely: