Changes

When <math>X\!</math> is the type of space that is generated by <math>\{ u, v, w \}\!</math>, let <math>\operatorname{d}X</math> be the type of space that is generated by <math>\{ \operatorname{d}u, \operatorname{d}v, \operatorname{d}w \}</math>, and let <math>X \times \operatorname{d}X</math> be the type of space that is generated by the extended set of boolean basis elements <math>\{ u, v, w, \operatorname{d}u, \operatorname{d}v, \operatorname{d}w \}</math>.  For convenience, define a notation "<math>\operatorname{E}X</math>" so that <math>\operatorname{E}X = X \times \operatorname{d}X</math>.  Even though the differential variables are in some abstract sense no different than other boolean variables, it usually helps to mark their distinctive roles and their differential interpretation by means of the distinguishing domain name "<math>\operatorname{d}\mathbb{B}</math>".  Using these designations of logical spaces, the propositions over them can be assigned both abstract and concrete types.

When <math>X\!</math> is the type of space that is generated by <math>\{ u, v, w \}\!</math>, let <math>\operatorname{d}X</math> be the type of space that is generated by <math>\{ \operatorname{d}u, \operatorname{d}v, \operatorname{d}w \}</math>, and let <math>X \times \operatorname{d}X</math> be the type of space that is generated by the extended set of boolean basis elements <math>\{ u, v, w, \operatorname{d}u, \operatorname{d}v, \operatorname{d}w \}</math>.  For convenience, define a notation "<math>\operatorname{E}X</math>" so that <math>\operatorname{E}X = X \times \operatorname{d}X</math>.  Even though the differential variables are in some abstract sense no different than other boolean variables, it usually helps to mark their distinctive roles and their differential interpretation by means of the distinguishing domain name "<math>\operatorname{d}\mathbb{B}</math>".  Using these designations of logical spaces, the propositions over them can be assigned both abstract and concrete types.

For instance, consider the proposition <math>q(u, v, w)\!</math>, as before, and then consider its tacit extension <math>q(u, v, w, \operatorname{d}u, \operatorname{d}v, \operatorname{d}w)\!</math>, the latter of which may be indicated more explicitly as "<math>\operatorname{e}q\!</math>".

For instance, consider the proposition q<u, v, w>, as before,

and then consider its tacit extension q<u, v, w, du, dv, dw>,

the latter of which may be indicated more explicitly as "eq".

1.  Proposition q is abstractly typed as q : B^3 -> B.

#<p>Proposition <math>q\!</math> is abstractly typed as <math>q : \mathbb{B}^3 \to \mathbb{B}.</math></p><p>Proposition <math>q\!</math> is concretely typed as <math>q : X \to \mathbb{B}.</math></p>

    Proposition q is concretely typed as q : X -> B.

#<p>Proposition <math>\operatorname{e}q\!</math> is abstractly typed as <math>\operatorname{e}q : \mathbb{B}^3 \times \operatorname{d}\mathbb{B}^3 \to \mathbb{B}.</math></p><p>Proposition <math>\operatorname{e}q\!</math> is concretely typed as <math>\operatorname{e}q : X \times \operatorname{d}X \to \mathbb{B}.</math></p><p>Succinctly, <math>\operatorname{e}q : \operatorname{E}X \to \mathbb{B}.</math></p>

We now return to our consideration of the effects of various differential operators on propositions. This time around we have enough exact terminology that we shall be able to explain what is actually going on here in a rather more articulate fashion.

 

We now return to our consideration of the effects

of various differential operators on propositions.

This time around we have enough exact terminology

that we shall be able to explain what is actually

going on here in a rather more articulate fashion.

The first transformation of the source proposition q that we may

The first transformation of the source proposition q that we may

wish to stop and examine, though it is not unusual to skip right

wish to stop and examine, though it is not unusual to skip right