ONT Re: Differential Logic -- Series A

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

DLOG.  Note A3

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

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
|                                                 |
|                        o                        |
|                        |                        |
|                      dx|dy                      |
|                        |                        |
|          o-----------o | o-----------o          |
|         /             \|/             \         |
|        /       x       |       y       \        |
|       /               /|\               \       |
|      /               /`|`\               \      |
|     o               o``|``o               o     |
|     |      dy (dx)  |``v``|  dx (dy)      |     |
|     |   o-----------|->o<-|-----------o   |     |
|     |               |`````|               |     |
|     |   o<----------|--o--|---------->o   |     |
|     |      dy (dx)  |``|``|  dx (dy)      |     |
|     o               o``|``o               o     |
|      \               \`|`/               /      |
|       \               \|/               /       |
|        \               |               /        |
|         \             /|\             /         |
|          o-----------o | o-----------o          |
|                        |                        |
|                      dx|dy                      |
|                        |                        |
|                        v                        |
|                        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).

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
http://www.cs.bsu.edu/homepages/mighty/history.html
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o