[Inquiry] Re: Dynamics And Logic

[Jon Awbrey]

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

DAL.  Note 6

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

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<p, q> = pq.

To begin we need to formulate a suitably generic
definition of the extended universe of discourse:

   Relative to an initial domain X = X_1 x ... x X_k,

   EX = X x dX = 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 : EX -> B that is defined by:

   Ef<x_1, ..., x_k, dx_1, ..., dx_k>

   =  f<x_1 + dx_1, ..., x_k + 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 type of boolean variables as the other x_j.
It is conventional to give the additional variables these inflected
names, but whatever extra connotations we attach to these syntactic
conveniences are wholly external to their purely algebraic meanings.

In the case of the conjunction f<p, q> = pq,
the enlargement Ef is formulated as follows:

   Ef<p, q, dp, dq>

   =  [p + dp][q + dq]

   =  (p, dp)(q, dq)

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<p, q, dp, dq>

   =  p q  +  p dq  +  q dp  +  dp dq

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 initial domain of discourse X = !P! x !Q!.

o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` p `dp q `dq ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o---o o---o ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` | | `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ | | / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\| |/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` @=@ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
| Ef =` ` ` ` ` ` (p, dp) (q, dq) ` ` ` ` ` ` ` ` |
o-------------------------------------------------o

o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `dp ` `dq ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o---o o---o ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` | | `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ | | / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\| |/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` @=@ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
| Ef|pq = ` ` ` ` ` `(dp) (dq)` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o

o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `dp | `dq ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o---o o---o ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` | | `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ | | / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\| |/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` @=@ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
| Ef|p(q) = ` ` ` ` `(dp) `dq ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o

o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` | `dp ` `dq ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o---o o---o ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` | | `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ | | / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\| |/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` @=@ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
| Ef|(p)q = ` ` ` ` ` dp` (dq)` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o

o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` | `dp | `dq ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o---o o---o ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` | | `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ | | / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\| |/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` @=@ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
| Ef|(p)(q) = ` ` ` ` dp` `dq ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o

Given the kind 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 = pq Ef_pq + p(q) Ef_p(q) + (p)q Ef_(p)q + (p)(q) Ef_(p)(q)

Here is a summary of the result, illustrated by means of
a digraph picture, where the "no change" element (dp)(dq)
is drawn as a loop at the point p q.

o-------------------------------------------------o
| `f =` ` ` ` ` ` ` ` ` p q ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| Ef =` ` ` ` ` ` ` p `q` `(dp)(dq) ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` + ` ` ` p (q) `(dp) dq` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` + ` ` `(p) q` ` dp (dq) ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` + ` ` `(p)(q) ` dp` dq` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `(dp) (dq)` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `.--->---.` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\p q/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` |
| `p (q) o-------------->o<--------------o (p) q` |
| ` ` ` ` ` ` (dp) dq ` `^` ` dp (dq) ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` dp | dq ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` (p) (q) ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
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 X.

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o