User:Jon Awbrey/DIFF/C
Differential Logic : Series C
It would be good to summarize, in rough but intuitive terms, the outlook on differential logic that we have reached so far.
We have been considering a class of operators on universes of discourse, each of which takes us from considering one universe of discourse, X, to considering a larger universe of discourse, EX.
Each of these operators, in general terms having the form F : X -> EX, acts on each proposition p : X -> B of the source universe X to produce a proposition Fp : EX -> B of the target universe EX.
The two main operators that we have worked with up to this point are the enlargement operator E : X -> EX and the difference operator D : X -> EX.
E and D take a proposition in X, that is, a proposition p : X -> B that is said to be "about" the subject matter of X, and produce the extended propositions Ep, Dp : EX -> B, which may be interpreted as being about specified collections of changes that might occur in X.
Here we have need of visual representations, some array of concrete pictures to anchor our more earthy intuitions and to help us keep our wits about us before we try to climb any higher into the ever more rarefied air of abstractions.
One good picture comes to us by way of the "field" concept. Given a space X, a "field" of a specified type T over X is formed by assigning to each point of X an object of type T. If that sounds like the same thing as a function from X to the space of things of type T, it is, but it does seems to help to vary the mental pictures and the figures of speech that naturally spring to mind within these fertile fields.
In the field picture, a proposition p : X -> B becomes a "scalar" field, that is, a field of values in B, or a "field of true-false indications".
Let us take a moment to view an old proposition in this new light, for example, the conjunction uv : X -> B that is depicted in Figure 1.
o-------------------------------------------------o | X | | | | o-------------o o-------------o | | / \ / \ | | / o \ | | / /`\ \ | | / /```\ \ | | o o`````o o | | | |`````| | | | | U |`````| V | | | | |`````| | | | o o`````o o | | \ \```/ / | | \ \`/ / | | \ o / | | \ / \ / | | o-------------o o-------------o | | | | | o-------------------------------------------------o | f = u v | o-------------------------------------------------o Figure 1. Conjunction uv : X -> B
Each of the operators E, D : X -> EX takes us from considering propositions p : X -> B, here viewed as "scalar fields" over X, to considering the corresponding "differential fields" over X, analogous to what are usually called "vector fields" over X.
The structure of these differential fields can be described this way. To each point of X there is attached an object of the following type, a proposition about changes in X, that is, a proposition g : dX -> B. In this setting, if X is the universe that is generated by the set of coordinate propositions {u, v}, then dX is the differential universe that is generated by the set of differential propositions {du, dv}. These differential propositions may be interpreted as indicating "change in u" and "change in v", respectively.
A differential operator F, of the first order sort that we have been considering, takes a proposition p : X -> B and gives back a differential proposition Fp : EX -> B.
In the field view, we see the proposition p : X -> B as a scalar field and we see the differential proposition Fp : EX -> B as a vector field, specifically, a field of propositions about contemplated changes in X.
The field of changes produced by E on uv is shown in Figure 2.
o-------------------------------------------------o | X | | | | o-------------o o-------------o | | / \ / \ | | / U o V \ | | / /`\ \ | | / /```\ \ | | o o.->-.o o | | | u(v)(du)dv |`\`/`| (u)v du(dv) | | | | o---------------|->o<-|---------------o | | | | |``^``| | | | o o``|``o o | | \ \`|`/ / | | \ \|/ / | | \ o / | | \ /|\ / | | o-------------o | o-------------o | | | | | | | | | | | o | | (u)(v) du dv | | | o-------------------------------------------------o | f = u v | o-------------------------------------------------o | | | Ef = u v (du)(dv) | | | | + u (v) (du) dv | | | | + (u) v du (dv) | | | | + (u)(v) du dv | | | o-------------------------------------------------o Figure 2. Enlargement E[uv] : EX -> B
The differential field E[uv] specifies the changes that need to be made from each point of X in order to reach one of the models of the proposition uv, that is, in order to satisfy the proposition uv.
The field of changes produced by D on uv is shown in Figure 3.
o-------------------------------------------------o | X | | | | o-------------o o-------------o | | / \ / \ | | / U o V \ | | / /`\ \ | | / /```\ \ | | o o`````o o | | | (du)dv |`````| du(dv) | | | | o<--------------|->o<-|-------------->o | | | | |``^``| | | | o o``|``o o | | \ \`|`/ / | | \ \|/ / | | \ o / | | \ /|\ / | | o-------------o | o-------------o | | | | | | | | v | | o | | du dv | | | o-------------------------------------------------o | f = u v | o-------------------------------------------------o | | | Df = u v ((du)(dv)) | | | | + u (v) (du) dv | | | | + (u) v du (dv) | | | | + (u)(v) du dv | | | o-------------------------------------------------o Figure 3. Difference D[uv] : EX -> B
The differential field D[uv] specifies the changes that need to be made from each point of X in order to change the value of the proposition uv.
