ONT Re: Differential Logic -- Series A
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
DLOG. Note A4
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
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 xy.
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
| f = x y |
o-------------------------------------------------o
| |
| Df = x y ((dx)(dy)) |
| |
| + x (y) (dx) dy |
| |
| + (x) y dx (dy) |
| |
| + (x)(y) dx dy |
| |
o-------------------------------------------------o
| |
| x y |
| x (y) o<------------->o<------------->o (x) y |
| (dx) dy ^ dx (dy) |
| | |
| | |
| dx | dy |
| | |
| | |
| v |
| o |
| (x) (y) |
| |
o-------------------------------------------------o
Any proposition worth its salt has many equivalent ways to view it,
any one of which may reveal some unsuspected aspect of its meaning.
We will encounter more and more of these variant readings as we go.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
http://www.cs.bsu.edu/homepages/mighty/history.html
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o