Line 6,294: |
Line 6,294: |
| | | | | |
| <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> |
| |} | | |} |
Line 6,769: |
Line 6,769: |
| 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: | | 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"> |
| {| 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%" |
| | | | | |
Line 6,778: |
Line 6,780: |
| |} | | |} |
| |} | | |} |
− | </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: | | 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"> |
| {| 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%" |
| | | | | |
Line 6,799: |
Line 6,805: |
| |} | | |} |
| |} | | |} |
− | </font><br> | + | </font> |
| + | |
| + | <br> |
| | | |
| 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. | | 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. |
Line 6,805: |
Line 6,813: |
| 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. | | 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. | + | 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> | | <br> |
Line 6,848: |
Line 6,856: |
| | | |
| 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. | | 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. |
| + | |
| + | <br> |
| | | |
| <font face="courier new"> | | <font face="courier new"> |
Line 6,929: |
Line 6,939: |
| <br> | | <br> |
| | | |
− | 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. | + | 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. |
| + | |
| + | <br> |
| | | |
| {| 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%" |
Line 7,359: |
Line 7,371: |
| <br> | | <br> |
| | | |
− | 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. | + | 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> | | <br> |
Line 7,390: |
Line 7,402: |
| <br> | | <br> |
| | | |
− | <p>[[Image:Diff Log Dyn Sys -- Figure 69 -- Difference Map (Short Form).gif|center]]</p>
| + | {| align="center" border="0" cellspacing="10" style="text-align:center; width:100%" |
− | <p><center><font size="+1">'''Figure 69. Difference Map of F = ‹f, g› = ‹((u)(v)), ((u, v))›'''</font></center></p>
| + | | [[Image:Diff Log Dyn Sys -- Figure 69 -- Difference Map (Short Form).gif|center]] |
| + | |- |
| + | | height="20px" valign="top" | <math>\text{Figure 69.} ~~ \text{Difference Map of}~ F(u, v) = (\; \texttt{((} u \texttt{)(} v \texttt{))} \;,\; \texttt{((} u \texttt{,} v \texttt{))} \;)</math> |
| + | |} |
| + | |
| + | <br> |
| | | |
− | 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. | + | 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> | | <br> |
Line 7,427: |
Line 7,444: |
| <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> |
| | | |
− | Figure 70-b shows another way to picture the action of the tangent functor on the logical transformation ''F''‹''u'', ''v''› = ‹((''u'')(''v'')), ((''u'', ''v''))›, roughly in the style of the ''bundle of universes'' type of diagram. | + | Figure 70-b shows another way to picture the action of the tangent functor on the logical transformation <math>F(u, v) = (\; \texttt{((} u \texttt{)(} v \texttt{))} \;,\; \texttt{((} u \texttt{,} v \texttt{))} \;).\!</math> |
| + | |
| + | <br> |
| | | |
− | <p>[[Image:Diff Log Dyn Sys -- Figure 70-b -- Tangent Functor Diagram.gif|center|frame|<font size="3">'''Figure 70-b. Tangent Functor Ferris Wheel for F‹u, v› = ‹((u)(v)), ((u, v))›'''</font>]]</p>
| + | {| align="center" border="0" cellspacing="10" style="text-align:center; width:100%" |
| + | | [[Image:Diff Log Dyn Sys -- Figure 70-b -- Tangent Functor Diagram.gif|center]] |
| + | |- |
| + | | height="20px" valign="top" | <math>\text{Figure 70-b.} ~~ \text{Tangent Functor Ferris Wheel for}~ F(u, v) = (\; \texttt{((} u \texttt{)(} v \texttt{))} \;,\; \texttt{((} u \texttt{,} v \texttt{))} \;)</math> |
| + | |} |
| + | |
| + | <br> |
| | | |
− | * '''Nota Bene.''' The original Figure 70-b lost some of its labeling in a succession of platform metamorphoses over the years, so I have included an Ascii version below to indicate where the missing labels go. | + | * '''Note.''' The original Figure 70-b lost some of its labeling in a succession of platform metamorphoses over the years, so we have included an ASCII version below to indicate where the missing labels go. |
| | | |
| {| align="center" border="0" cellpadding="10" | | {| align="center" border="0" cellpadding="10" |