Line 2,637: |
Line 2,637: |
| | style="border-right:1px solid black; border-top:1px solid black" | | | | style="border-right:1px solid black; border-top:1px solid black" | |
| |- | | |- |
− | | style="border-left:1px solid black" | <math>\text{R2a.}\!</math> | + | | style="border-left:1px solid black" | <math>\text{R1b.}\!</math> |
| | <math>\upharpoonleft Q \upharpoonright (x)</math> | | | <math>\upharpoonleft Q \upharpoonright (x)</math> |
| | style="border-right:1px solid black" | | | | style="border-right:1px solid black" | |
Line 2,654: |
Line 2,654: |
| 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. | | 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> | + | <br> |
− | Rule 2
| |
| | | |
− | If f : U -> B | + | {| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black; border-bottom:1px solid black" width="90%" |
| + | |- |
| + | | align="left" style="border-left:1px solid black" width="20%" | |
| + | | align="left" width="60%" | |
| + | | align="right" style="border-right:1px solid black" width="20%" | <math>\text{Rule 2}\!</math> |
| + | |- |
| + | | style="border-left:1px solid black; border-top:1px solid black" | <math>\text{If}\!</math> |
| + | | style="border-top:1px solid black" | <math>f : X \to \underline\mathbb{B}</math> |
| + | | style="border-right:1px solid black; border-top:1px solid black" | |
| + | |- |
| + | | style="border-left:1px solid black" | <math>\text{and}\!</math> |
| + | | <math>x \in X</math> |
| + | | style="border-right:1px solid black" | |
| + | |- |
| + | | style="border-left:1px solid black" | <math>\text{then}\!</math> |
| + | | <math>\text{the following are equivalent:}\!</math> |
| + | | style="border-right:1px solid black" | |
| + | |- |
| + | | style="border-left:1px solid black; border-top:1px solid black" | <math>\text{R2a.}\!</math> |
| + | | style="border-top:1px solid black" | <math>f(x)\!</math> |
| + | | style="border-right:1px solid black; border-top:1px solid black" | |
| + | |- |
| + | | style="border-left:1px solid black" | <math>\text{R2b.}\!</math> |
| + | | <math>f(x) = \underline{1}</math> |
| + | | style="border-right:1px solid black" | |
| + | |} |
| | | |
− | and u C U,
| + | <br> |
− | | |
− | then the following are equivalent:
| |
− | | |
− | R2a. f(u).
| |
− | | |
− | R2b. f(u) = 1.
| |
| | | |
| + | <pre> |
| 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. |
| | | |