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 <math>X\!</math> be the set of values <math>\{ (\!|x|\!), x \} = \{ \operatorname{not}\ x, x \}.</math>

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

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

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

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>

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

The first couple of operators that we need to consider are logical analogues of those that occur in the classical "finite difference calculus", namely:

The first couple of operators that we need to consider are logical analogues of those that occur in the classical ''finite difference calculus'', namely:

* The ''difference'' operator &Delta;, written here as ''D''.

: The ''difference operator'' <math>\Delta,\!</math> written here as <math>\operatorname{D}.</math>

* The ''enlargement'' operator &Epsilon;, written here as ''E''.

: The ''enlargement operator'' <math>\Epsilon,\!</math> written here as <math>\operatorname{E}.</math>

These days, ''E'' is more often called the ''shift'' operator.

These days, <math>\operatorname{E}</math> is more often called the ''shift operator''.

In order to describe the universe in which these operators operate, it will be necessary to enlarge our original universe of discourse.  We mount up from the space ''U'' = ''X''&nbsp; &times;&nbsp;''Y'' to its ''differential extension'',

In order to describe the universe in which these operators operate, it will be necessary to enlarge our original universe of discourse.  We mount up from the space ''U'' = ''X''&nbsp; &times;&nbsp;''Y'' to its ''differential extension'',