12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Sunday October 06, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Syntactic Transformations (view source)
Revision as of 14:24, 3 February 2009
, 14:24, 3 February 2009→Syntactic Transformation Rules: format rule box
'''Editing Note.''' Check earlier and later drafts to see where <math>\text{P1a, P1b, P1c}~</math> came from. Are these just placeholders for the Value or Evaluation Rules?
'''Editing Note.''' Check earlier and later drafts to see where <math>\text{P1a, P1b, P1c}~</math> came from. Are these just placeholders for the Value or Evaluation Rules?
<pre>
<br>
If S, T are sentences
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
|
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:40px; text-align:center"
| width="80%" |
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~8}</math>
|}
|-
|
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:40px"
| width="2%" style="border-top:1px solid black" |
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
| width="60%" style="border-top:1px solid black" | <math>s, t ~\text{are sentences about things in}~ X</math>
| width="20%" style="border-top:1px solid black; border-left:1px solid black" |
|- style="height:40px"
|
| <math>\text{then}\!</math>
| <math>\text{the following are equivalent:}\!</math>
| style="border-left:1px solid black" |
|}
|-
|
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:40px"
| width="2%" style="border-top:1px solid black" |
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R8a.}</math>
| width="60%" style="border-top:1px solid black" | <math>s ~\Leftrightarrow~ t</math>
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" |
<math>\operatorname{R8a~:~D7a}</math>
|- style="height:20px"
|
|
|
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
|- style="height:60px"
|
| <math>\operatorname{R8b.}</math>
| <math>\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright</math>
| style="border-left:1px solid black; text-align:center" |
<p><math>\operatorname{R8b~:~D7b}</math></p>
<p><math>\operatorname{R8b~:~R7a}</math></p>
|- style="height:20px"
|
|
|
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
|- style="height:60px"
|
| <math>\operatorname{R8c.}</math>
| <math>\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))</math>
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8c~:~R7b}</math>
|- style="height:20px"
|
|
|
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
|- style="height:40px"
|
| <math>\operatorname{R8d.}</math>
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))</math>
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8d~:~R7c}</math>
|- style="height:20px"
|
|
|
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
|- style="height:40px"
|
| <math>\operatorname{R8e.}</math>
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft t \downharpoonright (x))</math>
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8e~:~R7d}</math>
|- style="height:20px"
|
|
|
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
|- style="height:60px"
|
| <math>\operatorname{R8f.}</math>
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright (x) ~,~ \downharpoonleft t \downharpoonright (x) ~\underline{))}</math>
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8f~:~R7e}</math>
|- style="height:20px"
|
|
|
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
|- style="height:40px"
|
| <math>\operatorname{R8g.}</math>
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright ~\underline{))}^\$ (x)</math>
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8g~:~R7f}</math>
|}
|}
<br>
For instance, the observation that expresses the equality of sets in terms of their indicator functions can be formalized according to the pattern in Rule 9, namely, at lines R9a, R9b, and R9c, and these components of Rule 9 can be cited in future uses by their indices in this list. Using Rule 7, annotated as R7, to adduce a few properties of indicator functions to the account, it is possible to extend Rule 9 by another few steps, referenced as R9d, R9e, R9f, and R9g.
For instance, the observation that expresses the equality of sets in terms of their indicator functions can be formalized according to the pattern in Rule 9, namely, at lines (a, b, c), and these components of Rule 9 can be cited in future uses as "R9a", "R9b", "R9c", respectively. Using Rule 7, annotated as "R7", to adduce a few properties of indicator functions to the account, it is possible to extend Rule 9 by another few steps, referenced as "R9d", "R9e", "R9f", "R9g".
<br>
<br>
