Line 352: |
Line 352: |
| |} | | |} |
| | | |
− | <pre>
| + | Given the proposition <math>f(p, q)\!</math> over <math>X = P \times Q,</math> the ''(first order) difference'' of <math>f\!</math> is the proposition <math>\operatorname{D}f</math> over <math>\operatorname{E}X</math> that is defined by the formula <math>\operatorname{D}f = \operatorname{E}f - f,</math> or, written out in full: |
− | Given the proposition f<p, q> over X = !P! x !Q!, the | |
− | (first order) "difference" of f is the proposition Df | |
− | over EX that is defined by the formula Df = Ef - f, or, | |
− | written out in full: | |
| | | |
− | Df<p, q, dp, dq>
| + | {| align="center" cellpadding="6" width="90%" |
| + | | align="center" | |
| + | <math>\begin{matrix} |
| + | \operatorname{D}f(p, q, \operatorname{d}p, \operatorname{d}q) |
| + | & = & |
| + | f(p + \operatorname{d}p,~ q + \operatorname{d}q) - f(p, q) |
| + | & = & |
| + | \texttt{(} f( \texttt{(} p, \operatorname{d}p \texttt{)},~ \texttt{(} q, \operatorname{d}q \texttt{)} ),~ f(p, q) \texttt{)} |
| + | \end{matrix}</math> |
| + | |} |
| | | |
− | = f<p + dp, q + dq> - f<p, q>
| + | In the example <math>f(p, q) = pq,\!</math> the difference <math>\operatorname{D}f</math> is computed as follows: |
− | | |
− | = (f<(p, dp), (q, dq)>, f<p, q>)
| |
− | | |
− | In the example f<p, q> = pq, the difference Df is given by:
| |
− | | |
− | Df<p, q, dp, dq>
| |
− | | |
− | = [p + dp][q + dq] - pq
| |
− | | |
− | = ((p, dp)(q, dq), pq)
| |
| | | |
| + | {| align="center" cellpadding="6" width="90%" |
| + | | align="center" | |
| + | <math>\begin{matrix} |
| + | \operatorname{D}f(p, q, \operatorname{d}p, \operatorname{d}q) |
| + | & = & |
| + | (p + \operatorname{d}p)(q + \operatorname{d}q) - pq |
| + | & = & |
| + | \texttt{((} p, \operatorname{d}p \texttt{)(} q, \operatorname{d}q \texttt{)}, pq \texttt{)} |
| + | \end{matrix}</math> |
| + | |- |
| + | | align="center" | |
| + | <pre> |
| o-------------------------------------------------o | | o-------------------------------------------------o |
| | | | | | | |
Line 391: |
Line 398: |
| | Df = ((p, dp)(q, dq), pq) | | | | Df = ((p, dp)(q, dq), pq) | |
| o-------------------------------------------------o | | o-------------------------------------------------o |
| + | </pre> |
| + | |} |
| | | |
| + | <pre> |
| We did not yet go through the trouble to interpret this (first order) | | We did not yet go through the trouble to interpret this (first order) |
| "difference of conjunction" fully, but were happy simply to evaluate | | "difference of conjunction" fully, but were happy simply to evaluate |