Changes

MyWikiBiz, Author Your Legacy — Tuesday April 30, 2024
Jump to navigationJump to search
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&nbsp;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%" | &nbsp;
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:
12,080

edits

Navigation menu