Difference between revisions of "User:Jon Awbrey/SCRATCHPAD"

MyWikiBiz, Author Your Legacy — Wednesday May 01, 2024
Jump to navigationJump to search
(move box displays to their own workspace)
Line 914: Line 914:
 
                       &                      &  & \} & \\
 
                       &                      &  & \} & \\
 
\end{array}</math>
 
\end{array}</math>
 
<br>
 
 
==Box Displays==
 
 
===Blank Form===
 
 
<br>
 
 
{| 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:50px; text-align:center"
 
| style="width:80%" | &nbsp;
 
| style="width:20%; border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:50px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="12%" style="border-top:1px solid black" | &nbsp;
 
| width="66%" style="border-top:1px solid black" | &nbsp;
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:50px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:10px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="12%" style="border-top:1px solid black" | &nbsp;
 
| width="66%" style="border-top:1px solid black" | &nbsp;
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | &nbsp;
 
| valign="top" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | &nbsp;
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | &nbsp;
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | &nbsp;
 
| valign="top" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | &nbsp;
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | &nbsp;
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | &nbsp;
 
| valign="top" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | &nbsp;
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | &nbsp;
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | &nbsp;
 
| valign="top" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | &nbsp;
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | &nbsp;
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | &nbsp;
 
| valign="top" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" |&nbsp;
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | &nbsp;
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | &nbsp;
 
| valign="top" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | &nbsp;
 
|}
 
|}
 
 
<br>
 
 
===Formal Grammars===
 
 
<br>
 
 
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
 
| align="left"  style="border-left:1px solid black;"  width="50%" |
 
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 1}\!</math>
 
| align="right" style="border-right:1px solid black;" width="50%" |
 
<math>\mathfrak{Q} = \varnothing</math>
 
|-
 
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
 
<math>\begin{array}{rcll}
 
1.
 
& S
 
& :>
 
& m_1 \ = \ ^{\backprime\backprime} \operatorname{~} ^{\prime\prime}
 
\\
 
2.
 
& S
 
& :>
 
& p_j, \, \text{for each} \, j \in J
 
\\
 
3.
 
& S
 
& :>
 
& \operatorname{Conc}^0 \ = \ ^{\backprime\backprime\prime\prime}
 
\\
 
4.
 
& S
 
& :>
 
& \operatorname{Surc}^0 \ = \ ^{\backprime\backprime} \, \operatorname{()} \, ^{\prime\prime}
 
\\
 
5.
 
& S
 
& :>
 
& S^*
 
\\
 
6.
 
& S
 
& :>
 
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, S \, \cdot \, ( \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S \, )^* \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
 
\\
 
\end{array}</math>
 
|}
 
 
<br>
 
 
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
 
| align="left"  style="border-left:1px solid black;"  width="50%" |
 
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 2}\!</math>
 
| align="right" style="border-right:1px solid black;" width="50%" |
 
<math>\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}</math>
 
|-
 
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
 
<math>\begin{array}{rcll}
 
1.
 
& S
 
& :>
 
& \varepsilon
 
\\
 
2.
 
& S
 
& :>
 
& m_1
 
\\
 
3.
 
& S
 
& :>
 
& p_j, \, \text{for each} \, j \in J
 
\\
 
4.
 
& S
 
& :>
 
& S \, \cdot \, S
 
\\
 
5.
 
& S
 
& :>
 
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
 
\\
 
6.
 
& T
 
& :>
 
& S
 
\\
 
7.
 
& T
 
& :>
 
& T \, \cdot \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S
 
\\
 
\end{array}</math>
 
|}
 
 
<br>
 
 
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
 
| align="left"  style="border-left:1px solid black;"  width="50%" |
 
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 3}\!</math>
 
| align="right" style="border-right:1px solid black;" width="50%" |
 
<math>\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, F \, ^{\prime\prime}, \, ^{\backprime\backprime} \, R \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}</math>
 
|-
 
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
 
<math>\begin{array}{rcll}
 
1.
 
& S
 
& :>
 
& R
 
\\
 
2.
 
& S
 
& :>
 
& F
 
\\
 
3.
 
& S
 
& :>
 
& S \, \cdot \, S
 
\\
 
4.
 
& R
 
& :>
 
& \varepsilon
 
\\
 
5.
 
& R
 
& :>
 
& m_1
 
\\
 
6.
 
& R
 
& :>
 
& p_j, \, \text{for each} \, j \in J
 
\\
 
7.
 
& R
 
& :>
 
& R \, \cdot \, R
 
\\
 
8.
 
& F
 
& :>
 
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
 
\\
 
9.
 
& T
 
& :>
 
& S
 
\\
 
10.
 
& T
 
& :>
 
& T \, \cdot \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S
 
\\
 
\end{array}</math>
 
|}
 
 
<br>
 
 
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
 
| align="left"  style="border-left:1px solid black;"  width="50%" |
 
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 4}\!</math>
 
| align="right" style="border-right:1px solid black;" width="50%" |
 
<math>\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T' \, ^{\prime\prime} \, \}</math>
 
|-
 
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
 
<math>\begin{array}{rcll}
 
1.
 
& S
 
& :>
 
& \varepsilon
 
\\
 
2.
 
& S
 
& :>
 
& S'
 
\\
 
3.
 
& S'
 
& :>
 
& m_1
 
\\
 
4.
 
& S'
 
& :>
 
& p_j, \, \text{for each} \, j \in J
 
\\
 
5.
 
& S'
 
& :>
 
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
 
\\
 
6.
 
& S'
 
& :>
 
& S' \, \cdot \, S'
 
\\
 
7.
 
& T
 
& :>
 
& \varepsilon
 
\\
 
8.
 
& T
 
& :>
 
& T'
 
\\
 
9.
 
& T'
 
& :>
 
& T \, \cdot \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S
 
\\
 
\end{array}</math>
 
|}
 
 
<br>
 
 
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
 
| align="left"  style="border-left:1px solid black;"  width="50%" |
 
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 5}\!</math>
 
| align="right" style="border-right:1px solid black;" width="50%" |
 
<math>\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}</math>
 
|-
 
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
 
<math>\begin{array}{rcll}
 
1.
 
& S
 
& :>
 
& \varepsilon
 
\\
 
2.
 
& S
 
& :>
 
& S'
 
\\
 
3.
 
& S'
 
& :>
 
& m_1
 
\\
 
4.
 
& S'
 
& :>
 
& p_j, \, \text{for each} \, j \in J
 
\\
 
5.
 
& S'
 
& :>
 
& S' \, \cdot \, S'
 
\\
 
6.
 
& S'
 
& :>
 
& ^{\backprime\backprime} \, \operatorname{()} \, ^{\prime\prime}
 
\\
 
7.
 
& S'
 
& :>
 
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
 
\\
 
8.
 
& T
 
& :>
 
& ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime}
 
\\
 
9.
 
& T
 
& :>
 
& S'
 
\\
 
10.
 
& T
 
& :>
 
& T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime}
 
\\
 
11.
 
& T
 
& :>
 
& T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime} \, \cdot \, S'
 
\\
 
\end{array}</math>
 
|}
 
 
<br>
 
 
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
 
| align="left"  style="border-left:1px solid black;"  width="50%" |
 
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 6}\!</math>
 
| align="right" style="border-right:1px solid black;" width="50%" |
 
<math>\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, F \, ^{\prime\prime}, \, ^{\backprime\backprime} \, R \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}</math>
 
|-
 
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
 
<math>\begin{array}{rcll}
 
1.
 
& S
 
& :>
 
& \varepsilon
 
\\
 
2.
 
& S
 
& :>
 
& S'
 
\\
 
3.
 
& S'
 
& :>
 
& R
 
\\
 
4.
 
& S'
 
& :>
 
& F
 
\\
 
5.
 
& S'
 
& :>
 
& S' \, \cdot \, S'
 
\\
 
6.
 
& R
 
& :>
 
& m_1
 
\\
 
7.
 
& R
 
& :>
 
& p_j, \, \text{for each} \, j \in J
 
\\
 
8.
 
& R
 
& :>
 
& R \, \cdot \, R
 
\\
 
9.
 
& F
 
& :>
 
& ^{\backprime\backprime} \, \operatorname{()} \, ^{\prime\prime}
 
\\
 
10.
 
& F
 
& :>
 
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
 
\\
 
11.
 
& T
 
& :>
 
& ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime}
 
\\
 
12.
 
& T
 
& :>
 
& S'
 
\\
 
13.
 
& T
 
& :>
 
& T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime}
 
\\
 
14.
 
& T
 
& :>
 
& T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime} \, \cdot \, S'
 
\\
 
\end{array}</math>
 
|}
 
 
<br>
 
 
===Proof Schemata===
 
 
====Definition 1====
 
 
=====Variant 1=====
 
 
<br>
 
 
{| align="center" cellpadding="2" 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%"
 
|- style="height:40px"
 
| width="2%"  | &nbsp;
 
| width="18%" | &nbsp;
 
| width="60%" | &nbsp;
 
| align="center" width="20%" | <math>\text{Definition 1}\!</math>
 
|- style="height:40px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| style="border-top:1px solid black" | <math>Q \subseteq X</math>
 
| style="border-top:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}</math>
 
| &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{such that:}\!</math>
 
| &nbsp;
 
| &nbsp;
 
|- style="height:40px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="border-top:1px solid black" | <math>\text{D1a.}\!</math>
 
| style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ x \in Q</math>
 
| align="center" style="border-top:1px solid black" | <math>\forall x \in X</math>
 
|}
 
 
<br>
 
 
=====Variant 2=====
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\text{Definition 1}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{such that:}\!</math>
 
| &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D1a.}</math>
 
| width="60%" style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ x \in Q</math>
 
| width="20%" style="border-top:1px solid black; text-align:center" | <math>\forall x \in X</math>
 
|}
 
