12,080
edits
Changes
Directory:Jon Awbrey/Papers/Differential Logic : Introduction (view source)
Revision as of 21:00, 15 June 2009
, 21:00, 15 June 2009→Note 22: markup
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>
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>
The structure of these differential fields can be described this way. With each point of <math>X\!</math> there is associated an object of the following type: a proposition about changes in <math>X,\!</math> that is, a proposition <math>g : \operatorname{d}X \to \mathbb{B}.</math> In this frame of reference, if <math>X^\circ</math> is the universe that is generated by the set of coordinate propositions <math>\{ p, q \},\!</math> then <math>\operatorname{d}X^\circ</math> is the differential universe that is generated by the set of differential propositions <math>\{ \operatorname{d}p, \operatorname{d}q \}.</math> These differential propositions may be interpreted as indicating <math>{}^{\backprime\backprime} \text{change in}\, p \, {}^{\prime\prime}</math> and <math>{}^{\backprime\backprime} \text{change in}\, q \, {}^{\prime\prime},</math> respectively.
<pre>
<pre>
A differential operator W, of the first order sort that we have
A differential operator W, of the first order sort that we have
been considering, takes a proposition f : X -> B and gives back
been considering, takes a proposition f : X -> B and gives back