12,122
edits
Changes
Directory:Jon Awbrey/Papers/Differential Logic : Introduction (view source)
Revision as of 20:30, 15 June 2009
, 20:30, 15 June 2009→Note 22: markup + convert graphics
Let us take a moment to view an old proposition in this new light, for example, the logical conjunction <math>pq : X \to \mathbb{B}</math> pictured in Figure 22-a.
Let us take a moment to view an old proposition in this new light, for example, the logical conjunction <math>pq : X \to \mathbb{B}</math> pictured in Figure 22-a.
{| align="center" cellpadding="10" style="text-align:center"
{| align="center" cellpadding="6" style="text-align:center"
| [[Image:Venn Diagram F = P And Q.jpg|500px]]
| [[Image:Venn Diagram F = P And Q.jpg|500px]]
|-
|-
| <math>\text{Figure 22-a.}~ ~\operatorname{Conjunction}~ pq : X \to \mathbb{B}</math>
| <math>\text{Figure 22-a. Conjunction}~ pq : X \to \mathbb{B}</math>
|}
|}
Each of the operators <math>\operatorname{E}, \operatorname{D} : X^\circ \to \operatorname{E}X^\circ</math> takes us from considering propositions <math>f : X \to \mathbb{B},</math> here viewed as ''scalar fields'' over <math>X,\!</math> to considering the corresponding ''differential fields'' over <math>X,\!</math> analogous to what are usually called ''vector fields'' over <math>X.\!</math>
<pre>
<pre>
The structure of these differential fields can be described this way.
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:
To each point of X there is attached an object of the following type:
and we see the differential proposition Wf: EX -> B as a vector field,
and we see the differential proposition Wf: EX -> B as a vector field,
specifically, a field of propositions about contemplated changes in X.
specifically, a field of propositions about contemplated changes in X.
</pre>
The field of changes produced by E on pq is shown in Figure 22-b.
The field of changes produced by <math>\operatorname{E}</math> on <math>pq\!</math> is shown in Figure 22-b.
{| align="center" cellpadding="6" style="text-align:center"
|
<pre>
o-------------------------------------------------o
o-------------------------------------------------o
| |
| |
| |
| |
o-------------------------------------------------o
o-------------------------------------------------o
| f = p q |
</pre>
|-
| <math>\text{Figure 22-b. Enlargement}~ \operatorname{E}(pq) : \operatorname{E}X \to \mathbb{B}</math>
|-
|
<math>\begin{array}{rcccccc}
f
& = & p & \cdot & q
\\[4pt]
\operatorname{E}f
| |
& = & p & \cdot & q & \cdot & (\operatorname{d}p)(\operatorname{d}q)
\\[4pt]
& + & p & \cdot & (q) & \cdot & (\operatorname{d}p)~\operatorname{d}q~
\\[4pt]
& + & (p) & \cdot & q & \cdot & ~\operatorname{d}p~(\operatorname{d}q)
\\[4pt]
& + & (p) & \cdot & (q) & \cdot & ~\operatorname{d}p~~\operatorname{d}q~\end{array}</math>
|}
The differential field E[pq] specifies the changes
The differential field <math>\operatorname{E}(pq)</math> specifies the changes that need to be made from each point of <math>X\!</math> in order to reach one of the models of the proposition <math>pq,\!</math> that is, in order to satisfy the proposition <math>pq.\!</math>
that need to be made from each point of X in order
to reach one of the models of the proposition pq,
that is, in order to satisfy the proposition pq.
The field of changes produced by D on pq is shown in Figure 22-c.
The field of changes produced by <math>\operatorname{D}\!</math> on <math>pq\!</math> is shown in Figure 22-c.
{| align="center" cellpadding="6" style="text-align:center"
|
<pre>
o-------------------------------------------------o
o-------------------------------------------------o
| |
| |
o-------------------------------------------------o
o-------------------------------------------------o
Figure 22-c. Difference D[pq] : EX -> B
Figure 22-c. Difference D[pq] : EX -> B
</pre>
|}
The differential field D[pq] specifies the changes
The differential field <math>\operatorname{D}(pq)</math> specifies the changes that need to be made from each point of <math>X\!</math> in order to feel a change in the felt value of the field <math>pq.\!</math>
that need to be made from each point of X in order
to feel a change in the felt value of the field pq.
</pre>
==Note 23==
==Note 23==