|}
 
 
<br>
 
 
====Rule 1====
 
 
<br>
 
 
{| align="center" cellpadding="2" 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%"
 
|- style="height:40px"
 
| width="2%"  | &nbsp;
 
| width="18%" | &nbsp;
 
| width="60%" | &nbsp;
 
| align="center" width="20%" | <math>\text{Rule 1}\!</math>
 
|- style="height:40px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| style="border-top:1px solid black" | <math>Q \subseteq X</math>
 
| style="border-top:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}</math>
 
| &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{and if}\!</math>
 
| <math>x \in X</math>
 
| &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| &nbsp;
 
|- style="height:40px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="border-top:1px solid black" | <math>\text{R1a.}\!</math>
 
| style="border-top:1px solid black" | <math>x \in Q</math>
 
| style="border-top:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{R1b.}\!</math>
 
| <math>\upharpoonleft Q \upharpoonright (x)</math>
 
| &nbsp;
 
|}
 
 
<br>
 
 
====Rule 2====
 
 
<br>
 
 
{| align="center" cellpadding="2" 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%"
 
|- style="height:40px"
 
| width="2%"  | &nbsp;
 
| width="18%" | &nbsp;
 
| width="60%" | &nbsp;
 
| align="center" width="20%" | <math>\text{Rule 2}\!</math>
 
|- style="height:40px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="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-top:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>x \in X</math>
 
| &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| &nbsp;
 
|- style="height:40px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="border-top:1px solid black" | <math>\text{R2a.}\!</math>
 
| style="border-top:1px solid black" | <math>f(x)\!</math>
 
| style="border-top:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{R2b.}\!</math>
 
| <math>f(x) = \underline{1}</math>
 
| &nbsp;
 
|}
 
 
<br>
 
 
====Rule 3====
 
 
=====Variant 1=====
 
 
<br>
 
 
{| align="center" cellpadding="2" 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%"
 
|- style="height:40px"
 
| width="2%"  | &nbsp;
 
| width="18%" | &nbsp;
 
| width="60%" | &nbsp;
 
| align="center" style="border-left:1px solid black" width="20%" | <math>\text{Rule 3}\!</math>
 
|- style="height:40px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| style="border-top:1px solid black" | <math>Q \subseteq X</math>
 
| style="border-left:1px solid black; border-top:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>x \in X</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|- style="height:36px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="border-top:1px solid black" | <math>\text{R3a.}\!</math>
 
| style="border-top:1px solid black" | <math>x \in Q</math>
 
| style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\text{R3a : R1a}\!</math>
 
|- style="height:24px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:36px"
 
| &nbsp;
 
| <math>\text{R3b.}\!</math>
 
| <math>\upharpoonleft Q \upharpoonright (x)</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\text{R3b : R1b}\!</math></p>
 
<p><math>\text{R3b : R2a}\!</math></p>
 
|- style="height:24px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:36px"
 
| &nbsp;
 
| <math>\text{R3c.}\!</math>
 
| <math>\upharpoonleft Q \upharpoonright (x) = \underline{1}</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\text{R3c : R2b}\!</math>
 
|}
 
 
<br>
 
 
=====Variant 2=====
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~3}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="60%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>x ~\in~ X</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R3a.}</math>
 
| width="60%" style="border-top:1px solid black" | <math>x ~\in~ Q</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R3a~:~R1a}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{R3b.}</math>
 
| <math>\upharpoonleft Q \upharpoonright (x)</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{R3b~:~R1b}</math></p>
 
<p><math>\operatorname{R3b~:~R2a}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R3c.}</math>
 
| <math>\upharpoonleft Q \upharpoonright (x) ~=~ \underline{1}</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R3c~:~R2b}</math></p>
 
|}
 
|}
 
 
<br>
 
 
====Corollary 1====
 
 
<br>
 
 
{| align="center" cellpadding="2" 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%"
 
|- style="height:40px"
 
| width="2%"  | &nbsp;
 
| width="18%" | &nbsp;
 
| width="60%" | &nbsp;
 
| align="center" style="border-left:1px solid black" width="20%" |
 
<math>\text{Corollary 1}\!</math>
 
|- style="height:40px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| style="border-top:1px solid black" | <math>Q \subseteq X</math>
 
| style="border-left:1px solid black; border-top:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>x \in X</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following statement is true:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="border-top:1px solid black" | <math>\text{C1a.}\!</math>
 
| style="border-top:1px solid black" |
 
<math>x \in Q ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x) = \underline{1}</math>
 
| align="center" style="border-left:1px solid black; border-top:1px solid black" |
 
<math>\text{R3a} \Leftrightarrow \text{R3c}</math>
 
|}
 
 
<br>
 
 
====Rule 4====
 
 
<br>
 
 
{| align="center" cellpadding="2" 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%"
 
|- style="height:40px"
 
| width="2%"  | &nbsp;
 
| width="18%" | &nbsp;
 
| width="60%" | &nbsp;
 
| align="center" width="20%" | <math>\text{Rule 4}\!</math>
 
|- style="height:40px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| style="border-top:1px solid black" | <math>Q \subseteq X ~\text{is fixed}</math>
 
| style="border-top:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>x \in X ~\text{is varied}</math>
 
| &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| &nbsp;
 
|- style="height:40px"
 
| style="border-top:1px solid black" | &nbsp;
 
| style="border-top:1px solid black" | <math>\text{R4a.}\!</math>
 
| style="border-top:1px solid black" | <math>x \in Q</math>
 
| style="border-top:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{R4b.}\!</math>
 
| <math>\downharpoonleft x \in Q \downharpoonright</math>
 
| &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{R4c.}\!</math>
 
| <math>\downharpoonleft x \in Q \downharpoonright (x)</math>
 
| &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{R4d.}\!</math>
 
| <math>\upharpoonleft Q \upharpoonright (x)</math>
 
| &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{R4e.}\!</math>
 
| <math>\upharpoonleft Q \upharpoonright (x) = \underline{1}</math>
 
| &nbsp;
 
|}
 
 
<br>
 
 
===Logical Translation Rule 0===
 
 
<br>
 
 
{| 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:48px; text-align:right"
 
| width="98%" | <math>\text{Logical Translation Rule 0}\!</math>
 
| width="2%"  | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:48px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" |
 
<math>s_j ~\text{is a sentence about things in the universe X}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>p_j ~\text{is a proposition about things in the universe X}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{such that:}\!</math>
 
| &nbsp;
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{L0a.}\!</math>
 
| <math>\downharpoonleft s_j \downharpoonright ~=~ p_j, ~\text{for all}~ j \in J,</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following equations are true:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:56px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{L0b.}\!</math>
 
| width="20%" style="border-top:1px solid black" |
 
<math>\downharpoonleft \operatorname{Conc}_j^J s_j \downharpoonright</math>
 
| width="10%" style="border-top:1px solid black" | <math>=\!</math>
 
| width="20%" style="border-top:1px solid black" |
 
<math>\operatorname{Conj}_j^J \downharpoonleft s_j \downharpoonright</math>
 
| width="10%" style="border-top:1px solid black" | <math>=\!</math>
 
| width="20%" style="border-top:1px solid black" |
 
<math>\operatorname{Conj}_j^J p_j</math>
 
|- style="height:56px"
 
| &nbsp;
 
| <math>\text{L0c.}\!</math>
 
| <math>\downharpoonleft \operatorname{Surc}_j^J s_j \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>\operatorname{Surj}_j^J \downharpoonleft s_j \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>\operatorname{Surj}_j^J p_j</math>
 
|}
 
|}
 
 
<br>
 
 
===Logical Translation Rule 1===
 
 
<br>
 
 
{| 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:48px; text-align:right"
 
| width="98%" | <math>\text{Logical Translation Rule 1}\!</math>
 
| width="2%"  | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:48px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" |
 
<math>s ~\text{is a sentence about things in the universe X}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>p ~\text{is a proposition} ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{such that:}\!</math>
 
| &nbsp;
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{L1a.}\!</math>
 
| <math>\downharpoonleft s \downharpoonright ~=~ p</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following equations hold:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" style="text-align:center" width="100%"
 
|- style="height:52px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" align="left" | <math>\text{L1b}_{00}.\!</math>
 
| width="20%" style="border-top:1px solid black" |
 
<math>\downharpoonleft \operatorname{false} \downharpoonright</math>
 
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
 
| width="20%" style="border-top:1px solid black" | <math>(~)</math>
 
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
 
| width="30%" style="border-top:1px solid black" |
 
<math>\underline{0} ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L1b}_{01}.\!</math>
 
| <math>\downharpoonleft \operatorname{not}~ s \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\downharpoonleft s \downharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(p) ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L1b}_{10}.\!</math>
 
| <math>\downharpoonleft s \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>\downharpoonleft s \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>p ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L1b}_{11}.\!</math>
 
| <math>\downharpoonleft \operatorname{true} \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>((~))</math>
 
| <math>=\!</math>
 
| <math>\underline{1} ~:~ X \to \underline\mathbb{B}</math>
 
|}
 
|}
 
 
<br>
 
 
===Geometric Translation Rule 1===
 
 
<br>
 
 
{| 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:48px; text-align:right"
 
| width="98%" | <math>\text{Geometric Translation Rule 1}\!</math>
 
| width="2%"  | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:48px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>Q \subseteq X</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>p ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{such that:}\!</math>
 
| &nbsp;
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{G1a.}\!</math>
 
| <math>\upharpoonleft Q \upharpoonright ~=~ p</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following equations hold:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" style="text-align:center" width="100%"
 
|- style="height:52px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" align="left" | <math>\text{G1b}_{00}.\!</math>
 
| width="20%" style="border-top:1px solid black" |
 
<math>\upharpoonleft \varnothing \upharpoonright</math>
 
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
 
| width="20%" style="border-top:1px solid black" | <math>(~)</math>
 
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
 
| width="30%" style="border-top:1px solid black" |
 
<math>\underline{0} ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G1b}_{01}.\!</math>
 
| <math>\upharpoonleft {}^{_\sim} Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\upharpoonleft Q \upharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(p) ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G1b}_{10}.\!</math>
 
| <math>\upharpoonleft Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>\upharpoonleft Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>p ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G1b}_{11}.\!</math>
 
| <math>\upharpoonleft X \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>((~))</math>
 
| <math>=\!</math>
 
| <math>\underline{1} ~:~ X \to \underline\mathbb{B}</math>
 
|}
 
