Line 252: |
Line 252: |
| Then interpret the usual propositions about <math>p, q\!</math> as functions of the concrete type <math>f : P \times Q \to \mathbb{B}.</math> | | Then interpret the usual propositions about <math>p, q\!</math> as functions of the concrete type <math>f : P \times Q \to \mathbb{B}.</math> |
| | | |
− | <pre>
| + | We are going to consider various ''operators'' on these functions. Here, an operator <math>\operatorname{F}</math> is a function that takes one function <math>f\!</math> into another function <math>\operatorname{F}f.</math> |
− | We are going to consider various "operators" on these functions. | |
− | Here, an operator W is a function that takes one function f into | |
− | another function Wf. | |
| | | |
− | The first couple of operators that we need to consider are | + | The first couple of operators that we need to consider are logical analogues of the pair that play a founding role in the classical finite difference calculus, namely: |
− | logical analogues of the pair that play a founding role | |
− | in the classical "finite difference calculus", namely: | |
| | | |
− | The "difference" operator [capital Delta], written here as D.
| + | {| align="center" cellpadding="6" width="90%" |
| + | | The ''difference operator'' <math>\Delta,\!</math> written here as <math>\operatorname{D}.</math> |
| + | |- |
| + | | The ''enlargement" operator'' <math>\Epsilon,\!</math> written here as <math>\operatorname{E}.</math> |
| + | |} |
| | | |
− | The "enlargement" operator [capital Epsilon], written here as E.
| + | These days, <math>\operatorname{E}</math> is more often called the ''shift operator''. |
| | | |
− | These days, E is more often called the "shift" operator.
| + | In order to describe the universe in which these operators operate, it is necessary to enlarge the original universe of discourse. Starting from the initial space <math>X = P \times Q,</math> its ''(first order) differential extension'' <math>\operatorname{E}X</math> is constructed according to the following specifications: |
| | | |
− | In order to describe the universe in which these operators operate,
| + | {| align="center" cellpadding="6" width="90%" |
− | it will be necessary to enlarge our original universe of discourse.
| + | | |
| + | <math>\begin{array}{rcc} |
| + | \operatorname{E}X & = & X \times \operatorname{d}X |
| + | \end{array}</math> |
| + | |} |
| | | |
− | Starting out from the initial space X = !P! x !Q!, we
| + | where: |
− | construct its (first order) "differential extension":
| |
| | | |
− | EX = X x dX = !P! x !Q! x d!P! x d!Q!
| + | {| align="center" cellpadding="6" width="90%" |
− | | + | | |
− | where:
| + | <math>\begin{array}{rcc} |
− | | + | X |
− | X = !P! x !Q!
| + | & = & |
− | | + | P \times Q |
− | dX = d!P! x d!Q!
| + | \\[4pt] |
− | | + | \operatorname{d}X |
− | d!P! = {(dp), dp}
| + | & = & |
− | | + | \operatorname{d}P \times \operatorname{d}Q |
− | d!Q! = {(dq), dq}
| + | \\[4pt] |
| + | \operatorname{d}P |
| + | & = & |
| + | \{ \texttt{(} \operatorname{d}p \texttt{)},~ \operatorname{d}p \} |
| + | \\[4pt] |
| + | \operatorname{d}Q |
| + | & = & |
| + | \{ \texttt{(} \operatorname{d}q \texttt{)},~ \operatorname{d}q \} |
| + | \end{array}</math> |
| + | |} |
| | | |
| + | <pre> |
| The interpretations of these new symbols can be diverse, | | The interpretations of these new symbols can be diverse, |
| but the easiest interpretation for now is just to say | | but the easiest interpretation for now is just to say |