ONT Re: Differential Logic
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
DLOG. Note D41
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
The Secant Operator: $E$ (concl.)
If one is working within the confines of propositional calculus,
it is possible to give an elementary definition of $E$F by means
of a system of propositional equations, as will now be described.
Given a transformation:
F = <F_1, ..., F_k> : B^n -> B^k
of concrete type:
F : [u_1, ..., u_n] -> [x_1, ..., x_k]
the transformation:
$E$F = <F_1, ..., F_k, EF_1, ..., EF_k> : B^n x D^n -> B^k x D^k
of concrete type:
$E$F : [u_1, ..., u_n, du_1, ..., du_n] -> [x_1, ..., x_k, dx_1, ..., dx_k]
is defined by means of the following system of logical equations:
o--------------------------------------------------------------------------------------o
| |
| x_1 = !e!F_1 <u_1, ..., u_n, du_1, ..., du_n> = F_1 <u_1, ..., u_n> |
| |
| ... |
| |
| x_k = !e!F_k <u_1, ..., u_n, du_1, ..., du_n> = F_k <u_1, ..., u_n> |
| |
| |
| dx_1 = EF_1 <u_1, ..., u_n, du_1, ..., du_n> = F_1 <u_1 + du_1, ..., u_n + du_n> |
| |
| ... |
| |
| dx_k = EF_k <u_1, ..., u_n, du_1, ..., du_n> = F_k <u_1 + du_1, ..., u_n + du_n> |
| |
o--------------------------------------------------------------------------------------o
It is important to note that this system of equations can be read as a conjunction
of equational propositions, in effect, as a single proposition in the universe of
discourse that is generated by all of the named variables. Specifically, this
is the universe of discourse over 2(n + k) variables that is denoted by:
E[!U! |_| !X!] = [u_1, ..., u_n, x_1, ..., x_k, du_1, ..., du_n, dx_1, ..., dx_k].
In this light, it should be clear that the system of equations defining $E$F embodies,
in a higher rank and in a differentially extended version, an analogy with the process
of thematization that was treated earlier for propositions of the type F : B^n -> B.
The entire collection of constraints that is represented in the above system
of equations may be abbreviated by writing $E$F = <!e!F, EF>, for any map F.
This is tantamount to regarding $E$ as a complex operator, $E$ = <!e!, E>,
with a form of application that distributes each component of the operator
to work on each component of the operand:
$E$F = <!e!, E> F = <!e!F, EF> = <!e!F_1, ..., !e!F_k, EF_1, ..., EF_k>.
Quite a lot of "thematic infrastructure" or interpretive information
is being swept under the rug in the use of such abbreviations. When
confusion arises about the meaning of such constructions, one always
has recourse to the defining system of equations, in its totality a
purely propositional expression. This means that the angle brackets,
which were used in this context to build an image of multi-component
transformations, should not be expected to determine a well-defined
product in themselves, but only to serve as reminders of the prior
thematic decisions (choices of variable names, etc.) that have to
be made in order to determine one. Accordingly, the angle bracket
notation < , > can be regarded as a kind of "thematic frame", an
interpretive storage device that preserves the proper associations
of concrete logical features between the extended universes at the
source and target of $E$F.
The generic notations $d$^0.F, $d$^1.F, ..., $d$^m.F in Figure 33 refer to
the increasing orders of differentials that are extracted in the course of
analyzing F. When the analysis is halted at a partial stage of development,
notations like $r$^0.F, $r$^1.F, ..., $r$^m.F may be used to summarize the
contributions to $E$F that remain to be analyzed. The Figure illustrates
a convention that renders the remainder term $r$^m.F, in effect, the sum
of all differentials of order strictly greater than m.
I next discuss the set of operators that figure into this form of analysis,
describing their effects on transformations. In simplified or specialized
contexts these operators tend to take on a variety of different names and
notations, some of whose number I will introduce along the way.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o