|}
 
 
<br>
 
 
===Logical Translation Rule 2===
 
 
<br>
 
 
{| 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:48px; text-align:right"
 
| width="98%" | <math>\text{Logical Translation Rule 2}\!</math>
 
| width="2%"  | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:48px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="84%" style="border-top:1px solid black" |
 
<math>s, t ~\text{are sentences about things in the universe}~ X</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>p, q ~\text{are propositions} ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{such that:}\!</math>
 
| &nbsp;
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{L2a.}\!</math>
 
| <math>\downharpoonleft s \downharpoonright ~=~ p \quad \operatorname{and} \quad \downharpoonleft t \downharpoonright ~=~ q</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following equations hold:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" style="text-align:center" width="100%"
 
|- style="height:52px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" align="left" | <math>\text{L2b}_{0}.\!</math>
 
| width="32%" style="border-top:1px solid black" |
 
<math>\downharpoonleft \operatorname{false} \downharpoonright</math>
 
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
 
| width="28%" style="border-top:1px solid black" | <math>(~)</math>
 
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
 
| width="16%" style="border-top:1px solid black" | <math>(~)</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{1}.\!</math>
 
| <math>\downharpoonleft \operatorname{neither}~ s ~\operatorname{nor}~ t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(p)(q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{2}.\!</math>
 
| <math>\downharpoonleft \operatorname{not}~ s ~\operatorname{but}~ t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>(p) q\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{3}.\!</math>
 
| <math>\downharpoonleft \operatorname{not}~ s \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\downharpoonleft s \downharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(p)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{4}.\!</math>
 
| <math>\downharpoonleft s ~\operatorname{and~not}~ t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright)</math>
 
| <math>=\!</math>
 
| <math>p (q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{5}.\!</math>
 
| <math>\downharpoonleft \operatorname{not}~ t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\downharpoonleft t \downharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{6}.\!</math>
 
| <math>\downharpoonleft s ~\operatorname{or}~ t, ~\operatorname{not~both} \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(p, q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{7}.\!</math>
 
| <math>\downharpoonleft \operatorname{not~both}~ s ~\operatorname{and}~ t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(p q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{8}.\!</math>
 
| <math>\downharpoonleft s ~\operatorname{and}~ t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>p q\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{9}.\!</math>
 
| <math>\downharpoonleft s ~\operatorname{is~equivalent~to}~ t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>((\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright))</math>
 
| <math>=\!</math>
 
| <math>((p, q))\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{10}.\!</math>
 
| <math>\downharpoonleft t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>\downharpoonleft t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>q\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{11}.\!</math>
 
| <math>\downharpoonleft s ~\operatorname{implies}~ t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright))</math>
 
| <math>=\!</math>
 
| <math>(p (q))\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{12}.\!</math>
 
| <math>\downharpoonleft s \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>\downharpoonleft s \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>p\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{13}.\!</math>
 
| <math>\downharpoonleft s ~\operatorname{is~implied~by}~ t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>((\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright)</math>
 
| <math>=\!</math>
 
| <math>((p) q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{14}.\!</math>
 
| <math>\downharpoonleft s ~\operatorname{or}~ t \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>((\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright))</math>
 
| <math>=\!</math>
 
| <math>((p)(q))\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{15}.\!</math>
 
| <math>\downharpoonleft \operatorname{true} \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>((~))</math>
 
| <math>=\!</math>
 
| <math>((~))</math>
 
|}
 
|}
 
 
<br>
 
 
===Geometric Translation Rule 2===
 
 
<br>
 
 
{| 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:48px; text-align:right"
 
| width="98%" | <math>\text{Geometric Translation Rule 2}\!</math>
 
| width="2%"  | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:48px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>P, Q \subseteq X</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>p, q ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{such that:}\!</math>
 
| &nbsp;
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{G2a.}\!</math>
 
| <math>\upharpoonleft P \upharpoonright ~=~ p \quad \operatorname{and} \quad \upharpoonleft Q \upharpoonright ~=~ q</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following equations hold:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" style="text-align:center" width="100%"
 
|- style="height:52px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" align="left" | <math>\text{G2b}_{0}.\!</math>
 
| width="32%" style="border-top:1px solid black" |
 
<math>\upharpoonleft \varnothing \upharpoonright</math>
 
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
 
| width="28%" style="border-top:1px solid black" | <math>(~)</math>
 
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
 
| width="16%" style="border-top:1px solid black" | <math>(~)</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{1}.\!</math>
 
| <math>\upharpoonleft \overline{P} ~\cap~ \overline{Q} \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(p)(q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{2}.\!</math>
 
| <math>\upharpoonleft \overline{P} ~\cap~ Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>(p) q\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{3}.\!</math>
 
| <math>\upharpoonleft \overline{P} \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\upharpoonleft P \upharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(p)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{4}.\!</math>
 
| <math>\upharpoonleft P ~\cap~ \overline{Q} \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright)</math>
 
| <math>=\!</math>
 
| <math>p (q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{5}.\!</math>
 
| <math>\upharpoonleft \overline{Q} \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\upharpoonleft Q \upharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{6}.\!</math>
 
| <math>\upharpoonleft P ~+~ Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(p, q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{7}.\!</math>
 
| <math>\upharpoonleft \overline{P ~\cap~ Q} \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright)</math>
 
| <math>=\!</math>
 
| <math>(p q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{8}.\!</math>
 
| <math>\upharpoonleft P ~\cap~ Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>p q\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{9}.\!</math>
 
| <math>\upharpoonleft \overline{P ~+~ Q} \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>((\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright))</math>
 
| <math>=\!</math>
 
| <math>((p, q))\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{10}.\!</math>
 
| <math>\upharpoonleft Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>\upharpoonleft Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>q\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{11}.\!</math>
 
| <math>\upharpoonleft \overline{P ~\cap~ \overline{Q}} \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>(\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright))</math>
 
| <math>=\!</math>
 
| <math>(p (q))\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{12}.\!</math>
 
| <math>\upharpoonleft P \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>\upharpoonleft P \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>p\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{13}.\!</math>
 
| <math>\upharpoonleft \overline{\overline{P} ~\cap~ Q} \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>((\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright)</math>
 
| <math>=\!</math>
 
| <math>((p) q)\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{14}.\!</math>
 
| <math>\upharpoonleft P ~\cup~ Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>((\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright))</math>
 
| <math>=\!</math>
 
| <math>((p)(q))\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{G2b}_{15}.\!</math>
 
| <math>\upharpoonleft X \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>((~))</math>
 
| <math>=\!</math>
 
| <math>((~))</math>
 
|}
 
|}
 
 
<br>
 
 
===Value Rule 1===
 
 
'''Editing Note.'''  There are several versions of this Rule in the last couple of drafts I can find.  I will try to figure out what's at issue here as I mark them up.
 
 
====Variant 1====
 
 
<br>
 
 
{| 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:48px; text-align:right"
 
| width="98%" | <math>\text{Value Rule 1}\!</math>
 
| width="2%"  | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:48px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>v, w ~\in~ \underline\mathbb{B}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>^{\backprime\backprime} v = w \, ^{\prime\prime} ~\text{is a sentence about pairs of values}~ (v, w) \in \underline\mathbb{B}^2,</math>
 
|- style="height:48px"
 
| &nbsp;
 
| &nbsp;
 
| <math>\downharpoonleft v = w \downharpoonright ~\text{is a proposition} ~:~ \underline\mathbb{B}^2 \to \underline\mathbb{B},</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>\text{the following are identical values in}~ \underline\mathbb{B}:</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:56px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{V1a.}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>\downharpoonleft v = w \downharpoonright (v, w)</math>
 
|- style="height:56px"
 
| &nbsp;
 
| <math>\text{V1b.}\!</math>
 
| <math>\downharpoonleft v \Leftrightarrow w \downharpoonright (v, w)</math>
 
|- style="height:56px"
 
| &nbsp;
 
| <math>\text{V1c.}\!</math>
 
| <math>\underline{((}~ v ~,~ w ~\underline{))}</math>
 
|}
 
|}
 
 
<br>
 
 
====Variant 2====
 
 
<br>
 
 
{| 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:48px; text-align:right"
 
| width="98%" | <math>\text{Value Rule 1}\!</math>
 
| width="2%"  | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:48px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>v, w ~\in~ \underline\mathbb{B}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:56px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{V1a.}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>v = w\!</math>
 
|- style="height:56px"
 
| &nbsp;
 
| <math>\text{V1b.}\!</math>
 
| <math>v \Leftrightarrow w</math>
 
|- style="height:56px"
 
| &nbsp;
 
| <math>\text{V1c.}\!</math>
 
| <math>\underline{((}~ v ~,~ w ~\underline{))}</math>
 
|}
 
|}
 
 
<br>
 
 
====Variant 3====
 
 
A rule that allows one to turn equivalent sentences into identical propositions:
 
 
{| align="center" cellpadding="8" width="90%"
 
| <math>(s ~\Leftrightarrow~ t) \quad \Leftrightarrow \quad (\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright)</math>
 
|}
 
 
Consider the following pair of expressions:
 
 
{| align="center" cellpadding="8" width="90%"
 
| <math>\downharpoonleft v ~=~ w \downharpoonright (v, w)</math>
 
|-
 
| <math>\downharpoonleft v(x) ~=~ w(x) \downharpoonright (x)</math>
 
|}
 
 
<br>
 
 
{| 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:48px; text-align:right"
 
| width="98%" | <math>\text{Value Rule 1}\!</math>
 
| width="2%"  | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:48px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>v, w ~\in~ \underline\mathbb{B}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical values in}~ \underline\mathbb{B}:</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:56px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{V1a.}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>\downharpoonleft v = w \downharpoonright</math>
 
|- style="height:56px"
 
| &nbsp;
 
| <math>\text{V1b.}\!</math>
 
| <math>\downharpoonleft v \Leftrightarrow w \downharpoonright</math>
 
|- style="height:56px"
 
| &nbsp;
 
| <math>\text{V1c.}\!</math>
 
| <math>\underline{((}~ v ~,~ w ~\underline{))}</math>
 
|}
 
|}
 
 
<br>
 
 
====Variant 4====
 
 
<br>
 
 
{| 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:48px; text-align:right"
 
| width="98%" | <math>\text{Value Rule 1}\!</math>
 
| width="2%"  | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:48px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>f, g ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>x ~\in~ X</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical values in}~ \underline\mathbb{B}:</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:56px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{V1a.}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>\downharpoonleft f(x) ~=~ g(x) \downharpoonright</math>
 
|- style="height:56px"
 
| &nbsp;
 
| <math>\text{V1b.}\!</math>
 
| <math>\downharpoonleft f(x) ~\Leftrightarrow~ g(x) \downharpoonright</math>
 
|- style="height:56px"
 
| &nbsp;
 
| <math>\text{V1c.}\!</math>
 
| <math>\underline{((}~ f(x) ~,~ g(x) ~\underline{))}</math>
 
|}
 
|}
 
 
<br>
 
 
====Variant 5====
 
 
<br>
 
 
{| 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:48px; text-align:right"
 
| width="98%" | <math>\text{Value Rule 1}\!</math>
 
| width="2%"  | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:48px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>f, g ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:48px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical propositions on}~ X:</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:56px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{V1a.}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>\downharpoonleft f ~=~ g \downharpoonright</math>
 
|- style="height:56px"
 
| &nbsp;
 
| <math>\text{V1b.}\!</math>
 
| <math>\downharpoonleft f ~\Leftrightarrow~ g \downharpoonright</math>
 
|- style="height:56px"
 
| &nbsp;
 
| <math>\text{V1c.}\!</math>
 
| <math>\underline{((}~ f ~,~ g ~\underline{))}^\$</math>
 
|}
 
