Line 2,481: |
Line 2,481: |
| ==Note 10== | | ==Note 10== |
| | | |
− | <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 need 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 need 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 | |
− | relevance to differential logic in a strikingly apt and useful way. | |
− | The data for that account is contained in Table 9-a, above or here: | |
| | | |
− | DAL 9. http://forum.wolframscience.com/showthread.php?postid=1301#post1301
| + | <br> |
− | DAL 9. http://stderr.org/pipermail/inquiry/2004-May/001408.html
| |
| | | |
− | The shift operator E can be understood as enacting
| + | {| align="center" border="1" cellpadding="8" cellspacing="0" style="background:#f8f8ff; text-align:center; width:90%" |
− | a substitution operation on the proposition f that
| + | |+ <math>\text{Table A3.}~~\operatorname{E}f ~\text{Expanded Over Differential Features}~ \{ \operatorname{d}p, \operatorname{d}q \}</math> |
− | is given as its argument. In our present focus on
| + | |- style="background:#f0f0ff" |
− | propositional forms that involve two variables, we
| + | | width="10%" | |
− | have the following datatype and applied definition:
| + | | width="18%" | <math>f\!</math> |
| + | | width="18%" | |
| + | <p><math>\operatorname{T}_{11} f</math></p> |
| + | <p><math>\operatorname{E}f|_{\operatorname{d}p~\operatorname{d}q}</math></p> |
| + | | width="18%" | |
| + | <p><math>\operatorname{T}_{10} f</math></p> |
| + | <p><math>\operatorname{E}f|_{\operatorname{d}p(\operatorname{d}q)}</math></p> |
| + | | width="18%" | |
| + | <p><math>\operatorname{T}_{01} f</math></p> |
| + | <p><math>\operatorname{E}f|_{(\operatorname{d}p)\operatorname{d}q}</math></p> |
| + | | width="18%" | |
| + | <p><math>\operatorname{T}_{00} f</math></p> |
| + | <p><math>\operatorname{E}f|_{(\operatorname{d}p)(\operatorname{d}q)}</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} |
| + | (p)(q) |
| + | \\[4pt] |
| + | (p)~q~ |
| + | \\[4pt] |
| + | ~p~(q) |
| + | \\[4pt] |
| + | ~p~~q~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~p~~q~ |
| + | \\[4pt] |
| + | ~p~(q) |
| + | \\[4pt] |
| + | (p)~q~ |
| + | \\[4pt] |
| + | (p)(q) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~p~(q) |
| + | \\[4pt] |
| + | ~p~~q~ |
| + | \\[4pt] |
| + | (p)(q) |
| + | \\[4pt] |
| + | (p)~q~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (p)~q~ |
| + | \\[4pt] |
| + | (p)(q) |
| + | \\[4pt] |
| + | ~p~~q~ |
| + | \\[4pt] |
| + | ~p~(q) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (p)(q) |
| + | \\[4pt] |
| + | (p)~q~ |
| + | \\[4pt] |
| + | ~p~(q) |
| + | \\[4pt] |
| + | ~p~~q~ |
| + | \end{matrix}</math> |
| + | |- |
| + | | |
| + | <math>\begin{matrix} |
| + | f_3 |
| + | \\[4pt] |
| + | f_{12} |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (p) |
| + | \\[4pt] |
| + | ~p~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~p~ |
| + | \\[4pt] |
| + | (p) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~p~ |
| + | \\[4pt] |
| + | (p) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (p) |
| + | \\[4pt] |
| + | ~p~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (p) |
| + | \\[4pt] |
| + | ~p~ |
| + | \end{matrix}</math> |
| + | |- |
| + | | |
| + | <math>\begin{matrix} |
| + | f_6 |
| + | \\[4pt] |
| + | f_9 |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~(p,~q)~ |
| + | \\[4pt] |
| + | ((p,~q)) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~(p,~q)~ |
| + | \\[4pt] |
| + | ((p,~q)) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ((p,~q)) |
| + | \\[4pt] |
| + | ~(p,~q)~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ((p,~q)) |
| + | \\[4pt] |
| + | ~(p,~q)~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~(p,~q)~ |
| + | \\[4pt] |
| + | ((p,~q)) |
| + | \end{matrix}</math> |
| + | |- |
| + | | |
| + | <math>\begin{matrix} |
| + | f_5 |
| + | \\[4pt] |
| + | f_{10} |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (q) |
| + | \\[4pt] |
| + | ~q~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~q~ |
| + | \\[4pt] |
| + | (q) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (q) |
| + | \\[4pt] |
| + | ~q~ |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ~q~ |
| + | \\[4pt] |
| + | (q) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (q) |
| + | \\[4pt] |
| + | ~q~ |
| + | \end{matrix}</math> |
| + | |- |
| + | | |
| + | <math>\begin{matrix} |
| + | f_7 |
| + | \\[4pt] |
| + | f_{11} |
| + | \\[4pt] |
| + | f_{13} |
| + | \\[4pt] |
| + | f_{14} |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (~p~~q~) |
| + | \\[4pt] |
| + | (~p~(q)) |
| + | \\[4pt] |
| + | ((p)~q~) |
| + | \\[4pt] |
| + | ((p)(q)) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ((p)(q)) |
| + | \\[4pt] |
| + | ((p)~q~) |
| + | \\[4pt] |
| + | (~p~(q)) |
| + | \\[4pt] |
| + | (~p~~q~) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | ((p)~q~) |
| + | \\[4pt] |
| + | ((p)(q)) |
| + | \\[4pt] |
| + | (~p~~q~) |
| + | \\[4pt] |
| + | (~p~(q)) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (~p~(q)) |
| + | \\[4pt] |
| + | (~p~~q~) |
| + | \\[4pt] |
| + | ((p)(q)) |
| + | \\[4pt] |
| + | ((p)~q~) |
| + | \end{matrix}</math> |
| + | | |
| + | <math>\begin{matrix} |
| + | (~p~~q~) |
| + | \\[4pt] |
| + | (~p~(q)) |
| + | \\[4pt] |
| + | ((p)~q~) |
| + | \\[4pt] |
| + | ((p)(q)) |
| + | \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> |
| + | |} |
| | | |
− | E : (X -> B) -> (EX -> B)
| + | <br> |
| | | |
− | E : f<p, q> -> Ef<p, q, dp, dq>
| + | The shift operator <math>\operatorname{E}</math> can be understood as enacting a ''substitution operation'' on the proposition that is given as its argument. |
| | | |
− | Ef<p, q, dp, dq>
| + | The shift operator <math>\operatorname{E}</math> can be understood as enacting a substitution operation on the propositional form <math>f(p, q)\!</math> that is given as its argument. In our present focus on propositional forms that involve two variables, we have the following type specifications and definitions: |
| | | |
− | = f<p + dp, q + dq)
| + | {| align="center" cellpadding="6" width="90%" |
− | | + | | |
− | = f<(p, dp), (q, dq)>
| + | <math>\begin{array}{lcl} |
| + | \operatorname{E} ~:~ (X \to \mathbb{B}) |
| + | & \to & |
| + | (\operatorname{E}X \to \mathbb{B}) |
| + | \\[6pt] |
| + | \operatorname{E} ~:~ f(p, q) |
| + | & \mapsto & |
| + | \operatorname{E}f(p, q, \operatorname{d}p, \operatorname{d}q) |
| + | \\[6pt] |
| + | \operatorname{E}f(p, q, \operatorname{d}p, \operatorname{d}q) |
| + | & = & |
| + | f(p + \operatorname{d}p, q + \operatorname{d}q) |
| + | \\[6pt] |
| + | & = & |
| + | f( \texttt{(} p, \operatorname{d}p \texttt{)}, \texttt{(} q, \operatorname{d}q \texttt{)} ) |
| + | \end{array}</math> |
| + | |} |
| | | |
| + | <pre> |
| Therefore, if we evaluate Ef at particular values of dp and dq, | | Therefore, if we evaluate Ef at particular values of dp and dq, |
| for example, dp = i and dq = j, where i, j are in B, we obtain: | | for example, dp = i and dq = j, where i, j are in B, we obtain: |