12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Friday May 03, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Differential Logic and Dynamic Systems 2.0 (view source)
Revision as of 03:30, 6 September 2013
, 03:30, 6 September 2013update
|
|
<math>\begin{matrix}
<math>\begin{matrix}
(x, y) & = & F(u, v) & = & ( \texttt{((} u \texttt{)(} v \texttt{))}, \texttt{((} u \texttt{,} v \texttt{))} )
(x, y) & = & F(u, v) & = & ~(~ \texttt{((} u \texttt{)(} v \texttt{))} ~,~ \texttt{((} u \texttt{,} v \texttt{))} ~)~
\end{matrix}</math>
\end{matrix}</math>
|}
|}
<br>
<br>
Table 65 extends this scheme from single cells to arbitrary regions of the source and target universes, and illustrates a form of computation that can be used to determine how a logical transformation acts on all of the propositions in the universe. The way that a transformation of positions affects the propositions, or any other structure that can be built on top of the positions, is normally called the ''induced action'' of the given transformation on the system of structures in question.
Table 65 extends this scheme from single cells to arbitrary regions, showing how we might compute the action of a logical transformation on arbitrary propositions in the universe of discourse. The effect of a point-transformation on arbitrary propositions, or any other structures erected on points, is referred to as the ''induced action'' of the transformation on the structures in question.
<br><font face="courier new">
<br>
{| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
<font face="courier new">
{| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:90%"
|+ '''Table 65. Induced Transformation on Propositions'''
|+ '''Table 65. Induced Transformation on Propositions'''
|- style="background:ghostwhite"
|- style="background:ghostwhite"
|}
|}
|}
|}
</font><br>
</font>
<br>
Since ''G''<sub>1</sub> and ''G''<sub>2</sub> can be any propositions of the type '''B'''<sup>2</sup> → '''B''', there are 2<sup>4</sup> = 16 choices for each of the maps ''G''<sub>1</sub> and ''G''<sub>2</sub>, and thus there are 2<sup>4</sup><math>\cdot</math>2<sup>4</sup> = 2<sup>8</sup> = 256 different mappings altogether of the form ''G'' : ''U''<sup> •</sup> → ''X''<sup> •</sup>. The set of all functions of a given type is customarily denoted by placing its type indicator in parentheses, in the present instance writing (''U''<sup> •</sup> → ''X''<sup> •</sup>) = {''G'' : ''U''<sup> •</sup> → ''X''<sup> •</sup>}, and so the cardinality of this ''function space'' can be most conveniently summed up by writing |(''U''<sup> •</sup> → ''X''<sup> •</sup>)| = |('''B'''<sup>2</sup> → '''B'''<sup>2</sup>)| = 4<sup>4</sup> = 256.
Given the alphabets <math>\mathcal{U} = \{ u, v \}\!</math> and <math>\mathcal{X} = \{ x, y \},\!</math> along with the corresponding universes of discourse <math>U^\bullet, X^\bullet \cong [\mathbb{B}^2],\!</math> how many logical transformations of the general form <math>G = (G_1, G_2) : U^\bullet \to X^\bullet\!</math> are there? Since <math>G_1\!</math> and <math>G_2\!</math> can be any propositions of the type <math>\mathbb{B}^2 \to \mathbb{B},\!</math> there are <math>2^4 = 16\!</math> choices for each of the maps <math>G_1\!</math> and <math>G_2\!</math> and thus there are <math>2^4 \cdot 2^4 = 2^8 = 256\!</math> different mappings altogether of the form <math>G : U^\bullet \to X^\bullet.\!</math> The set of functions of a given type is denoted by placing its type indicator in parentheses, in the present instance writing <math>(U^\bullet \to X^\bullet) = \{ G : U^\bullet \to X^\bullet \},\!</math> and so the cardinality of the ''function space'' <math>(U^\bullet \to X^\bullet)\!</math> is summed up by writing <math>|(U^\bullet \to X^\bullet)| = |(\mathbb{B}^2 \to \mathbb{B}^2)| = 4^4 = 256.\!</math>
Given any transformation ''G'' = ‹''G''<sub>1</sub>, ''G''<sub>2</sub>› : ''U''<sup> •</sup> → ''X''<sup> •</sup> of this type, one can define a couple of further transformations, related to ''G'', that operate between the extended universes, E''U''<sup> •</sup> and E''X''<sup> •</sup>, of its source and target domains.
Given a transformation <math>G = (G_1, G_2) : U^\bullet \to X^\bullet\!</math> of this type, we proceed to define a pair of further transformations, related to <math>G,\!</math> that operate between the extended universes, <math>\mathrm{E}U^\bullet\!</math> and <math>\mathrm{E}X^\bullet,\!</math> of its source and target domains.
First, the enlargement map (or the secant transformation) E''G'' = ‹E''G''<sub>1</sub>, E''G''<sub>2</sub>› : E''U''<sup> •</sup> → E''X''<sup> •</sup> is defined by the following set of component equations:
First, the ''enlargement map'' (or ''secant transformation'') <math>\mathrm{E}G = (\mathrm{E}G_1, \mathrm{E}G_2) : \mathrm{E}U^\bullet \to \mathrm{E}X^\bullet\!</math> is defined by the following set of component equations:
<br><font face="courier new">
<br><font face="courier new">
</font><br>
</font><br>
Next, the ''difference map'' (or ''chordal transformation'') <math>\mathrm{D}G = (\mathrm{D}G_1, \mathrm{D}G_2) : \mathrm{E}U^\bullet \to \mathrm{E}X^\bullet~\!</math> is defined in component-wise fashion as the boolean sum of the initial proposition <math>G_i\!</math> and the enlarged proposition <math>\mathrm{E}G_i,\!</math> for <math>i = 1, 2,\!</math> according to the following set of equations:
<br><font face="courier new">
<br><font face="courier new">
</font><br>
</font><br>
Maintaining a strict analogy with ordinary difference calculus would perhaps have us write D''G''<sub>''i''</sub> = E''G''<sub>''i''</sub> – ''G''<sub>''i''</sub>, but the sum and difference operations are the same thing in boolean arithmetic. It is more often natural in the logical context to consider an initial proposition ''q'', then to compute the enlargement E''q'', and finally to determine the difference D''q'' = ''q'' + E''q'', so we let the variant order of terms reflect this sequence of considerations.
Maintaining a strict analogy with ordinary difference calculus would perhaps have us write <math>\mathrm{D}G_i = \mathrm{E}G_i - G_i,\!</math> but the sum and difference operations are the same thing in boolean arithmetic. It is more often natural in the logical context to consider an initial proposition <math>q,\!</math> then to compute the enlargement <math>\mathrm{E}q,\!</math> and finally to determine the difference <math>\mathrm{D}q = q + \mathrm{E}q,\!</math> so we let the variant order of terms reflect this sequence of considerations.
Viewed in this light the difference operator D is imagined to be a function of very wide scope and polymorphic application, one that is able to realize the association between each transformation ''G'' and its difference map D''G'', for instance, taking the function space (''U''<sup> •</sup> → ''X''<sup> •</sup>) into (E''U''<sup> •</sup> → E''X''<sup> •</sup>). Given the interpretive flexibility of contexts in which we are allowing a proposition to appear, it should be clear that an operator of this scope is not at all a trivial matter to define properly, and may take some trouble to work out. For the moment, let's content ourselves with returning to particular cases.
Viewed in this light the difference operator <math>\mathrm{D}\!</math> is imagined to be a function of very wide scope and polymorphic application, one that is able to realize the association between each transformation <math>G\!</math> and its difference map <math>\mathrm{D}G,\!</math> for example, taking the function space <math>(U^\bullet \to X^\bullet)\!</math> into <math>(\mathrm{E}U^\bullet \to \mathrm{E}X^\bullet).\!</math> When we consider the variety of interpretations permitted to propositions over the contexts in which we put them to use, it should be clear that an operator of this scope is not at all a trivial matter to define in general and that it may take some trouble to work out. For the moment we content ourselves with returning to particular cases.
Acting on the logical transformation <math>F = (f, g) = ~(~ \texttt{((} u \texttt{)(} v \texttt{))} ~,~ \texttt{((} u \texttt{,} v \texttt{))} ~)~,\!</math> the operators <math>\mathrm{E}\!</math> and <math>\mathrm{D}\!</math> yield the enlarged map <math>\mathrm{E}F = (\mathrm{E}f, \mathrm{E}g)\!</math> and the difference map <math>\mathrm{D}F = (\mathrm{D}f, \mathrm{D}g),\!</math> respectively, whose components are given as follows.
<br><font face="courier new">
<br>
<font face="courier new">
{| align="center" border="1" cellpadding="12" cellspacing="0" style="font-weight:bold; text-align:left; width:96%"
{| align="center" border="1" cellpadding="12" cellspacing="0" style="font-weight:bold; text-align:left; width:96%"
|
|
|}
|}
</font>
</font>
<br>
<br>
<font face="courier new">
<font face="courier new">
{| align="center" border="1" cellpadding="12" cellspacing="0" style="font-weight:bold; text-align:left; width:96%"
{| align="center" border="1" cellpadding="12" cellspacing="0" style="font-weight:bold; text-align:left; width:96%"
|}
|}
|}
|}
</font><br>
</font>
<br>
But these initial formulas are purely definitional, and help us little in understanding either the purpose of the operators or the meaning of their results. Working symbolically, let us apply the same method to the separate components ''f'' and ''g'' that we earlier used on ''J''. This work is recorded in Appendix 1 and a summary of the results is presented in Tables 66-i and 66-ii.
But these initial formulas are purely definitional, and help us little in understanding either the purpose of the operators or the meaning of their results. Working symbolically, let us apply the same method to the separate components <math>f\!</math> and <math>g\!</math> that we earlier used on <math>J.\!</math> This work is recorded in Appendix 1 and a summary of the results is presented in Tables 66-i and 66-ii.
<font face="courier new">
<font face="courier new">
|}
|}
|}
|}
</font><br>
</font>
<br>
<font face="courier new">
<font face="courier new">
|}
|}
|}
|}
</font><br>
</font>
<br>
Table 67 shows how to compute the analytic series for ''F'' = ‹''f'', ''g''› = ‹((''u'')(''v'')), ((''u'', ''v''))› in terms of coordinates, and Table 68 recaps these results in symbolic terms, agreeing with earlier derivations.
Table 67 shows how to compute the analytic series for <math>F = (f, g) = ~(~ \texttt{((} u \texttt{)(} v \texttt{))} ~,~ \texttt{((} u \texttt{,} v \texttt{))} ~)~\!</math> in terms of coordinates, and Table 68 recaps these results in symbolic terms, agreeing with earlier derivations.
{| align="center" border="1" cellpadding="0" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
{| align="center" border="1" cellpadding="0" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
|}
|}
|}
|}
<br>
<br>
|}
|}
|}
|}
<br>
<br>
Figure 69 gives a graphical picture of the difference map D''F'' = ‹D''f'', D''g''› for the transformation ''F'' = ‹''f'', ''g''› = ‹((''u'')(''v'')), ((''u'', ''v''))›. This depicts the same information about D''f'' and D''g'' that was given in the corresponding rows of the computation summary in Tables 66-i and 66-ii, excerpted here:
Figure 69 gives a graphical picture of the difference map <math>\mathrm{D}F = (\mathrm{D}f, \mathrm{D}g)\!</math> for the transformation <math>F = (f, g) = ~(~ \texttt{((} u \texttt{)(} v \texttt{))} ~,~ \texttt{((} u \texttt{,} v \texttt{))} ~)~.\!</math> This represents the same information about <math>\mathrm{D}f~\!</math> and <math>\mathrm{D}g~\!</math> that was given in the corresponding rows of Tables 66-i and 66-ii, for ease of reference repeated below.
<br><font face="courier new">
<br>
<font face="courier new">
{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
|
|
|}
|}
|}
|}
</font><br>
</font>
<br>
<br>
<p>[[Image:Diff Log Dyn Sys -- Figure 69 -- Difference Map (Short Form).gif|center]]</p>
<p>[[Image:Diff Log Dyn Sys -- Figure 69 -- Difference Map (Short Form).gif|center]]</p>
<p><center><font size="+1">'''Figure 69. Difference Map of F = ‹f, g› = ‹((u)(v)), ((u, v))›'''</font></center></p>
<p><center><font size="+1">'''Figure 69. Difference Map of F = ‹f, g› = ‹((u)(v)), ((u, v))›'''</font></center></p>
Figure 70-a shows a graphical way of picturing the tangent functor map d''F'' = ‹d''f'', d''g''› for the transformation ''F'' = ‹''f'', ''g''› = ›((u)(v)), ((u, v))›. This amounts to the same information about d''f'' and d''g'' that was given in the computation summary of Tables 66-i and 66-ii, the relevant rows of which are repeated here:
Figure 70-a shows a way of visualizing the tangent functor map <math>\mathrm{d}F = (\mathrm{d}f, \mathrm{d}g)\!</math> for the transformation <math>F = (f, g) = ~(~ \texttt{((} u \texttt{)(} v \texttt{))} ~,~ \texttt{((} u \texttt{,} v \texttt{))} ~)~.\!</math> This amounts to the same information about <math>\mathrm{d}f~\!</math> and <math>\mathrm{d}g~\!</math> that was given in Tables 66-i and 66-ii, the corresponding rows of which are repeated below.
<br>
<font face="courier new">
{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
|
|
|}
|}
|}
|}
</font><br>
</font>
<br>
<br>
<p>[[Image:Diff Log Dyn Sys -- Figure 70-a -- Tangent Functor Diagram.gif|center]]</p>
<p>[[Image:Diff Log Dyn Sys -- Figure 70-a -- Tangent Functor Diagram.gif|center]]</p>
<p><center><font size="+1">'''Figure 70-a. Tangent Functor Diagram for F‹u, v› = ‹((u)(v)), ((u, v))›'''</font></center></p>
<p><center><font size="+1">'''Figure 70-a. Tangent Functor Diagram for F‹u, v› = ‹((u)(v)), ((u, v))›'''</font></center></p>