|}
 
 
<br>
 
 
===Evaluation Rule 1===
 
 
<br>
 
 
{| 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:50px; text-align:right"
 
| width="98%" | <math>\operatorname{Evaluation~Rule~1}</math>
 
| width="2%"  | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:50px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="84%" style="border-top:1px solid black" | <math>f, g ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>x ~\in~ X</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:10px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="14%" style="border-top:1px solid black" | &nbsp;
 
| width="64%" style="border-top:1px solid black" | &nbsp;
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{E1a.}</math>
 
| <math>f(x) ~=~ g(x)</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{E1a~:~V1a}</math>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{E1b.}</math>
 
| <math>f(x) ~\Leftrightarrow~ g(x)</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{E1b~:~V1b}</math>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{E1c.}</math>
 
| <math>\underline{((}~ f(x) ~,~ g(x) ~\underline{))}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{E1c~:~V1c}</math></p>
 
<p><math>\operatorname{E1c~:~$1a}</math></p>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{E1d.}</math>
 
| <math>\underline{((}~ f ~,~ g ~\underline{))}^\$ (x)</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{E1d~:~$1b}</math>
 
|- style="height:10px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|}
 
 
<br>
 
 
===Definition 2===
 
 
====Variant 1====
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~2}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>P, Q ~\subseteq~ X</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D2a.}</math>
 
| width="60%" style="border-top:1px solid black" | <math>P ~=~ Q</math>
 
| width="20%" style="border-top:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D2b.}</math>
 
| <math>x \in P ~\Leftrightarrow~ x \in Q</math>
 
| align="center" | <math>\forall x \in X</math>
 
|}
 
|}
 
 
<br>
 
 
====Variant 2====
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~2}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>P, Q ~\subseteq~ X</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D2a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>P ~=~ Q</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{D2b.}</math>
 
| <math>\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)</math>
 
|}
 
|}
 
 
<br>
 
 
===Definition 3===
 
 
====Variant 1====
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~3}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>f, g ~:~ X \to Y</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D3a.}</math>
 
| width="60%" style="border-top:1px solid black" | <math>f ~=~ g</math>
 
| width="20%" style="border-top:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D3b.}</math>
 
| <math>f(x) ~=~ g(x)</math>
 
| align="center" | <math>\forall x \in X</math>
 
|}
 
|}
 
 
<br>
 
 
====Variant 2====
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~3}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>f, g ~:~ X \to Y</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D3a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>f ~=~ g</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{D3b.}</math>
 
| <math>\overset{X}{\underset{x}{\forall}}~ (f(x) ~=~ g(x))</math>
 
|}
 
|}
 
 
<br>
 
 
====Variant 3====
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~3}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>f, g ~:~ X \to Y</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D3a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>f ~=~ g</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{D3b.}</math>
 
| <math>\prod_x^X~ (f(x) ~=~ g(x))</math>
 
|}
 
|}
 
 
<br>
 
 
===Definition 4===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~4}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical subsets of}~ X \times \underline\mathbb{B}:</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D4a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D4b.}</math>
 
| <math>\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in Q \downharpoonright</math>
 
|}
 
|}
 
 
<br>
 
 
===Definition 5===
 
 
====Variant 1====
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~5}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical propositions:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D5a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{D5b.}</math>
 
|
 
<math>\begin{array}{lcl}
 
f    & : & X \to \underline\mathbb{B}
 
\\
 
f(x) & = & \downharpoonleft x \in Q \downharpoonright \quad (\forall x \in X)
 
\end{array}</math>
 
|}
 
|}
 
 
<br>
 
 
====Variant 2====
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~5}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical propositions:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D5a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{D5b.}</math>
 
|
 
<math>\begin{array}{ccccl}
 
f & : & X & \to    & \underline\mathbb{B}
 
\\
 
f & : & x & \mapsto & \downharpoonleft x \in Q \downharpoonright
 
\end{array}</math>
 
|}
 
|}
 
 
<br>
 
 
====Variant 3====
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~5}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical propositions} ~:~ X \to \underline\mathbb{B}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D5a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D5b.}</math>
 
| <math>\downharpoonleft x \in Q \downharpoonright</math>
 
|}
 
|}
 
 
<br>
 
 
===Definition 6===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~6}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>\text{each string}~ s_j, ~\text{as}~ j ~\text{ranges over the set}~ J,</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| <math>\text{is a sentence about things in the universe}~ X~</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:60px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D6a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>\overset{J}{\underset{j}{\forall}}~ s_j</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{D6b.}</math>
 
| <math>\operatorname{Conj}_j^J s_j</math>
 
|}
 
|}
 
 
<br>
 
 
===Definition 7===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~7}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>s, t ~\text{are sentences about things in the universe}~ X</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D7a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>s ~\Leftrightarrow~ t</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D7b.}</math>
 
| <math>\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright</math>
 
|}
 
|}
 
 
<br>
 
 
===Rule 5===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~5}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</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" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R5a.}</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{R5a~:~D2a}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{R5b.}</math>
 
| <math>\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{R5b~:~D2b}</math></p>
 
<p><math>\operatorname{R5b~:~D7a}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{R5c.}</math>
 
| <math>\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright)</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{R5c~:~D7b}</math></p>
 
<p><math>\operatorname{R5c~:~\_\_?\_\_}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:80px"
 
| &nbsp;
 
| <math>\operatorname{R5d.}</math>
 
|
 
<math>\begin{matrix}
 
\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in P \downharpoonright
 
\\
 
=
 
\\
 
\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in Q \downharpoonright
 
\end{matrix}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{R5d~:~\_\_?\_\_}</math></p>
 
<p><math>\operatorname{R5d~:~D5b}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R5e.}</math>
 
| <math>\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R5e~:~D5a}</math>
 
|}
 
|}
 
 
<br>
 
 
===Rule 6===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~6}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="60%" style="border-top:1px solid black" | <math>f, g ~:~ X \to Y</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R6a.}</math>
 
| width="60%" style="border-top:1px solid black" | <math>f ~=~ g</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R6a~:~D3a}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{R6b.}</math>
 
| <math>\overset{X}{\underset{x}{\forall}}~ (f(x) ~=~ g(x))</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{R6b~:~D3b}</math></p>
 
<p><math>\operatorname{R6b~:~D6a}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R6c.}</math>
 
| <math>\operatorname{Conj_x^X}~ (f(x) ~=~ g(x))</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R6c~:~D6b}</math>
 
|}
 
|}
 
 
<br>
 
 
===Rule 7===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| 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" | &nbsp;
 
| 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" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| 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"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <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"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <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"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <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"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <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"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <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>
 
|}
 
|}
 
 
<br>
 
 
===Rule 8===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| 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" | &nbsp;
 
| 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" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| 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"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <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"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <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"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <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"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <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"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <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"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <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>
 
 
===Rule 9===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~9}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</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" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R9a.}</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{R9a~:~R5a}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{R9b.}</math>
 
| <math>\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{R9b~:~R5e}</math></p>
 
<p><math>\operatorname{R9b~:~R7a}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{R9c.}</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{R9c~:~R7b}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R9d.}</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{R9d~:~R7c}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R9e.}</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{R9e~:~R7d}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{R9f.}</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{R9f~:~R7e}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R9g.}</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{R9g~:~R7f}</math>
 
|}
 
|}
 
 
<br>
 
 
===Rule 10===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~10}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</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" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R10a.}</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{R10a~:~D2a}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{R10b.}</math>
 
| <math>\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{R10b~:~D2b}</math></p>
 
<p><math>\operatorname{R10b~:~R8a}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R10c.}</math>
 
| <math>\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10c~:~R8b}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R10d.}</math>
 
| <math>\overset{X}{\underset{x}{\forall}}~ \downharpoonleft x \in P \downharpoonright (x) ~=~ \downharpoonleft x \in Q \downharpoonright (x)</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10d~:~R8c}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R10e.}</math>
 
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~=~ \downharpoonleft x \in Q \downharpoonright (x))</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10e~:~R8d}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R10f.}</math>
 
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft x \in Q \downharpoonright (x))</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10f~:~R8e}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R10g.}</math>
 
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft x \in P \downharpoonright (x) ~,~ \downharpoonleft x \in Q \downharpoonright (x) ~\underline{))}</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10g~:~R8f}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R10h.}</math>
 
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft x \in P \downharpoonright ~,~ \downharpoonleft x \in Q \downharpoonright ~\underline{))}^\$ (x)</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10h~:~R8g}</math>
 
|}
 
|}
 
 
<br>
 
 
===Rule 11===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~11}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="60%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R11a.}</math>
 
| width="60%" style="border-top:1px solid black" | <math>Q ~=~ \{ x \in X ~:~ s \}</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R11a~:~R5a}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R11b.}</math>
 
| <math>\upharpoonleft Q \upharpoonright ~=~ \upharpoonleft \{ x \in X ~:~ s \} \upharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11b~:~R5e}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{R11c.}</math>
 
|
 
<math>\begin{array}{lcl}
 
\upharpoonleft Q \upharpoonright
 
& \subseteq &
 
X \times \underline\mathbb{B}
 
\\
 
\upharpoonleft Q \upharpoonright
 
& = &
 
\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y  = \, \downharpoonleft s \downharpoonright (x) \}
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{R11c~:~\_\_?\_\_}</math></p>
 
<p><math>\operatorname{R11c~:~\_\_?\_\_}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{R11d.}</math>
 
|
 
<math>\begin{array}{ccccl}
 
\upharpoonleft Q \upharpoonright & : & X & \to    & \underline\mathbb{B}
 
\\
 
\upharpoonleft Q \upharpoonright & : & x & \mapsto & \downharpoonleft s \downharpoonright (x)
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{R11d~:~\_\_?\_\_}</math></p>
 
<p><math>\operatorname{R11d~:~\_\_?\_\_}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{R11e.}</math>
 
| <math>\overset{X}{\underset{x}{\forall}}~ \upharpoonleft Q \upharpoonright (x) ~=~ \downharpoonleft s \downharpoonright (x)</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{R11e~:~\_\_?\_\_}</math></p>
 
<p><math>\operatorname{R11e~:~\_\_?\_\_}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{R11f.}</math>
 
| <math>\upharpoonleft Q \upharpoonright ~=~ \downharpoonleft s \downharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11f~:~\_\_?\_\_}</math>
 
|}
 
|}
 
 
<br>
 
 
===Fact 1===
 
 
====Variant 1====
 
 
<br>
 
 
{| 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:50px; text-align:center"
 
| style="width:80%" | &nbsp;
 
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~1}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:50px"
 
| style="border-top:1px solid black; width:2%"  | &nbsp;
 
| style="border-top:1px solid black; width:18%" | <math>\text{If}\!</math>
 
| style="border-top:1px solid black; width:60%" | <math>P, Q ~\subseteq~ X</math>
 
| style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:60px"
 
| style="width:2%;  border-top:1px solid black" | &nbsp;
 
| style="width:14%; border-top:1px solid black" | <math>\operatorname{F1a.}</math>
 
| style="width:64%; border-top:1px solid black" | <math>s \quad \Leftrightarrow \quad (P ~=~ Q)</math>
 
| style="width:20%; border-top:1px solid black; border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F1a~:~R9a}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{F1b.}</math>
 
| <math>s \quad \Leftrightarrow \quad (\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright)</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F1b~:~R9b}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F1c.}</math>
 
