ONT Re: Differential Logic -- Series B
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
DLOG. Note B6
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
I think that we finally have enough of the preliminary
set-ups and warm-ups out of the way that we can begin
to tackle the differential analysis proper of our
sample proposition q = (( u v )( u w )( v w )).
When X is the type of space that is generated by {u, v, w},
let dX be the type of space that is generated by (du, dv, dw},
and let X x dX be the type of space that is generated by the
extended set of boolean basis elements {u, v, w, du, dv, dw}.
For convenience, define a notation "EX" so that EX = X x dX.
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 "dB".
Using these designations of logical spaces, the propositions
over them can be assigned both abstract and concrete types.
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.
Proposition q is concretely typed as q : X -> B.
2. Proposition eq is abstractly typed as eq : B^3 x dB^3 -> B.
Proposition eq is concretely typed as eq : X x dX -> B.
Succinctly, eq : EX -> B.
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
wish to stop and examine, though it is not unusual to skip right
over this stage of analysis, frequently regarding it as a purely
intermediary stage, holding scarcely even so much as the passing
interest, is the work of the "enlargement" or "shift" operator E.
Applying the operator E to the operand proposition q yields:
o-------------------------------------------------o
| Eq |
o-------------------------------------------------o
| |
| u du v dv u du w dw v dv w dw |
| o---o o---o o---o o---o o---o o---o |
| \ | | / \ | | / \ | | / |
| \ | | / \ | | / \ | | / |
| \| |/ \| |/ \| |/ |
| o=o o=o o=o |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \|/ |
| o |
| | |
| | |
| | |
| @ |
| |
o-------------------------------------------------o
| |
| (( ( u , du ) ( v , dv ) |
| )( ( u , du ) ( w , dw ) |
| )( ( v , dv ) ( w , dw ) |
| )) |
| |
o-------------------------------------------------o
The enlarged proposition Eq is a minimally interpretable as
as a function on the six variables of {u, v, w, du, dv, dw}.
In other words, Eq : EX -> B, or Eq : X x dX -> B.
Conjoining a query on the center cell, c = uvw, yields:
o-------------------------------------------------o
| Eq.c |
o-------------------------------------------------o
| |
| u du v dv u du w dw v dv w dw |
| o---o o---o o---o o---o o---o o---o |
| \ | | / \ | | / \ | | / |
| \ | | / \ | | / \ | | / |
| \| |/ \| |/ \| |/ |
| o=o o=o o=o |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \ | / |
| \|/ |
| o |
| | |
| | |
| | |
| @ u v w |
| |
o-------------------------------------------------o
| |
| (( ( u , du ) ( v , dv ) |
| )( ( u , du ) ( w , dw ) |
| )( ( v , dv ) ( w , dw ) |
| )) |
| |
| u v w |
| |
o-------------------------------------------------o
The models of this last expression tell us which combinations of
feature changes among the set {du, dv, dw} will take us from our
present interpretation, the center cell expressed by "u v w", to
a true value under the given proposition (( u v )( u w )( v w )).
The models of Eq.c can be described in the usual ways as follows:
1. The points of the space EX that have
the following coordinate descriptions:
<u, v, w, du, dv, dw> =
<1, 1, 1, 0, 0, 0>,
<1, 1, 1, 0, 0, 1>,
<1, 1, 1, 0, 1, 0>,
<1, 1, 1, 1, 0, 0>.
2. The points of the space EX that have
the following conjunctive expressions:
u v w (du)(dv)(dw),
u v w (du)(dv) dw ,
u v w (du) dv (dw),
u v w du (dv)(dw).
In summary, Eq.c informs us that we can get from c to a model of q by
making the following changes in our position with respect to u, v, w,
to wit, "change none or just one among {u, v, w}".
I think that it would be worth our time to diagram the models
of the "enlarged" or "shifted" proposition, Eq, at least, the
selection of them that we find issuing from the center cell c.
Figure 4 is an extended venn diagram for the proposition Eq.c,
where the shaded area gives the models of q and the "@" signs
mark the terminal points of the requisite feature alterations.
o-------------------------------------------------o
| X |
| |
| o-------------o |
| / \ |
| / \ |
| / \ |
| / \ |
| o U o |
| | | |
| | | |
| | | |
| o---o---------o o---------o---o |
| / \`````````\ /`````````/ \ |
| / \`````dw``o``dv`````/ \ |
| / \`@<----/@\---->@`/ \ |
| / \`````/`|`\`````/ \ |
| o o---o--|--o---o o |
| | |``|``| | |
| | V |`du``| W | |
| | |` |``| | |
| o o``v``o o |
| \ \`@`/ / |
| \ \`/ / |
| \ o / |
| \ / \ / |
| o-------------o o-------------o |
| |
| |
o-------------------------------------------------o
Figure 4. Effect of the Enlargement Operator E
On the Proposition q, Evaluated at c
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
http://www.cs.bsu.edu/homepages/mighty/history.html
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o