Changes

User:Jon Awbrey/SCRATCHPAD (view source)

Revision as of 03:08, 2 February 2009

436 bytes removed , 03:08, 2 February 2009

→‎Rule 9

Line 2,803: Line 2,803:

===Rule 9===

−

~~<pre>~~

−

~~Rule 9~~

−

~~If X, Y c U,~~

−

~~then the following are equivalent:~~

−

~~R9a. X = Y. :R5a~~

−

::

−

~~R9b. {X} = {Y}. :R5e~~

−

~~:R7a~~

−

::

−

~~R9c. {X}(u) = {Y}(u), for all u C U. :R7b~~

−

::

−

~~R9d. ConjUu ( {X}(u) = {Y}(u) ). :R7c~~

−

::

−

~~R9e. ConjUu ( {X}(u) <=> {Y}(u) ). :R7d~~

−

::

−

~~R9f. ConjUu (( {X}(u) , {Y}(u) )). :R7e~~

−

::

−

~~R9g. ConjUu (( {X} , {Y} ))$(u). :R7f~~

−

~~</pre>~~

Line 2,834: Line 2,811:

|- style="height:40px; text-align:center"

| width="80%" |  

−

| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~8}</math>

+

| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~9}</math>

|}

|-

Line 2,842: Line 2,819:

| 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="60%" style="border-top:1px solid black" | <math>P, Q ~\subseteq~ X</math>

| width="20%" style="border-top:1px solid black; border-left:1px solid black" |  

|- style="height:40px"

Line 2,855: Line 2,832:

|- style="height:40px"

| width="2%" style="border-top:1px solid black" |  

−

| width="18%" style="border-top:1px solid black" | <math>\operatorname{~~R8a~~.}</math>

+

| width="18%" style="border-top:1px solid black" | <math>\operatorname{R9a.}</math>

−

| width="60%" style="border-top:1px solid black" | <math>s ~~~\Leftrightarrow~~~ t</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" |

+

| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R9a~:~R5a}</math>

−

<math>\operatorname{~~R8a~~~:~~~D7a~~}</math>

|- style="height:20px"

|  

Line 2,866: Line 2,842:

|- style="height:60px"

|  

−

| <math>\operatorname{~~R8b~~.}</math>

+

| <math>\operatorname{R9b.}</math>

−

| <math>\~~downharpoonleft s~~ \~~downharpoonright~~ ~=~ \~~downharpoonleft t~~ \~~downharpoonright~~</math>

+

| <math>\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright</math>

| style="border-left:1px solid black; text-align:center" |

−

<math>\operatorname{~~R8b~~~:~~~D7b~~}</math>

+

<math>\operatorname{R9b~:~R5e}</math>

−

<math>\operatorname{~~R8b~~~:~R7a}</math>

+

<math>\operatorname{R9b~:~R7a}</math>

|- style="height:20px"

|  

Line 2,878: Line 2,854:

|- style="height:60px"

|  

−

| <math>\operatorname{~~R8c~~.}</math>

+

| <math>\operatorname{R9c.}</math>

−

| <math>\overset{X}{\underset{x}{\forall}}~ (\~~downharpoonleft s~~ \~~downharpoonright~~ (x) ~=~ \~~downharpoonleft t~~ \~~downharpoonright~~ (x))</math>

+

| <math>\overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>

−

| style="border-left:1px solid black; text-align:center" | <math>\operatorname{~~R8c~~~:~R7b}</math>

+

| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9c~:~R7b}</math>

|- style="height:20px"

|  

Line 2,888: Line 2,864:

|- style="height:40px"

|  

−

| <math>\operatorname{~~R8d~~.}</math>

+

| <math>\operatorname{R9d.}</math>

−

| <math>\operatorname{Conj_x^X}~ (\~~downharpoonleft s~~ \~~downharpoonright~~ (x) ~=~ \~~downharpoonleft t~~ \~~downharpoonright~~ (x))</math>

+

| <math>\operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>

−

| style="border-left:1px solid black; text-align:center" | <math>\operatorname{~~R8d~~~:~R7c}</math>

+

| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9d~:~R7c}</math>

|- style="height:20px"

|  

Line 2,898: Line 2,874:

|- style="height:40px"

|  

−

| <math>\operatorname{~~R8e~~.}</math>

+

| <math>\operatorname{R9e.}</math>

−

| <math>\operatorname{Conj_x^X}~ (\~~downharpoonleft s~~ \~~downharpoonright~~ (x) ~\Leftrightarrow~ \~~downharpoonleft t~~ \~~downharpoonright~~ (x))</math>

+

| <math>\operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x))</math>

−

| style="border-left:1px solid black; text-align:center" | <math>\operatorname{~~R8e~~~:~R7d}</math>

+

| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9e~:~R7d}</math>

|- style="height:20px"

|  

Line 2,908: Line 2,884:

|- style="height:60px"

|  

−

| <math>\operatorname{~~R8f~~.}</math>

+

| <math>\operatorname{R9f.}</math>

−

| <math>\operatorname{Conj_x^X}~ \underline{((}~ \~~downharpoonleft s~~ \~~downharpoonright~~ (x) ~,~ \~~downharpoonleft t~~ \~~downharpoonright~~ (x) ~\underline{))}</math>

+

| <math>\operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}</math>

−

| style="border-left:1px solid black; text-align:center" | <math>\operatorname{~~R8f~~~:~R7e}</math>

+

| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9f~:~R7e}</math>

|- style="height:20px"

|  

Line 2,918: Line 2,894:

|- style="height:40px"

|  

−

| <math>\operatorname{~~R8g~~.}</math>

+

| <math>\operatorname{R9g.}</math>

−

| <math>\operatorname{Conj_x^X}~ \underline{((}~ \~~downharpoonleft s~~ \~~downharpoonright~~ ~,~ \~~downharpoonleft t~~ \~~downharpoonright~~ ~\underline{))}^\$ (x)</math>

+

| <math>\operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\$ (x)</math>

−

| style="border-left:1px solid black; text-align:center" | <math>\operatorname{~~R8g~~~:~R7f}</math>

+

| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9g~:~R7f}</math>

|}

Jon Awbrey

12,089

edits