| <math>s \quad \Leftrightarrow \quad \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{F1c~:~R9c}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F1d.}</math>
 
| <math>s \quad \Leftrightarrow \quad \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{F1d~:~R9d}</math></p>
 
<p><math>\operatorname{F1d~:~R8a}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F1e.}</math>
 
| <math>\downharpoonleft s \downharpoonright \quad = \quad \downharpoonleft \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{F1e~:~R8b}</math></p>
 
<p><math>\operatorname{F1e~:~\_\_?\_\_}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F1f.}</math>
 
| <math>\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \downharpoonleft (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{F1f~:~\_\_?\_\_}</math></p>
 
<p><math>\operatorname{F1f~:~\_\_?\_\_}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F1g.}</math>
 
| <math>\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{F1g~:~\_\_?\_\_}</math></p>
 
<p><math>\operatorname{F1g~:~\_\_?\_\_}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{F1h.}</math>
 
| <math>\downharpoonleft s \downharpoonright \quad = \quad \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{F1h~:~~\_\_?\_\_}</math>
 
|}
 
|}
 
 
<br>
 
 
====Variant 2====
 
 
<br>
 
 
{| 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:50px; text-align:center"
 
| style="width:80%" | &nbsp;
 
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~1}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:50px"
 
| style="border-top:1px solid black; width:2%"  | &nbsp;
 
| style="border-top:1px solid black; width:18%" | <math>\text{If}\!</math>
 
| style="border-top:1px solid black; width:60%" | <math>P, Q ~\subseteq~ X</math>
 
| style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:60px"
 
| style="width:2%;  border-top:1px solid black" | &nbsp;
 
| style="width:14%; border-top:1px solid black" | <math>\operatorname{F1a.}</math>
 
| style="width:64%; border-top:1px solid black" | <math>s \quad \Leftrightarrow \quad (P ~=~ Q)</math>
 
| style="width:20%; border-top:1px solid black; border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F1a~:~R9a}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{F1b.}</math>
 
| <math>s \quad \Leftrightarrow \quad (\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright)</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F1b~:~R9b}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F1c.}</math>
 
| <math>s \quad \Leftrightarrow \quad \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{F1c~:~R9c}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F1d.}</math>
 
| <math>s \quad \Leftrightarrow \quad \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{F1d~:~R9d}</math></p>
 
<p><math>\operatorname{F1d~:~R8a}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F1e.}</math>
 
| <math>\downharpoonleft s \downharpoonright \quad = \quad \downharpoonleft \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{F1e~:~R8b}</math></p>
 
<p><math>\operatorname{F1e~:~\_\_?\_\_}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F1f.}</math>
 
| <math>\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \downharpoonleft (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{F1f~:~\_\_?\_\_}</math></p>
 
<p><math>\operatorname{F1f~:~\_\_?\_\_}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F1g.}</math>
 
| <math>\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{F1g~:~\_\_?\_\_}</math></p>
 
<p><math>\operatorname{F1g~:~\_\_?\_\_}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{F1h.}</math>
 
| <math>\downharpoonleft s \downharpoonright \quad = \quad \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{F1h~:~~\_\_?\_\_}</math>
 
|}
 
|}
 
 
<br>
 
 
===Definition 8===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~8}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical subsets of}~ S \times I \, :</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D8a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>L_{SI}\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D8b.}</math>
 
| <math>\operatorname{Con}^L</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D8c.}</math>
 
| <math>\operatorname{Con}(L)</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D8d.}</math>
 
| <math>\operatorname{proj}_{SI}(L)</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D8e.}</math>
 
| <math>\{ (s, i) \in S \times I ~:~ (o, s, i) \in L ~\operatorname{for~some}~ o \in O \}</math>
 
|}
 
|}
 
 
<br>
 
 
===Definition 9===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~9}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical subsets of}~ I \times S \, :</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:50px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D9a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>L_{IS}\!</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D9b.}</math>
 
| <math>\overset{\smile}{L_{SI}}</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D9c.}</math>
 
| <math>\overset{\smile}{\operatorname{Con}^L}</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D9d.}</math>
 
| <math>\overset{\smile}{\operatorname{Con}(L)}</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D9e.}</math>
 
| <math>\operatorname{proj}_{IS}(L)</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D9f.}</math>
 
| <math>\operatorname{Conv}(\operatorname{Con}(L))</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D9g.}</math>
 
| <math>\{ (i, s) \in I \times S ~:~ (o, s, i) \in L ~\operatorname{for~some}~ o \in O \}</math>
 
|}
 
|}
 
 
<br>
 
 
===Definition 10===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~10}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical subsets of}~ O \times S \, :</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D10a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>L_{OS}\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D10b.}</math>
 
| <math>\operatorname{Den}^L</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D10c.}</math>
 
| <math>\operatorname{Den}(L)</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D10d.}</math>
 
| <math>\operatorname{proj}_{OS}(L)</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D10e.}</math>
 
| <math>\{ (o, s) \in O \times S ~:~ (o, s, i) \in L ~\operatorname{for~some}~ i \in I \}</math>
 
|}
 
|}
 
 
<br>
 
 
===Definition 11===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~11}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical subsets of}~ S \times O \, :</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:50px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D11a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>L_{SO}\!</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D11b.}</math>
 
| <math>\overset{\smile}{L_{OS}}</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D11c.}</math>
 
| <math>\overset{\smile}{\operatorname{Den}^L}</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D11d.}</math>
 
| <math>\overset{\smile}{\operatorname{Den}(L)}</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D11e.}</math>
 
| <math>\operatorname{proj}_{SO}(L)</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D11f.}</math>
 
| <math>\operatorname{Conv}(\operatorname{Den}(L))</math>
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\operatorname{D11g.}</math>
 
| <math>\{ (s, o) \in S \times O ~:~ (o, s, i) \in L ~\operatorname{for~some}~ i \in I \}</math>
 
|}
 
|}
 
 
<br>
 
 
===Definition 12===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~12}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>x ~\in~ S</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical subsets of}~ O \, :</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D12a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>L_{OS} \cdot x</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D12b.}</math>
 
| <math>\operatorname{Den}^L \cdot x</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D12c.}</math>
 
| <math>\operatorname{Den}^L |_x</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D12d.}</math>
 
| <math>\operatorname{Den}^L (-, x)</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D12e.}</math>
 
| <math>\operatorname{Den}(L, x)</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D12f.}</math>
 
| <math>\operatorname{Den}(L) \cdot x</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D12g.}</math>
 
| <math>\{ o \in O ~:~ (o, x) \in \operatorname{Den}(L) \}</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D12h.}</math>
 
| <math>\{ o \in O ~:~ (o, x, i) \in L ~\operatorname{for~some}~ i \in I \}</math>
 
|}
 
|}
 
 
<br>
 
 
===Definition 13===
 
 
<br>
 
 
{| 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%" | &nbsp;
 
| width="20%" | <math>\operatorname{Definition~13}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical subsets of}~ S \times I \, :</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:40px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D13a.}</math>
 
| width="80%" style="border-top:1px solid black" | <math>\operatorname{Der}^L</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D13b.}</math>
 
| <math>\operatorname{Der}(L)</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D13c.}</math>
 
| <math>\{ (x, y) \in S \times I ~:~ \operatorname{Den}^L|_x = \operatorname{Den}^L|_y \}</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{D13d.}</math>
 
| <math>\{ (x, y) \in S \times I ~:~ \operatorname{Den}(L, x) = \operatorname{Den}(L, y) \}</math>
 
|}
 
|}
 
 
<br>
 
 
===Fact 2.1===
 
 
<br>
 
 
{| 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:50px; text-align:center"
 
| style="width:80%" | &nbsp;
 
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~2.1}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:50px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="10%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="68%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are identical subsets of}~ S \times I :</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:60px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="10%" style="border-top:1px solid black" | <math>\operatorname{F2.1a.}</math>
 
| width="68%" style="border-top:1px solid black" | <math>\operatorname{Der}^L</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{F2.1a~:~D13a}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.1b.}</math>
 
| valign="top" | <math>\operatorname{Der}(L)</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.1b~:~D13b}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.1c.}</math>
 
| valign="top" |
 
<math>\begin{array}{ll}
 
\{ & (x, y) \in S \times I ~: \\
 
  & \operatorname{Den}(L, x) ~=~ \operatorname{Den}(L, y) \\
 
\} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{F2.1c~:~D13c}</math></p>
 
<p><math>\operatorname{F2.1c~:~R9a}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.1d.}</math>
 
| valign="top" |
 
<math>\begin{array}{ll}
 
\{ & (x, y) \in S \times I ~: \\
 
  & \upharpoonleft \operatorname{Den}(L, x) \upharpoonright ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright \\
 
\} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.1d~:~R9b}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.1e.}</math>
 
| valign="top" |
 
<math>\begin{array}{ll}
 
\{ & (x, y) \in S \times I ~: \\
 
  & \overset{O}{\underset{o}{\forall}}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) \\
 
\} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.1e~:~R9c}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.1f.}</math>
 
| valign="top" |
 
<math>\begin{array}{ll}
 
\{ & (x, y) \in S \times I ~: \\
 
  & \underset{o \in O}{\operatorname{Conj}}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) \\
 
\} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.1f~:~R9d}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.1g.}</math>
 
| valign="top" |
 
<math>\begin{array}{ll}
 
\{ & (x, y) \in S \times I ~: \\
 
  & \underset{o \in O}{\operatorname{Conj}}~ \underline{((}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~,~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) ~\underline{))} \\
 
\} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.1g~:~R9e}</math>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.1h.}</math>
 
| valign="top" |
 
<math>\begin{array}{ll}
 
\{ & (x, y) \in S \times I ~: \\
 
  & \underset{o \in O}{\operatorname{Conj}}~ \underline{((}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright ~,~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright ~\underline{))}^\$ (o) \\
 
\} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{F2.1h~:~R9f}</math></p>
 
<p><math>\operatorname{F2.1h~:~D12e}</math></p>
 
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.1i.}</math>
 
| valign="top" |
 
<math>\begin{array}{ll}
 
\{ & (x, y) \in S \times I ~: \\
 
  & \underset{o \in O}{\operatorname{Conj}}~ \underline{((}~ \upharpoonleft L_{OS} \cdot x \upharpoonright ~,~ \upharpoonleft L_{OS} \cdot y \upharpoonright ~\underline{))}^\$ (o) \\
 
\} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.1i~:~D12a}</math>
 
|}
 
|}
 
 
<br>
 
 
===Fact 2.2===
 
 
====Variant 1====
 
 
<br>
 
 
{| 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:50px; text-align:center"
 
| style="width:80%" | &nbsp;
 
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~2.2}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:50px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="12%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="66%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:10px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="12%" style="border-top:1px solid black" | &nbsp;
 
