12,080
edits
Changes
Directory:Jon Awbrey/Papers/Cactus Language (view source)
Revision as of 21:04, 25 January 2009
, 21:04, 25 January 2009→Syntactic Transformations: math markup + typo fix
| 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" |
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>
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" |
|}
<br>
<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.