[Inquiry] Re: Differential Logic

[Jon Awbrey]

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

DLOG.  Note D2

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

| Out of the dimness opposite equals advance . . . .
|    Always substance and increase,
| Always a knit of identity . . . . always distinction . . . .
|    always a breed of life.
|
| Walt Whitman, 'Leaves of Grass', [Whi, 28]

A Functional Conception of Propositional Calculus

In the general case, we start with a set of logical features {a_1, ..., a_n}
that represent properties of objects or propositions about the world.  In
concrete examples the features {a_i} commonly appear as capital letters
from an "alphabet" like {A, B, C, ...} or as meaningful words from a
linguistic "vocabulary" of codes.  This language can be drawn from
any sources, whether natural, technical, or artificial in character
and interpretation.  In the application to dynamic systems we tend
to use the letters {x_1, ... , x_n} as our coordinate propositions,
and to interpret them as denoting properties of a system's "state",
that is, as propositions about its location in configuration space.
Because I have to consider non-deterministic systems from the outset,
I often use the word "state" in a loose sense, to denote the position
or configuration component of a contemplated state vector, whether or
not it ever gets a deterministic completion.

The set of logical features {a_1, ..., a_n} provides a basis for generating
an n-dimensional "universe of discourse" that I denote as [a_1, ..., a_n].
It is useful to consider each universe of discourse as a unified categorical
object that incorporates both the set of points <|a_1, ... , a_n|> and the set
of propositions f : <|a_1, ..., a_n|> -> B that are implicit with the ordinary
picture of a venn diagram on n features.  Thus, we may regard the universe of
discourse [a_1, ..., a_n] as an ordered pair having the type (B^n, (B^n - >B)),
and we may abbreviate this last type designation as (B^n +-> B), or even more
succinctly as [B^n].  (NB.  I am using "<| ... |>" as "generator brackets".)

Table 2 exhibits the scheme of notation I use to formalize the domain
of propositional calculus, corresponding to the logical content of
truth tables and venn diagrams.  Although it overworks the square
brackets a bit, I also use either one of the equivalent notations
[n] or #n# to denote the data type of a finite set on n elements.

Table 2.  Fundamental Notations for Propositional Calculus
o---------o-------------------o-------------------o-------------------o
| Symbol  | Notation          | Description       | Type              |
o---------o-------------------o-------------------o-------------------o
| !A!     | {a_1, ..., a_n}   | Alphabet          | [n]  =  #n#       |
o---------o-------------------o-------------------o-------------------o
|  A_i    | {(a_i), a_i}      | Dimension i       |  B                |
o---------o-------------------o-------------------o-------------------o
|  A      | <|!A!|>           | Set of cells,     |  B^n              |
|         | <|a_i, ... a_n|>  | coordinate tuples,|                   |
|         | {<a_i, ... a_n>}  | interpretations,  |                   |
|         | A_1 x ... x A_n   | points, or vectors|                   |
|         | Prod_i A_i        | in the universe   |                   |
o---------o-------------------o-------------------o-------------------o
|  A*     | (hom : A -> B)    | Linear functions  | (B^n)*  =  B^n    |
o---------o-------------------o-------------------o-------------------o
|  A^     | (A -> B)          | Boolean functions |  B^n -> B         |
o---------o-------------------o-------------------o-------------------o
|  A%     | [!A!]             | Universe of Disc. | (B^n, (B^n -> B)) |
|         | (A, A^)           | based on features | (B^n +-> B)       |
|         | (A +-> B)         | {a_i, ..., a_n}   | [B^n]             |
|         | (A, (A -> B))     |                   |                   |
|         | [a_1, ..., a_n]   |                   |                   |
o---------o-------------------o-------------------o-------------------o

Jon Awbrey

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