| width="66%" style="border-top:1px solid black" | &nbsp;
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.2a.}</math>
 
| valign="top" |
 
<math>\begin{array}{cccl}
 
\operatorname{Der}^L
 
& = & \{ & (x, y) \in S \times I ~: \\
 
&  &    & \begin{array}{ccl}
 
          \underset{o \in O}{\operatorname{Conj}} \\
 
          & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 
          & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 
          & ) & \\
 
          \end{array} \\
 
&  & \} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.2a~:~R11a}</math>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.2b.}</math>
 
| valign="top" |
 
<math>\begin{array}{ccccl}
 
\upharpoonleft \operatorname{Der}^L \upharpoonright
 
& = & \upharpoonleft  & \{ & (x, y) \in S \times I ~: \\
 
&  &                &    & \begin{array}{ccl}
 
                            \underset{o \in O}{\operatorname{Conj}} \\
 
                            & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 
                            & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 
                            & ) & \\
 
                            \end{array} \\
 
&  &                & \} & \\
 
&  & \upharpoonright &    & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.2b~:~R11b}</math>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.2c.}</math>
 
| valign="top" |
 
<math>\begin{array}{cccl}
 
\upharpoonleft \operatorname{Der}^L \upharpoonright
 
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
 
&  &    & \begin{array}{cccl}
 
          \downharpoonleft  & \underset{o \in O}{\operatorname{Conj}} \\
 
          &                & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 
          &                & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 
          &                & ) & \\
 
          \downharpoonright &  & \\
 
          \end{array} \\
 
&  & \} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.2c~:~R11c}</math></p>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.2d.}</math>
 
| valign="top" |
 
<math>\begin{array}{cccl}
 
\upharpoonleft \operatorname{Der}^L \upharpoonright
 
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
 
&  &    & \begin{array}{cccl}
 
          \underset{o \in O}{\operatorname{Conj}} \\
 
          & \downharpoonleft  & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 
          &                  & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 
          &                  & ) & \\
 
          & \downharpoonright &  & \\
 
          \end{array} \\
 
&  & \} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.2d~:~Log}</math>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.2e.}</math>
 
| valign="top" |
 
<math>\begin{array}{cccl}
 
\upharpoonleft \operatorname{Der}^L \upharpoonright
 
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
 
&  &    & \begin{array}{ccl}
 
          \underset{o \in O}{\operatorname{Conj}} \\
 
          & \underline{((} & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 
          & ,              & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 
          & \underline{))} & \\
 
          \end{array} \\
 
&  & \} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.2e~:~Log}</math>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.2f.}</math>
 
| valign="top" |
 
<math>\begin{array}{cccl}
 
\upharpoonleft \operatorname{Der}^L \upharpoonright
 
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
 
&  &    & \begin{array}{cll}
 
          \underset{o \in O}{\operatorname{Conj}} \\
 
          & \underline{((}    & \upharpoonleft \operatorname{Den}^L x \upharpoonright \\
 
          & ,                & \upharpoonleft \operatorname{Den}^L y \upharpoonright \\
 
          & \underline{))}^\$ & (o) \\
 
          \end{array} \\
 
&  & \} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.2f~:~$~}</math>
 
|}
 
|}
 
 
<br>
 
 
====Variant 2====
 
 
<br>
 
 
{| 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:50px; text-align:center"
 
| style="width:80%" | &nbsp;
 
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~2.2}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:50px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="10%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="68%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:60px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="78%" style="border-top:1px solid black" |
 
<math>\begin{align}
 
\operatorname{F2.2a.} \quad \operatorname{Der}^L
 
& = & \{ & (x, y) \in S \times I ~: \\
 
&  &    & \underset{o \in O}{\operatorname{Conj}} \, (\upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \, = \, \upharpoonleft \operatorname{Den}^L y \upharpoonright (o)) \\
 
&  & \} & \\
 
\end{align}</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{F2.2a~:~R11a}</math>
 
|- style="height:20px"
 
| colspan="2" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:40px"
 
| &nbsp;
 
| <math>\operatorname{F2.2b.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.2b~:~R11b}</math>
 
|- style="height:20px"
 
| colspan="2" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F2.2c.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.2c~:~R11c}</math></p>
 
|- style="height:20px"
 
| colspan="2" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F2.2d.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.2d~:~Log}</math>
 
|- style="height:20px"
 
| colspan="2" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F2.2e.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.2e~:~Log}</math>
 
|- style="height:20px"
 
| colspan="2" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:60px"
 
| &nbsp;
 
| <math>\operatorname{F2.2f.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<math>\operatorname{F2.2f~:~$~}</math>
 
|}
 
|}
 
 
<br>
 
 
===Fact 2.3===
 
 
<br>
 
 
{| 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:50px; text-align:center"
 
| style="width:80%" | &nbsp;
 
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~2.3}</math>
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:50px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="12%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
| width="66%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:50px"
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{the following are equivalent:}\!</math>
 
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|-
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:10px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="12%" style="border-top:1px solid black" | &nbsp;
 
| width="66%" style="border-top:1px solid black" | &nbsp;
 
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.3a.}</math>
 
| valign="top" |
 
<math>\begin{array}{cccl}
 
\operatorname{Der}^L
 
& = & \{ & (x, y) \in S \times I ~: \\
 
&  &    & \begin{array}{ccl}
 
          \underset{o \in O}{\operatorname{Conj}} \\
 
          & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 
          & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 
          & ) & \\
 
          \end{array} \\
 
&  & \} & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.3a~:~R11a}</math>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.3b.}</math>
 
| valign="top" |
 
<math>\begin{array}{ccccl}
 
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
 
& = & \downharpoonleft  & \underset{o \in O}{\operatorname{Conj}} \\
 
&  &                  & & \begin{array}{cl}
 
                            ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 
                            = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 
                            ) & \\
 
                            \end{array} \\
 
&  & \downharpoonright & & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.3b~:~R11d}</math>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.3c.}</math>
 
| valign="top" |
 
<math>\begin{array}{ccccl}
 
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
 
& = & \underset{o \in O}{\operatorname{Conj}} \\
 
&  & & \begin{array}{ccl}
 
        \downharpoonleft  & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 
                          & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 
                          & ) & \\
 
        \downharpoonright &  & \\
 
        \end{array} \\
 
&  & & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.3c~:~Log}</math></p>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.3d.}</math>
 
| valign="top" |
 
<math>\begin{array}{ccccl}
 
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
 
& = & \underset{o \in O}{\operatorname{Conj}} \\
 
&  & & \begin{array}{ccl}
 
        \downharpoonleft  & ( & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, x) \\
 
                          & = & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, y) \\
 
                          & ) & \\
 
        \downharpoonright &  & \\
 
        \end{array} \\
 
&  & & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.3d~:~Def}</math>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.3e.}</math>
 
| valign="top" |
 
<math>\begin{array}{ccccl}
 
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
 
& = & \underset{o \in O}{\operatorname{Conj}} \\
 
&  & & \begin{array}{cl}
 
        \underline{((} & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, x) \\
 
        ,              & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, y) \\
 
        \underline{))} & \\
 
        \end{array} \\
 
&  & & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" |
 
<p><math>\operatorname{F2.3e~:~Log}</math></p>
 
<p><math>\operatorname{F2.3e~:~D10b}</math></p>
 
|- style="height:20px"
 
| colspan="3" | &nbsp;
 
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
|- style="height:100px"
 
| &nbsp;
 
| valign="top" | <math>\operatorname{F2.3f.}</math>
 
| valign="top" |
 
<math>\begin{array}{ccccl}
 
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
 
& = & \underset{o \in O}{\operatorname{Conj}} \\
 
&  & & \begin{array}{cl}
 
        \underline{((} & \upharpoonleft L_{OS} \upharpoonright (o, x) \\
 
        ,              & \upharpoonleft L_{OS} \upharpoonright (o, y) \\
 
        \underline{))} & \\
 
        \end{array} \\
 
&  & & \\
 
\end{array}</math>
 
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.3f~:~D10a}</math>
 
|}
 
|}
 
  
 
<br>
 
<br>

Revision as of 18:24, 2 September 2010

Greek

  ἐν ἀρχῇ

  Ἐν ἀρχῇ ἦν ὁ λόγος  

Template:Polytonic

Πάτερ ἡμῶν ὁ ἐν τοῖς οὐρανοῖς· ἁγιασθήτω τὸ ὄνομά σου·

Template:Polytonic

ἐλθέτω ἡ βασιλεία σου·

LOGOS

Epigraph Formats


 

'Tis a derivative from me to mine,
And only that I stand for.

  Winter's Tale, 3.2.43–44


 

Out of the dimness opposite equals advance . . . .
     Always substance and increase,
Always a knit of identity . . . . always distinction . . . .
     always a breed of life.

  — Walt Whitman, Leaves of Grass, [Whi, 28]


On either side the river lie
Long fields of barley and of rye,
That clothe the wold and meet the sky;
And thro' the field the road runs by
  To many-tower'd Camelot;
And up and down the people go,
Gazing where the lilies blow
Round an island there below,
  The island of Shalott.
    — Tennyson, The Lady of Shalott, [Ten, 17]


The most valuable insights are arrived at last; but the most valuable insights are methods.

— Nietzsche, The Will to Power, [Nie, S469, 261]


The power of form, the will to give form to oneself. "Happiness" admitted as a goal. Much strength and energy behind the emphasis on forms. The delight in looking at a life that seems so easy. — To the French, the Greeks looked like children.

— Nietzsche, The Will to Power, [Nie, S94, 58]


          In every sort of project there are two things to consider: first, the absolute goodness of the project; in the second place, the facility of execution.

          In the first respect it suffices that the project be acceptable and practicable in itself, that what is good in it be in the nature of the thing; here, for example, that the proposed education be suitable for man and well adapted to the human heart.

          The second consideration depends on relations given in certain situations — relations accidental to the thing, which consequently are not necessary and admit of infinite variety.

— Rousseau, Emile, or On Education, [Rou-1, 34–35]


Division Styles


  1. Able
  2. Baker
  3. Charlie


  1. Able
  2. Baker
  3. Charlie


Blockquote Formats


Now, I ask, how is it that anything can be done with a symbol, without reflecting upon the conception, much less imagining the object that belongs to it? It is simply because the symbol has acquired a nature, which may be described thus, that when it is brought before the mind certain principles of its use — whether reflected on or not — by association immediately regulate the action of the mind; and these may be regarded as laws of the symbol itself which it cannot as a symbol transgress. (Peirce, CE 1, 173).


          The information of a term is the measure of its superfluous comprehension. That is to say that the proper office of the comprehension is to determine the extension of the term. …

          Every addition to the comprehension of a term, lessens its extension up to a certain point, after that further additions increase the information instead. …

          And therefore as every term must have information, every term has superfluous comprehension. And, hence, whenever we make a symbol to express any thing or any attribute we cannot make it so empty that it shall have no superfluous comprehension.

          I am going, next, to show that inference is symbolization and that the puzzle of the validity of scientific inference lies merely in this superfluous comprehension and is therefore entirely removed by a consideration of the laws of information.

