SUO: *Date 30 Apr 2002 -- Differential Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
SUO WG Members,
Once again, here is the collected and corrected edition of
the work on differential logic that I have been posting to
the Ontology Sublist. I would've sent just the links, but
there were so many annoying typos that I thought it would
be helpful to make a fresh copy.
Note 3. Local Proposition Df
Last time we computed what will variously be called
the "difference map", the "difference proposition",
or the "local proposition" Df_p for the proposition
f(x, y) = xy at the point p where x = 1 and y = 1.
In the universe U = X x Y, the four propositions
xy, x(y), (x)y, (x)(y) that indicate the "cells",
or the smallest regions of the venn diagram, are
called "singular propositions". These serve as
an alternative notation for naming the points
<1, 1>, <1, 0>, <0, 1>, <0, 0>, respectively.
Thus, we can write Df_p = Df|p = Df|<1, 1> = Df|xy,
so long as we know the frame of reference in force.
Sticking with the example f(x, y) = xy, let us compute the
value of the difference proposition Df at all of the points.
o---------------------------------------o
| |
| x dx y dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ x y |
| o=o-----------o |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o---------------------------------------o
| Df = ((x, dx)(y, dy), xy) |
o---------------------------------------o
o---------------------------------------o
| |
| dx dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ |
| o=o-----------o |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o---------------------------------------o
| Df|xy = ((dx)(dy)) |
o---------------------------------------o
o---------------------------------------o
| |
| o |
| dx | dy |
| o---o o---o |
| \ | | / |
| \ | | / o |
| \| |/ | |
| o=o-----------o |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o---------------------------------------o
| Df|x(y) = (dx) dy |
o---------------------------------------o
o---------------------------------------o
| |
| o |
| | dx dy |
| o---o o---o |
| \ | | / |
| \ | | / o |
| \| |/ | |
| o=o-----------o |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o---------------------------------------o
| Df|(x)y = dx (dy) |
o---------------------------------------o
o---------------------------------------o
| |
| o o |
| | dx | dy |
| o---o o---o |
| \ | | / |
| \ | | / o o |
| \| |/ \ / |
| o=o-----------o |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o---------------------------------------o
| Df|(x)(y) = dx dy |
o---------------------------------------o
The easy way to visualize the values of these graphical
expressions is just to notice the following equivalents:
o---------------------------------------o
| |
| x |
| o-o-o-...-o-o-o |
| \ / |
| \ / |
| \ / |
| \ / x |
| \ / o |
| \ / | |
| @ = @ |
| |
o---------------------------------------o
| (x, , ... , , ) = (x) |
o---------------------------------------o
o---------------------------------------o
| |
| o |
| x_1 x_2 x_k | |
| o---o-...-o---o |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / x_1 ... x_k |
| @ = @ |
| |
o---------------------------------------o
| (x_1, ..., x_k, ()) = x_1 · ... · x_k |
o---------------------------------------o
Laying out the arrows on the augmented venn diagram,
one gets a picture of a "differential vector field".
o---------------------------------------o
| |
| dx dy |
| ^ |
| o | o |
| / \ | / \ |
| / \|/ \ |
| /dy | dx\ |
| /(dx) /|\ (dy)\ |
| / ^ /`|`\ ^ \ |
| / \``|``/ \ |
| / /`\`|`/`\ \ |
| / /```\|/```\ \ |
| o x o`````o`````o y o |
| \ \`````````/ / |
| \ o---->```<----o / |
| \ dy \``^``/ dx / |
| \(dx) \`|`/ (dy)/ |
| \ \|/ / |
| \ | / |
| \ /|\ / |
| \ / | \ / |
| o | o |
| | |
| dx | dy |
| o |
| |
o---------------------------------------o
This really just constitutes a depiction of
the interpretations in EU = X x Y x dX x dY
that satisfy the difference proposition Df,
namely, these:
1. x y dx dy
2. x y dx (dy)
3. x y (dx) dy
4. x (y)(dx) dy
5. (x) y dx (dy)
6. (x)(y) dx dy
By inspection, it is fairly easy to understand Df
as telling you what you have to do from each point
of U in order to change the value borne by f(x, y).
Note 4. Difference Operator D
We have been studying the action of the difference operator D,
also known as the "localization operator", on the proposition
f : X x Y -> B that is commonly known as the conjunction x·y.
We described Df as a (first order) differential proposition,
that is, a proposition of the type Df : X x Y x dX x dY -> B.
Abstracting from the augmented venn diagram that illustrates
how the "models", or the "satisfying interpretations", of Df
distribute within the extended universe EU = X x Y x dX x dY,
we can depict Df in the form of a "digraph" or directed graph,
one whose points are labeled with the elements of U = X x Y
and whose arrows are labeled with the elements of dU = dX x dY.
o---------------------------------------o
| |
| x · y |
| |
| o |
| ^^^ |
| / | \ |
| (dx)· dy / | \ dx ·(dy) |
| / | \ |
| / | \ |
| v | v |
| x ·(y) o | o (x)· y |
| | |
| | |
| dx · dy |
| | |
| | |
| v |
| o |
| |
| (x)·(y) |
| |
o---------------------------------------o
| |
| f = x y |
| |
| Df = x y · ((dx)(dy)) |
| |
| + x (y) · (dx) dy |
| |
| + (x) y · dx (dy) |
| |
| + (x)(y) · dx dy |
| |
o---------------------------------------o
Any proposition worth its salt, as they say,
has many equivalent ways to look at it, any
of which may reveal some unsuspected aspect
of its meaning. We will encounter more and
more of these alternative readings as we go.
Note 5. Enlargement Operator E
The enlargement operator E, also known as the "shift operator",
has many interesting and very useful properties in its own right,
so let us not fail to observe a few of the more salient features
that play out on the surface of our simple example, f(x, y) = xy.
Introduce a suitably generic definition of the extended universe of discourse:
Let U = X_1 x ... x X_k and EU = U x dU = X_1 x ... x X_k x dX_1 x ... x dX_k.
For a proposition f : X_1 x ... x X_k -> B,
the (first order) 'enlargement' of f is the
proposition Ef : EU -> B that is defined by:
Ef(x_1, ..., x_k, dx_1, ..., dx_k) = f(x_1 + dx_1, ..., x_k + dx_k).
It should be noted that the so-called "differential variables" dx_j
are really just the same kind of boolean variables as the other x_j.
It is conventional to give the additional variables these brands of
inflected names, but whatever extra connotations we might choose to
attach to these syntactic conveniences are wholly external to their
purely algebraic meanings.
For the example f(x, y) = xy, we obtain:
Ef(x, y, dx, dy) = (x + dx)(y + dy).
Given that this expression uses nothing more than the "boolean ring"
operations of addition (+) and multiplication (·), it is permissible
to "multiply things out" in the usual manner to arrive at the result:
Ef(x, y, dx, dy) = x·y + x·dy + y·dx + dx·dy.
To understand what this means in logical terms, for instance, as expressed
in a boolean expansion or a "disjunctive normal form" (DNF), it is perhaps
a little better to go back and analyze the expression the same way that we
did for Df. Thus, let us compute the value of the enlarged proposition Ef
at each of the points in the universe of discourse U = X x Y.
o---------------------------------------o
| |
| x dx y dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ |
| @=@ |
| |
o---------------------------------------o
| Ef = (x, dx)·(y, dy) |
o---------------------------------------o
o---------------------------------------o
| |
| dx dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ |
| @=@ |
| |
o---------------------------------------o
| Ef|xy = (dx)·(dy) |
o---------------------------------------o
o---------------------------------------o
| |
| o |
| dx | dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ |
| @=@ |
| |
o---------------------------------------o
| Ef|x(y) = (dx)· dy |
o---------------------------------------o
o---------------------------------------o
| |
| o |
| | dx dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ |
| @=@ |
| |
o---------------------------------------o
| Ef|(x)y = dx ·(dy) |
o---------------------------------------o
o---------------------------------------o
| |
| o o |
| | dx | dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ |
| @=@ |
| |
o---------------------------------------o
| Ef|(x)(y) = dx · dy |
o---------------------------------------o
Given the sort of data that arises from this form of analysis,
we can now fold the disjoined ingredients back into a boolean
expansion or a DNF that is equivalent to the proposition Ef.
Ef = xy · Ef_xy + x(y) · Ef_x(y) + (x)y · Ef_(x)y + (x)(y) · Ef_(x)(y).
Here is a summary of the result, illustrated by means of a digraph picture,
where the "no change" element (dx)(dy) is drawn as a loop at the point x·y.
o---------------------------------------o
| |
| x · y |
| (dx)·(dy) |
| -->-- |
| \ / |
| \ / |
| o |
| ^^^ |
| / | \ |
| / | \ |
| (dx)· dy / | \ dx ·(dy) |
| / | \ |
| / | \ |
| x ·(y) o | o (x)· y |
| | |
| | |
| dx · dy |
| | |
| | |
| o |
| |
| (x)·(y) |
| |
o---------------------------------------o
| |
| f = x y |
| |
| Ef = x y · (dx)(dy) |
| |
| + x (y) · (dx) dy |
| |
| + (x) y · dx (dy) |
| |
| + (x)(y) · dx dy |
| |
o---------------------------------------o
We may understand the enlarged proposition Ef
as telling us all the different ways to reach
a model of f from any point of the universe U.
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