Line 5,465: |
Line 5,465: |
| ====Note 7==== | | ====Note 7==== |
| | | |
− | <pre>
| + | If you think that I linger in the realm of logical difference calculus out of sheer vacillation about getting down to the differential proper, it is probably out of a prior expectation that you derive from the art or the long-engrained practice of real analysis. But the fact is that ordinary calculus only rushes on to the sundry orders of approximation because the strain of comprehending the full import of <math>\operatorname{E}</math> and <math>\operatorname{D}</math> at once whelm over its discrete and finite powers to grasp them. But here, in the fully serene idylls of ZOL, we find ourselves fit with the compass of a wit that is all we'd ever wish to explore their effects with care. |
− | If you think that I linger in the realm of logical difference calculus | |
− | out of sheer vacillation about getting down to the differential proper, | |
− | it is probably out of a prior expectation that you derive from the art | |
− | or the long-engrained practice of real analysis. But the fact is that | |
− | ordinary calculus only rushes on to the sundry orders of approximation | |
− | because the strain of comprehending the full import of E and D at once | |
− | whelm over its discrete and finite powers to grasp them. But here, in | |
− | the fully serene idylls of ZOL, we find ourselves fit with the compass | |
− | of a wit that is all we'd ever wish to explore their effects with care. | |
| | | |
| So let us do just that. | | So let us do just that. |
| | | |
− | I will first rationalize the novel grouping of propositional forms | + | I will first rationalize the novel grouping of propositional forms in the last set of Tables, as that will extend a gentle invitation to the mathematical subject of ''group theory'', and demonstrate its relevance to differential logic in a strikingly apt and useful way. The data for that account is contained in Table A3. |
− | in the last set of Tables, as that will extend a gentle invitation | + | |
− | to the mathematical subject of "group theory", and demonstrate its | + | <br> |
− | relevance to differential logic in a strikingly apt and useful way. | + | |
− | The data for that account is contained in Table 3. | + | {| align="center" border="1" cellpadding="8" cellspacing="0" style="background:#f8f8ff; text-align:center; width:90%" |
| + | |+ <math>\text{Table A3.}~~\operatorname{E}f ~\text{Expanded Over Differential Features}~ \{ \operatorname{d}x, \operatorname{d}y \}</math> |
| + | |- style="background:#f0f0ff" |
| + | | width="10%" | |
| + | | width="18%" | <math>f\!</math> |
| + | | width="18%" | |
| + | <p><math>\operatorname{T}_{11} f</math></p> |
| + | <p><math>\operatorname{E}f|_{\operatorname{d}x~\operatorname{d}y}</math></p> |
| + | | width="18%" | |
| + | <p><math>\operatorname{T}_{10} f</math></p> |
| + | <p><math>\operatorname{E}f|_{\operatorname{d}x(\operatorname{d}y)}</math></p> |
| + | | width="18%" | |
| + | <p><math>\operatorname{T}_{01} f</math></p> |
| + | <p><math>\operatorname{E}f|_{(\operatorname{d}x)\operatorname{d}y}</math></p> |
| + | | width="18%" | |
| + | <p><math>\operatorname{T}_{00} f</math></p> |
| + | <p><math>\operatorname{E}f|_{(\operatorname{d}x)(\operatorname{d}y)}</math></p> |
| + | |- |
| + | | <math>f_0\!</math> |
| + | | <math>(~)</math> |
| + | | <math>(~)</math> |
| + | | <math>(~)</math> |
| + | | <math>(~)</math> |
| + | | <math>(~)</math> |
| + | |- |
| + | | |
| + | <math>\begin{matrix} |
| + | f_1 |
| + | \\[4pt] |
| + | f_2 |
| + | \\[4pt] |
| + | f_4 |
| + | \\[4pt] |
| + | f_8 |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (x)(y) |
| + | \\[4pt] |
| + | (x)~y~ |
| + | \\[4pt] |
| + | ~x~(y) |
| + | \\[4pt] |
| + | ~x~~y~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~x~~y~ |
| + | \\[4pt] |
| + | ~x~(y) |
| + | \\[4pt] |
| + | (x)~y~ |
| + | \\[4pt] |
| + | (x)(y) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~x~(y) |
| + | \\[4pt] |
| + | ~x~~y~ |
| + | \\[4pt] |
| + | (x)(y) |
| + | \\[4pt] |
| + | (x)~y~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (x)~y~ |
| + | \\[4pt] |
| + | (x)(y) |
| + | \\[4pt] |
| + | ~x~~y~ |
| + | \\[4pt] |
| + | ~x~(y) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (x)(y) |
| + | \\[4pt] |
| + | (x)~y~ |
| + | \\[4pt] |
| + | ~x~(y) |
| + | \\[4pt] |
| + | ~x~~y~ |
| + | \end{matrix}</math> |
| + | |- |
| + | | |
| + | <math>\begin{matrix} |
| + | f_3 |
| + | \\[4pt] |
| + | f_{12} |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (x) |
| + | \\[4pt] |
| + | ~x~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~x~ |
| + | \\[4pt] |
| + | (x) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~x~ |
| + | \\[4pt] |
| + | (x) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (x) |
| + | \\[4pt] |
| + | ~x~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (x) |
| + | \\[4pt] |
| + | ~x~ |
| + | \end{matrix}</math> |
| + | |- |
| + | | |
| + | <math>\begin{matrix} |
| + | f_6 |
| + | \\[4pt] |
| + | f_9 |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~(x,~y)~ |
| + | \\[4pt] |
| + | ((x,~y)) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~(x,~y)~ |
| + | \\[4pt] |
| + | ((x,~y)) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ((x,~y)) |
| + | \\[4pt] |
| + | ~(x,~y)~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ((x,~y)) |
| + | \\[4pt] |
| + | ~(x,~y)~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~(x,~y)~ |
| + | \\[4pt] |
| + | ((x,~y)) |
| + | \end{matrix}</math> |
| + | |- |
| + | | |
| + | <math>\begin{matrix} |
| + | f_5 |
| + | \\[4pt] |
| + | f_{10} |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (y) |
| + | \\[4pt] |
| + | ~y~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~y~ |
| + | \\[4pt] |
| + | (y) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (y) |
| + | \\[4pt] |
| + | ~y~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~y~ |
| + | \\[4pt] |
| + | (y) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (y) |
| + | \\[4pt] |
| + | ~y~ |
| + | \end{matrix}</math> |
| + | |- |
| + | | |
| + | <math>\begin{matrix} |
| + | f_7 |
| + | \\[4pt] |
| + | f_{11} |
| + | \\[4pt] |
| + | f_{13} |
| + | \\[4pt] |
| + | f_{14} |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (~x~~y~) |
| + | \\[4pt] |
| + | (~x~(y)) |
| + | \\[4pt] |
| + | ((x)~y~) |
| + | \\[4pt] |
| + | ((x)(y)) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ((x)(y)) |
| + | \\[4pt] |
| + | ((x)~y~) |
| + | \\[4pt] |
| + | (~x~(y)) |
| + | \\[4pt] |
| + | (~x~~y~) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ((x)~y~) |
| + | \\[4pt] |
| + | ((x)(y)) |
| + | \\[4pt] |
| + | (~x~~y~) |
| + | \\[4pt] |
| + | (~x~(y)) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (~x~(y)) |
| + | \\[4pt] |
| + | (~x~~y~) |
| + | \\[4pt] |
| + | ((x)(y)) |
| + | \\[4pt] |
| + | ((x)~y~) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (~x~~y~) |
| + | \\[4pt] |
| + | (~x~(y)) |
| + | \\[4pt] |
| + | ((x)~y~) |
| + | \\[4pt] |
| + | ((x)(y)) |
| + | \end{matrix}</math> |
| + | |- |
| + | | <math>f_{15}\!</math> |
| + | | <math>((~))</math> |
| + | | <math>((~))</math> |
| + | | <math>((~))</math> |
| + | | <math>((~))</math> |
| + | | <math>((~))</math> |
| + | |- style="background:#f0f0ff" |
| + | | colspan="2" | <math>\text{Fixed Point Total}\!</math> |
| + | | <math>4\!</math> |
| + | | <math>4\!</math> |
| + | | <math>4\!</math> |
| + | | <math>16\!</math> |
| + | |} |
| | | |
− | Table 3. Ef Expanded Over Differential Features {dx, dy}
| + | <br> |
− | o------o------------o------------o------------o------------o------------o
| |
− | | | | | | | |
| |
− | | | f | T_11 f | T_10 f | T_01 f | T_00 f |
| |
− | | | | | | | |
| |
− | | | | Ef| dx·dy | Ef| dx(dy) | Ef| (dx)dy | Ef|(dx)(dy)|
| |
− | | | | | | | |
| |
− | o------o------------o------------o------------o------------o------------o
| |
− | | | | | | | |
| |
− | | f_0 | () | () | () | () | () |
| |
− | | | | | | | |
| |
− | o------o------------o------------o------------o------------o------------o
| |
− | | | | | | | |
| |
− | | f_1 | (x)(y) | x y | x (y) | (x) y | (x)(y) |
| |
− | | | | | | | |
| |
− | | f_2 | (x) y | x (y) | x y | (x)(y) | (x) y |
| |
− | | | | | | | |
| |
− | | f_4 | x (y) | (x) y | (x)(y) | x y | x (y) |
| |
− | | | | | | | |
| |
− | | f_8 | x y | (x)(y) | (x) y | x (y) | x y |
| |
− | | | | | | | |
| |
− | o------o------------o------------o------------o------------o------------o
| |
− | | | | | | | |
| |
− | | f_3 | (x) | x | x | (x) | (x) |
| |
− | | | | | | | |
| |
− | | f_12 | x | (x) | (x) | x | x |
| |
− | | | | | | | |
| |
− | o------o------------o------------o------------o------------o------------o
| |
− | | | | | | | |
| |
− | | f_6 | (x, y) | (x, y) | ((x, y)) | ((x, y)) | (x, y) |
| |
− | | | | | | | |
| |
− | | f_9 | ((x, y)) | ((x, y)) | (x, y) | (x, y) | ((x, y)) |
| |
− | | | | | | | |
| |
− | o------o------------o------------o------------o------------o------------o
| |
− | | | | | | | |
| |
− | | f_5 | (y) | y | (y) | y | (y) |
| |
− | | | | | | | |
| |
− | | f_10 | y | (y) | y | (y) | y |
| |
− | | | | | | | |
| |
− | o------o------------o------------o------------o------------o------------o
| |
− | | | | | | | |
| |
− | | f_7 | (x y) | ((x)(y)) | ((x) y) | (x (y)) | (x y) |
| |
− | | | | | | | |
| |
− | | f_11 | (x (y)) | ((x) y) | ((x)(y)) | (x y) | (x (y)) |
| |
− | | | | | | | |
| |
− | | f_13 | ((x) y) | (x (y)) | (x y) | ((x)(y)) | ((x) y) |
| |
− | | | | | | | |
| |
− | | f_14 | ((x)(y)) | (x y) | (x (y)) | ((x) y) | ((x)(y)) |
| |
− | | | | | | | |
| |
− | o------o------------o------------o------------o------------o------------o
| |
− | | | | | | | |
| |
− | | f_15 | (()) | (()) | (()) | (()) | (()) |
| |
− | | | | | | | |
| |
− | o------o------------o------------o------------o------------o------------o
| |
− | | | | | | |
| |
− | | Fixed Point Total | 4 | 4 | 4 | 16 |
| |
− | | | | | | |
| |
− | o-------------------o------------o------------o------------o------------o
| |
| | | |
| + | <pre> |
| The shift operator E can be understood as enacting a substitution operation | | The shift operator E can be understood as enacting a substitution operation |
| on the proposition that is given as its argument. In our immediate example, | | on the proposition that is given as its argument. In our immediate example, |