(Peirce, CE 1, 467).


a. The theories of the soul (psyche) handed down by our predecessors have been sufficiently discussed; now let us start afresh, as it were, and try to determine (diorisai) what the soul is, and what definition (logos) of it will be most comprehensive (koinotatos).
b. We describe one class of existing things as substance (ousia), and this we subdivide into three: (1) matter (hyle), which in itself is not an individual thing, (2) shape (morphe) or form (eidos), in virtue of which individuality is directly attributed, and (3) the compound of the two.
c. Matter is potentiality (dynamis), while form is realization or actuality (entelecheia), and the word actuality is used in two senses, illustrated by the possession of knowledge (episteme) and the exercise of it (theorein).
d. Bodies (somata) seem to be pre-eminently substances, and most particularly those which are of natural origin (physica), for these are the sources (archai) from which the rest are derived.
e. But of natural bodies some have life (zoe) and some have not; by life we mean the capacity for self-sustenance, growth, and decay.
f. Every natural body (soma physikon), then, which possesses life must be substance, and substance of the compound type (synthete).
g. But since it is a body of a definite kind, viz., having life, the body (soma) cannot be soul (psyche), for the body is not something predicated of a subject, but rather is itself to be regarded as a subject, i.e., as matter.
h. So the soul must be substance in the sense of being the form of a natural body, which potentially has life. And substance in this sense is actuality.
i. The soul, then, is the actuality of the kind of body we have described. But actuality has two senses, analogous to the possession of knowledge and the exercise of it.
j. Clearly (phaneron) actuality in our present sense is analogous to the possession of knowledge; for both sleep (hypnos) and waking (egregorsis) depend upon the presence of the soul, and waking is analogous to the exercise of knowledge, sleep to its possession (echein) but not its exercise (energein).
k. Now in one and the same person the possession of knowledge comes first.
l. The soul may therefore be defined as the first actuality of a natural body potentially possessing life; and such will be any body which possesses organs (organikon).
m. (The parts of plants are organs too, though very simple ones: e.g., the leaf protects the pericarp, and the pericarp protects the seed; the roots are analogous to the mouth, for both these absorb food.)
n. If then one is to find a definition which will apply to every soul, it will be "the first actuality of a natural body possessed of organs".
o. So one need no more ask (zetein) whether body and soul are one than whether the wax (keros) and the impression (schema) it receives are one, or in general whether the matter of each thing is the same as that of which it is the matter; for admitting that the terms unity and being are used in many senses, the paramount (kyrios) sense is that of actuality.
p. We have, then, given a general definition of what the soul is: it is substance in the sense of formula (logos), i.e., the essence of such-and-such a body.
q. Suppose that an implement (organon), e.g. an axe, were a natural body; the substance of the axe would be that which makes it an axe, and this would be its soul; suppose this removed, and it would no longer be an axe, except equivocally. As it is, it remains an axe, because it is not of this kind of body that the soul is the essence or formula, but only of a certain kind of natural body which has in itself a principle of movement and rest.
r. We must, however, investigate our definition in relation to the parts of the body.
s. If the eye were a living creature, its soul would be its vision; for this is the substance in the sense of formula of the eye. But the eye is the matter of vision, and if vision fails there is no eye, except in an equivocal sense, as for instance a stone or painted eye.
t. Now we must apply what we have found true of the part to the whole living body. For the same relation must hold good of the whole of sensation to the whole sentient body qua sentient as obtains between their respective parts.
u. That which has the capacity to live is not the body which has lost its soul, but that which possesses its soul; so seed and fruit are potentially bodies of this kind.
v. The waking state is actuality in the same sense as the cutting of the axe or the seeing of the eye, while the soul is actuality in the same sense as the faculty of the eye for seeing, or of the implement for doing its work.
w. The body is that which exists potentially; but just as the pupil and the faculty of seeing make an eye, so in the other case the soul and body make a living creature.
x. It is quite clear, then, that neither the soul nor certain parts of it, if it has parts, can be separated from the body; for in some cases the actuality belongs to the parts themselves. Not but what there is nothing to prevent some parts being separated, because they are not actualities of any body.
y. It is also uncertain (adelon) whether the soul as an actuality bears the same relation to the body as the sailor (ploter) to the ship (ploion).
z. This must suffice as an attempt to determine in rough outline the nature of the soul.
  (Aristotle, On the Soul, 2.1)


Ordered List Formats

  1. Item 1
    1. Item a
      1. Item i
      2. Item ii
      3. Item iii
    2. Item b
    3. Item c
  2. Item 2
    1. Item a
      1. Item i
      2. Item ii
      3. Item iii
    2. Item b
    3. Item c
  3. Item 3

Outline Formats


Example 1. Modus Ponens
    Information Reducing Inference
     

\(\begin{array}{l} ~ p \Rightarrow q \\ ~ p \\ \overline{~~~~~~~~~~~~~~~} \\ ~ q \end{array}\)

    Information Preserving Inference
     

\(\begin{array}{l} ~ p \Rightarrow q \\ ~ p \\ ='"`UNIQ--h-6--QINU`"'\!=\!=\!=\!=\!=\!=\!= \\ ~ p ~ q \end{array}\)


Example 2. Transitivity
    Information Reducing Inference
     

\(\begin{array}{l} ~ p \le q \\ ~ q \le r \\ \overline{~~~~~~~~~~~~~~~} \\ ~ p \le r \end{array}\)

    Information Preserving Inference
     

\(\begin{array}{l} ~ p \le q \\ ~ q \le r \\ ='"`UNIQ--h-7--QINU`"'\!=\!=\!=\!=\!=\!=\!= \\ ~ p \le q \le r \end{array}\)


Transitive Law (Implicational Inference)
   

\(\begin{array}{l} ~ p \le q \\ ~ q \le r \\ \overline{~~~~~~~~~~~~~~~} \\ ~ p \le r \end{array}\)

By itself, the information \(p \le q\) would reduce our uncertainty from \(\log 8\!\) bits to \(\log 6\!\) bits.
By itself, the information \(q \le r\) would reduce our uncertainty from \(\log 8\!\) bits to \(\log 6\!\) bits.
By itself, the information \(p \le r\) would reduce our uncertainty from \(\log 8\!\) bits to \(\log 6\!\) bits.


Transitive Law (Equational Inference)
   

\(\begin{array}{l} ~ p \le q \\ ~ q \le r \\ ='"`UNIQ--h-8--QINU`"'\!=\!=\!=\!=\!=\!=\!= \\ ~ p \le q \le r \end{array}\)

The contents and the measures of information that are associated with the propositions \(p \le q\) and \(q \le r\) are the same as before.
On its own, the information \(p \le q \le r\) would reduce our uncertainty from log(8) = 3 bits to log(4) = 2 bits, a reduction of 1 bit.


Mathematical Symbols

\(-<\!\) -<
\(-\!<\) -\!<
\(-\!\!<\) -\!\!<
\(-\!\!\!<\) -\!\!\!<
\(\curlyvee\) \curlyvee
\(\curlywedge\) \curlywedge
\(\lessdot\) \lessdot
\(\gtrdot\) \gtrdot
\(:\!\lessdot\) :\!\lessdot
\(:\!\gtrdot\) :\!\gtrdot
\(\colon\!\lessdot\) \colon\!\lessdot
\(\colon\!\gtrdot\) \colon\!\gtrdot
\(\And\) \And
\(\dagger\) \dagger
\(\ddagger\) \ddagger
\(\lVert\) \lVert
\(\rVert\) \rVert
\(\parallel\) \parallel
\(\P\) \P
\(\S\) \S
\($\) $ NB. Idiosyntax of WikiTeX
\($\!\) $\! NB. Idiosyntax of WikiTeX
\(\$\) \$ NB. Standard Syntax in LaTeX
\(\mathfrak{g}_{\dagger\ddagger} \, ^\dagger\mathit{l}_\parallel \, ^\parallel\mathrm{w} \, ^\ddagger\mathrm{h}\)
\(\mathfrak{g}_{\dagger\ddagger} {}^\dagger\mathit{l}_\parallel {}^\parallel\mathrm{w} {}^\ddagger\mathrm{h}\)
\(\mathfrak{g}_{\dagger\ddagger} {}^\dagger\!\mathit{l}_\parallel {}^\parallel\!\mathrm{w} {}^\ddagger\!\mathrm{h}\)

Cactus TeX


\(\begin{array}{l} \texttt{ } \\ \texttt{~} \\ \texttt{()} \\ \texttt{(~)} \\ \texttt{(( ))} \\ \texttt{( )( )} \\ \texttt{a b c} \\ \texttt{a~b~c} \\ \texttt{a(a)~=~(~)} \\ \texttt{a((b)(c))~=~((ab)(ac))} \\ \end{array}\)


\(\begin{array}{l} \texttt{d}^2 \texttt{x} \\ \texttt{d}^\text{2} \texttt{x} \\ \texttt{d}^\texttt{2} \texttt{x} \\ \end{array}\)


\(\texttt{uv~(du~dv) ~+~ u(v)~(du (dv)) ~+~ (u)v~((du) dv) ~+~ (u)(v)~((du)(dv))}\)


\(\texttt{uv} \cdot \texttt{(du~dv)} + \texttt{u(v)} \cdot \texttt{(du (dv))} + \texttt{(u)v} \cdot \texttt{((du) dv)} + \texttt{(u)(v)} \cdot \texttt{((du)(dv))}\)


\(\begin{matrix} \bar{(} \ldots \bar{)} & \bar{|} \ldots \bar{|} \\ \\ \dot{(} \ldots \dot{)} & \dot{|} \ldots \dot{|} \\ \\ \hat{(} \ldots \hat{)} & \hat{|} \ldots \hat{|} \\ \\ \check{(} \ldots \check{)} & \check{|} \ldots \check{|} \\ \\ \tilde{(} \ldots \tilde{)} & \tilde{|} \ldots \tilde{|} \\ \\ \downharpoonleft \ldots \downharpoonright & \upharpoonleft \ldots \upharpoonright \\ \\ \overline{(} \ldots \overline{)} & \overline{|} \ldots \overline{|} \\ \\ \underline{(} \ldots \underline{)} & \underline{|} \ldots \underline{|} \\ \\ \overline{\underline{(}} \ldots \overline{\underline{)}} & \overline{\underline{|}} \ldots \overline{\underline{|}} \\ \\ \end{matrix}\)

\(\begin{array}{lllll} {}^{_\sim}\!X & = & U - X & = & \{ \, u \in U : \underline{(} u \in X \underline{)} \, \}. \end{array}\)

