Line 2,646: |
Line 2,646: |
| Conversely, any rule of this sort, properly qualified by the conditions under which it applies, can be turned back into a summary statement of the logical equivalence that is involved in its application. This mode of conversion a static principle and a transformational rule, that is, between a statement of equivalence and an equivalence of statements, is so automatic that it is usually not necessary to make a separate note of the "horizontal" versus the "vertical" versions. | | Conversely, any rule of this sort, properly qualified by the conditions under which it applies, can be turned back into a summary statement of the logical equivalence that is involved in its application. This mode of conversion a static principle and a transformational rule, that is, between a statement of equivalence and an equivalence of statements, is so automatic that it is usually not necessary to make a separate note of the "horizontal" versus the "vertical" versions. |
| | | |
− | <pre>
| + | As another example of a STR, consider the following logical equivalence, that holds for any <math>Q \subseteq X</math> and for all <math>x \in X.</math> |
− | As another example of a STR, consider the following logical equivalence, that holds for any X c U and for all u C U: | |
| | | |
− | {X}(u) <=> {X}(u) = 1. | + | {| align="center" cellpadding="8" width="90%" |
| + | | <math>\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x) = \underline{1}.</math> |
| + | |} |
| | | |
− | In practice, this logical equivalence is used to exchange an expression of the form "{X}(u)" with a sentence of the form "{X}(u) = 1" in any context where one has a relatively fixed X c U in mind and where one is conceiving u C U to vary over its whole domain, namely, the universe U. This leads to the STR that is given in Rule 2. | + | In practice, this logical equivalence is used to exchange an expression of the form <math>\upharpoonleft Q \upharpoonright (x)</math> with a sentence of the form <math>\upharpoonleft Q \upharpoonright (x) = \underline{1}</math> in any context where one has a relatively fixed <math>Q \subseteq X</math> in mind and where one is conceiving <math>x \in X</math> to vary over its whole domain, namely, the universe <math>X.\!</math> This leads to the STR that is given in Rule 2. |
| | | |
| + | <pre> |
| Rule 2 | | Rule 2 |
| | | |
− | If f : U �> B | + | If f : U -> B |
| | | |
| and u C U, | | and u C U, |
Line 2,665: |
Line 2,667: |
| R2b. f(u) = 1. | | R2b. f(u) = 1. |
| | | |
− | Rules like these can be chained together to establish extended rules, just so long as their antecedent conditions are compatible. For example, Rules 1 and 2 combine to give the equivalents that are listed in Rule 3. This follows from a recognition that the function {X} : U �> B that is introduced in Rule 1 is an instance of the function f : U �> B that is mentioned in Rule 2. By the time one arrives in the "consequence box" of either Rule, then, one has in mind a comparatively fixed X c U, a proposition f or {X} about things in U, and a variable argument u C U. | + | Rules like these can be chained together to establish extended rules, just so long as their antecedent conditions are compatible. For example, Rules 1 and 2 combine to give the equivalents that are listed in Rule 3. This follows from a recognition that the function {X} : U -> B that is introduced in Rule 1 is an instance of the function f : U -> B that is mentioned in Rule 2. By the time one arrives in the "consequence box" of either Rule, then, one has in mind a comparatively fixed X c U, a proposition f or {X} about things in U, and a variable argument u C U. |
| | | |
| Rule 3 | | Rule 3 |