Line 932: |
Line 932: |
| <br> | | <br> |
| | | |
− | <pre> | + | {| 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%" |
− | Rule 7 | + | | |
| + | {| 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~7}</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>p, q ~:~ X \to \underline\mathbb{B}</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{R7a.}</math> |
| + | | width="60%" style="border-top:1px solid black" | <math>p ~=~ q</math> |
| + | | width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R7a~:~R6a}</math> |
| + | |- style="height:20px" |
| + | | |
| + | | |
| + | | |
| + | | style="border-left:1px solid black; text-align:center" | <math>::\!</math> |
| + | |- style="height:60px" |
| + | | |
| + | | <math>\operatorname{R7b.}</math> |
| + | | <math>\overset{X}{\underset{x}{\forall}}~ (p(x) ~=~ q(x))</math> |
| + | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R7b~:~R6b}</math> |
| + | |- style="height:20px" |
| + | | |
| + | | |
| + | | |
| + | | style="border-left:1px solid black; text-align:center" | <math>::\!</math> |
| + | |- style="height:60px" |
| + | | |
| + | | <math>\operatorname{R7c.}</math> |
| + | | <math>\operatorname{Conj_x^X}~ (p(x) ~=~ q(x))</math> |
| + | | style="border-left:1px solid black; text-align:center" | |
| + | <p><math>\operatorname{R7c~:~R6c}</math></p> |
| + | <p><math>\operatorname{R7c~:~P1a}</math></p> |
| + | |- style="height:20px" |
| + | | |
| + | | |
| + | | |
| + | | style="border-left:1px solid black; text-align:center" | <math>::\!</math> |
| + | |- style="height:40px" |
| + | | |
| + | | <math>\operatorname{R7d.}</math> |
| + | | <math>\operatorname{Conj_x^X}~ (p(x) ~\Leftrightarrow~ q(x))</math> |
| + | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R7d~:~P1b}</math> |
| + | |- style="height:20px" |
| + | | |
| + | | |
| + | | |
| + | | style="border-left:1px solid black; text-align:center" | <math>::\!</math> |
| + | |- style="height:60px" |
| + | | |
| + | | <math>\operatorname{R7e.}</math> |
| + | | <math>\operatorname{Conj_x^X}~ \underline{((}~ p(x) ~,~ q(x) ~\underline{))}</math> |
| + | | style="border-left:1px solid black; text-align:center" | |
| + | <p><math>\operatorname{R7e~:~P1c}</math></p> |
| + | <p><math>\operatorname{R7e~:~$1a}</math></p> |
| + | |- style="height:20px" |
| + | | |
| + | | |
| + | | |
| + | | style="border-left:1px solid black; text-align:center" | <math>::\!</math> |
| + | |- style="height:40px" |
| + | | |
| + | | <math>\operatorname{R7f.}</math> |
| + | | <math>\operatorname{Conj_x^X}~ \underline{((}~ p ~,~ q ~\underline{))}^\$ (x)</math> |
| + | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R7f~:~$1b}</math> |
| + | |} |
| + | |} |
| | | |
− | If P, Q : U -> B,
| + | <br> |
− | | |
− | then the following are equivalent:
| |
− | | |
− | R7a. P = Q. :R6a
| |
− | ::
| |
− | R7b. P(u) = Q(u), for all u C U. :R6b
| |
− | ::
| |
− | R7c. ConjUu (P(u) = Q(u)). :R6c
| |
− | :P1a
| |
− | ::
| |
− | R7d. ConjUu (P(u) <=> Q(u)). :P1b
| |
− | ::
| |
− | R7e. ConjUu (( P(u) , Q(u) )). :P1c
| |
− | :$1a
| |
− | ::
| |
− | R7f. ConjUu (( P , Q ))$(u). :$1b
| |
− | </pre>
| |
| | | |
− | <br> | + | '''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> | | <pre> |