| Line 666: |
Line 666: |
| | {| align="center" cellpadding="6" width="90%" | | {| align="center" cellpadding="6" width="90%" |
| | | | | | |
| − | <math>\begin{array}{cccl} | + | <math>\begin{array}{lccl} |
| | \text{Let} & | | \text{Let} & |
| | X | | X |
| Line 683: |
Line 683: |
| | \\[6pt] | | \\[6pt] |
| | & | | & |
| − | & = & X_1 \times \ldots \times X_k ~\times~ \operatorname{d}X_1 \times \ldots \times \operatorname{d}X_k. | + | & = & X_1 \times \ldots \times X_k ~\times~ \operatorname{d}X_1 \times \ldots \times \operatorname{d}X_k |
| | \end{array}</math> | | \end{array}</math> |
| | |} | | |} |
| | | | |
| − | <pre>
| + | For a proposition of the form <math>f : X_1 \times \ldots \times X_k \to \mathbb{B},</math> the ''(first order) enlargement'' of <math>f\!</math> is the proposition <math>\operatorname{E}f : \operatorname{E}X \to \mathbb{B}</math> that is defined by the following equation: |
| − | For a proposition f : X_1 x ... x X_k -> B, | |
| − | the (first order) "enlargement" of f is the | |
| − | proposition Ef : EX -> B that is defined by: | |
| | | | |
| − | Ef<x_1, ..., x_k, dx_1, ..., dx_k>
| + | {| align="center" cellpadding="6" width="90%" |
| − | | + | | |
| − | = f<x_1 + dx_1, ..., x_k + dx_k>
| + | <math>\begin{array}{l} |
| − | | + | \operatorname{E}f(x_1, \ldots, x_k, \operatorname{d}x_1, \ldots, \operatorname{d}x_k) |
| − | = f<(x_1, dx_1), ..., (x_k, dx_k)>
| + | \\[6pt] |
| | + | = \quad f(x_1 + \operatorname{d}x_1, \ldots, x_k + \operatorname{d}x_k) |
| | + | \\[6pt] |
| | + | = \quad f( \texttt{(} x_1, \operatorname{d}x_1 \texttt{)}, \ldots, \texttt{(} x_k, \operatorname{d}x_k \texttt{)} ) |
| | + | \end{array}</math> |
| | + | |} |
| | | | |
| | + | <pre> |
| | It should be noted that the so-called "differential variables" dx_j | | It should be noted that the so-called "differential variables" dx_j |
| | are really just the same type of boolean variables as the other x_j. | | are really just the same type of boolean variables as the other x_j. |