\(\begin{array}{lllll} {}^{_\sim}\!X & = & U - X & = & \{ \, u \in U : \tilde{(} u \in X \tilde{)} \, \}. \end{array}\)

\[X = \{\ (\!|u|\!)(\!|v|\!),\ (\!|u|\!) v,\ u (\!|v|\!),\ u v\ \} \cong \mathbb{B}^2.\]
\[X = \{\ \underline{(u)(v)},\ \underline{(u)~v},\ \underline{u~(v)},\ \underline{u~v}\ \} \cong \mathbb{B}^2.\]
\[X = \{\!\] (u)(v)\(,\) (u)v\(,\) u(v)\(,\) uv \(\} \cong \mathbb{B}^2.\)
\[X = \{\!\] (u)(v) \(,\) (u)v \(,\) u(v) \(,\) uv \(\} \cong \mathbb{B}^2.\)
\(X = \{\!\) (u)(v) \(,\) (u)v \(,\) u(v) \(,\) uv \(\} \cong \mathbb{B}^2.\)
\(X = \{\!\) (u)(v) , (u)v ,  u(v) , uv \(\} \cong \mathbb{B}^2.\)


Examples of Logical Orbits

Version 1

\(\begin{array}{ccc} \texttt{u}' & = & \texttt{((u)(v))} \\ \texttt{v}' & = & \texttt{((u,~v))} \end{array}\)

\(\begin{matrix} \text{Orbit 1} \\ \text{Initial Point :}~ (u, v) = (1, 1) \end{matrix}\)

\(\begin{array}{c|cc} t & u & v \\ \\ 0 & 1 & 1 \\ 1 & 1 & 1 \\ 2 & '' & '' \\ \end{array}\)

\(\begin{matrix} \text{Orbit 2} \\ \text{Initial Point :}~ (u, v) = (0, 0) \end{matrix}\)

\(\begin{array}{c|cc} t & u & v \\ \\ 0 & 0 & 0 \\ 1 & 0 & 1 \\ 2 & 1 & 0 \\ 3 & 1 & 0 \\ 4 & '' & '' \\ \end{array}\)

Version 2

\(\text{Orbit 1. Intitial Point :}~ (u, v) = (1, 1)\)

\(\begin{array}{c|cc|cc|cc|cc|cc|c} t & u & v & du & dv & d^2 u & d^2 v & d^3 u & d^3 v & d^4 u & d^4 v & \ldots \\ \\ 0 & 1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 4 & '' & '' & '' & '' & '' & '' & '' & '' & '' & '' & \ldots \\ \end{array}\)

\(\text{Orbit 2. Intitial Point :}~ (u, v) = (0, 0)\)

\(\begin{array}{c|cc|cc|cc|cc|cc|c} t & u & v & du & dv & d^2 u & d^2 v & d^3 u & d^3 v & d^4 u & d^4 v & \ldots \\ \\ 0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 & 1 & 1 & 0 & \ldots \\ 1 & 0 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & \ldots \\ 2 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 3 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 4 & '' & '' & '' & '' & '' & '' & '' & '' & '' & '' & \ldots \\ \end{array}\)

Version 3

\(\text{Orbit 1}\!\)

\(\begin{array}{c|cc|cc|} t & u & v & du & dv \\[8pt] 0 & 1 & 1 & 0 & 0 \\ 1 & '' & '' & '' & '' \\ \end{array}\)

 
\(\text{Orbit 2}\!\)

\(\begin{array}{c|cc|cc|cc|} t & u & v & du & dv & d^2 u & d^2 v \\[8pt] 0 & 0 & 0 & 0 & 1 & 1 & 0 \\ 1 & 0 & 1 & 1 & 1 & 1 & 1 \\ 2 & 1 & 0 & 0 & 0 & 0 & 0 \\ 3 & '' & '' & '' & '' & '' & '' \\ \end{array}\)

Type Markers

Composer P

\(\begin{array}{l} ((x \underset{A}{:} ~y \overset{B}{\underset{A}{:}}) \underset{B}{:} ~z \overset{C}{\underset{B}{:}}) \underset{C}{:} \end{array}\)

\(\begin{array}{l} ((x \overset{A}{:} ~y \overset{B}{\underset{A}{:}}) \overset{B}{:} ~z \overset{C}{\underset{B}{:}}) \overset{C}{:} \end{array}\)

\(\begin{array}{l} ((x \overset{A}{\Uparrow} ~y \overset{B}{\underset{A}{\Uparrow}}) \overset{B}{\Uparrow} ~z \overset{C}{\underset{B}{\Uparrow}}) \overset{C}{\Uparrow} \end{array}\)

\(\begin{array}{l} ((x \underset{A}{\Downarrow} ~y \overset{A}{\underset{B}{\Downarrow}}) \underset{B}{\Downarrow} ~z \overset{B}{\underset{C}{\Downarrow}}) \underset{C}{\Downarrow} \end{array}\)

\(\begin{array}{l} ((x \overset{ }{\underset{A}{\Downarrow}} ~ y \overset{A}{\underset{B}{\Downarrow}} ) \overset{ }{\underset{B}{\Downarrow}} ~ z \overset{B}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ (x \overset{ }{\underset{A}{\Downarrow}} ~ (y \overset{A}{\underset{B}{\Downarrow}} ~ (z \overset{B}{\underset{C}{\Downarrow}} ~ P \overset{B \Rightarrow C}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}} ) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}} ) \overset{A}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \end{array}\)

Transposer T

\(\begin{array}{l} (y \overset{ }{\underset{B}{\Downarrow}} ~ (x \overset{ }{\underset{A}{\Downarrow}} ~ z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ) \overset{B}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ (x \overset{ }{\underset{A}{\Downarrow}} ~ (y \overset{ }{\underset{B}{\Downarrow}} ~ (z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~ T \overset{A \Rightarrow (B \Rightarrow C)}{\underset{B \Rightarrow (A \Rightarrow C)}{\Downarrow}} ) \overset{B}{\underset{A \Rightarrow C}{\Downarrow}} ) \overset{A}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \end{array}\)

Proof Example

\(\begin{array}{l} (y \overset{ }{\underset{B}{\Downarrow}} ~ (x \overset{ }{\underset{A}{\Downarrow}} ~ z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ) \overset{B}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ ((x \overset{ }{\underset{A}{\Downarrow}} ~ (y \overset{ }{\underset{B}{\Downarrow}} ~ K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}} ) \overset{A}{\underset{B}{\Downarrow}} ) \overset{ }{\underset{B}{\Downarrow}} ~ (x \overset{ }{\underset{A}{\Downarrow}} ~ z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ) \overset{B}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ (x \overset{ }{\underset{A}{\Downarrow}} ~ ((y \overset{ }{\underset{B}{\Downarrow}} ~ K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}} ) \overset{A}{\underset{B}{\Downarrow}} ~ (z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~ S \overset{A \Rightarrow (B \Rightarrow C)}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}} ) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}} ) \overset{A}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ \ldots \end{array}\)

Over And Under Setting

  1. The conjunction \(\overset{J}{\underset{j}{\operatorname{Conj}}}\ q_j\) of a set of propositions, \(\{ q_j : j \in J \},\) is a proposition that is true if and only if every one of the \(q_j\!\) is true.

    \(\overset{J}{\underset{j}{\operatorname{Conj}}}\ q_j\) is true  \(\Leftrightarrow\)  \(q_j\!\) is true for every \(j \in J.\)

  2. The surjunction \(\overset{J}{\underset{j}{\operatorname{Surj}}}\ q_j\) of a set of propositions, \(\{ q_j : j \in J \},\) is a proposition that is true if and only if exactly one of the \(q_j\!\) is untrue.

    \(\overset{J}{\underset{j}{\operatorname{Surj}}}\ q_j\) is true  \(\Leftrightarrow\)  \(q_j\!\) is untrue for unique \(j \in J.\)

Equation Sequences

\(\begin{array}{lll} [| \downharpoonleft s \downharpoonright |] & = & [| F |] \\[6pt] & = & F^{-1} (\underline{1}) \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ s ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ F(x, y) = \underline{1} ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ F(x, y) ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \underline{(}~x~,~y~\underline{)} = \underline{1} ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \underline{(}~x~,~y~\underline{)} ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x ~\operatorname{exclusive~or}~ y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \operatorname{just~one~true~of}~ x, y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x ~\operatorname{not~equal~to}~ y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x \nLeftrightarrow y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x \neq y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x + y ~\}. \end{array}\)

\(\begin{array}{lll} [| F^\$ (p, q) |] & = & [| \underline{(}~p~,~q~\underline{)}^\$ |] \\[6pt] & = & (F^\$ (p, q))^{-1} (\underline{1}) \\[6pt] & = & \{~ x \in X ~:~ F^\$ (p, q)(x) ~\} \\[6pt] & = & \{~ x \in X ~:~ \underline{(}~p~,~q~\underline{)}^\$ (x) ~\} \\[6pt] & = & \{~ x \in X ~:~ \underline{(}~p(x)~,~q(x)~\underline{)} ~\} \\[6pt] & = & \{~ x \in X ~:~ p(x) + q(x) ~\} \\[6pt] & = & \{~ x \in X ~:~ p(x) \neq q(x) ~\} \\[6pt] & = & \{~ x \in X ~:~ \upharpoonleft P \upharpoonright (x) ~\neq~ \upharpoonleft Q \upharpoonright (x) ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P ~\nLeftrightarrow~ x \in Q ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P\!-\!Q ~\operatorname{or}~ x \in Q\!-\!P ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P\!-\!Q ~\cup~ Q\!-\!P ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P + Q ~\} \\[6pt] & = & P + Q ~\subseteq~ X \\[6pt] & = & [|p|] + [|q|] ~\subseteq~ X \end{array}\)

Multiline TeX Formats


\( \begin{cases} a \\ b \\ c \\ \begin{cases} d \\ e \\ f \\ \end{cases} \\ g \\ h \\ i \\ \end{cases} \)


\(\begin{alignat}{2} x & = (y - z)(y + z) \\ & = y^2 - z^2 \\ \end{alignat}\)


\(\begin{align} \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & \begin{align} \underset{o \in O}{\operatorname{Conj}} \\ & \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) & = \\ & \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) & \\ \end{align} \\ & & \} & \\ \end{align}\)


\(\begin{align} \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & \underset{o \in O}{\operatorname{Conj}}~ (\upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o)) \\ & & \} & \\ \end{align}\)


\(\begin{align} \operatorname{F2.2a.} \quad \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & \underset{o \in O}{\operatorname{Conj}}~ (\upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o)) \\ & & \} & \\ \end{align}\)


\(\begin{array}{lllll} \operatorname{F2.2a.} & \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & & \underset{o \in O}{\operatorname{Conj}}~ (\upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o)) \\ & & & \} & \\ \end{array}\)