| 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%" |
| |
| − | | style="width:20%; border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:50px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="12%" style="border-top:1px solid black" |
| |
| − | | width="66%" style="border-top:1px solid black" |
| |
| − | | width="20%" style="border-top:1px solid black; border-left:1px solid black" |
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:10px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="12%" style="border-top:1px solid black" |
| |
| − | | width="66%" style="border-top:1px solid black" |
| |
| − | | width="20%" style="border-top:1px solid black; border-left:1px solid black" |
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | valign="top" |
| |
| − | | valign="top" |
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | |- style="height:20px"
| |
| − | | colspan="3" |
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | valign="top" |
| |
| − | | valign="top" |
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | |- style="height:20px"
| |
| − | | colspan="3" |
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | valign="top" |
| |
| − | | valign="top" |
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | |- style="height:20px"
| |
| − | | colspan="3" |
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | valign="top" |
| |
| − | | valign="top" |
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | |- style="height:20px"
| |
| − | | colspan="3" |
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | valign="top" |
| |
| − | | valign="top" |
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | |- style="height:20px"
| |
| − | | colspan="3" |
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | valign="top" |
| |
| − | | valign="top" |
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | |}
| |
| − | |}
| |
| − |
| |
| − | <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%" |
| |
| − | | width="18%" |
| |
| − | | width="60%" |
| |
| − | | align="center" width="20%" | <math>\text{Definition 1}\!</math>
| |
| − | |- style="height:40px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}</math>
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{such that:}\!</math>
| |
| − | |
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{such that:}\!</math>
| |
| − | |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\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%" |
| |
| − | | width="18%" |
| |
| − | | width="60%" |
| |
| − | | align="center" width="20%" | <math>\text{Rule 1}\!</math>
| |
| − | |- style="height:40px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}</math>
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{and if}\!</math>
| |
| − | | <math>x \in X</math>
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{R1b.}\!</math>
| |
| − | | <math>\upharpoonleft Q \upharpoonright (x)</math>
| |
| − | |
| |
| − | |}
| |
| − |
| |
| − | <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%" |
| |
| − | | width="18%" |
| |
| − | | width="60%" |
| |
| − | | align="center" width="20%" | <math>\text{Rule 2}\!</math>
| |
| − | |- style="height:40px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>x \in X</math>
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{R2b.}\!</math>
| |
| − | | <math>f(x) = \underline{1}</math>
| |
| − | |
| |
| − | |}
| |
| − |
| |
| − | <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%" |
| |
| − | | width="18%" |
| |
| − | | width="60%" |
| |
| − | | align="center" style="border-left:1px solid black" width="20%" | <math>\text{Rule 3}\!</math>
| |
| − | |- style="height:40px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>x \in X</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |- style="height:36px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:36px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:36px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>x ~\in~ X</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\operatorname{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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | width="18%" |
| |
| − | | width="60%" |
| |
| − | | align="center" style="border-left:1px solid black" width="20%" |
| |
| − | <math>\text{Corollary 1}\!</math>
| |
| − | |- style="height:40px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>x \in X</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following statement is true:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |- style="height:40px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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%" |
| |
| − | | width="18%" |
| |
| − | | width="60%" |
| |
| − | | align="center" width="20%" | <math>\text{Rule 4}\!</math>
| |
| − | |- style="height:40px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>x \in X ~\text{is varied}</math>
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | | style="border-top:1px solid black" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{R4b.}\!</math>
| |
| − | | <math>\downharpoonleft x \in Q \downharpoonright</math>
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{R4c.}\!</math>
| |
| − | | <math>\downharpoonleft x \in Q \downharpoonright (x)</math>
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{R4d.}\!</math>
| |
| − | | <math>\upharpoonleft Q \upharpoonright (x)</math>
| |
| − | |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{R4e.}\!</math>
| |
| − | | <math>\upharpoonleft Q \upharpoonright (x) = \underline{1}</math>
| |
| − | |
| |
| − | |}
| |
| − |
| |
| − | <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%" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:48px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>p_j ~\text{is a proposition about things in the universe X}</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <math>\text{such that:}\!</math>
| |
| − | |
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <math>\text{L0a.}\!</math>
| |
| − | | <math>\downharpoonleft s_j \downharpoonright ~=~ p_j, ~\text{for all}~ j \in J,</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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%" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:48px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>p ~\text{is a proposition} ~:~ X \to \underline\mathbb{B}</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <math>\text{such that:}\!</math>
| |
| − | |
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <math>\text{L1a.}\!</math>
| |
| − | | <math>\downharpoonleft s \downharpoonright ~=~ p</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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%" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:48px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>p ~:~ X \to \underline\mathbb{B}</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <math>\text{such that:}\!</math>
| |
| − | |
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <math>\text{G1a.}\!</math>
| |
| − | | <math>\upharpoonleft Q \upharpoonright ~=~ p</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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%" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:48px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>p, q ~\text{are propositions} ~:~ X \to \underline\mathbb{B}</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <math>\text{such that:}\!</math>
| |
| − | |
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <math>\text{L2a.}\!</math>
| |
| − | | <math>\downharpoonleft s \downharpoonright ~=~ p \quad \operatorname{and} \quad \downharpoonleft t \downharpoonright ~=~ q</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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%" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:48px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>p, q ~:~ X \to \underline\mathbb{B}</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <math>\text{such that:}\!</math>
| |
| − | |
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <math>\text{G2a.}\!</math>
| |
| − | | <math>\upharpoonleft P \upharpoonright ~=~ p \quad \operatorname{and} \quad \upharpoonleft Q \upharpoonright ~=~ q</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | | 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%" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:48px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | | <math>\downharpoonleft v = w \downharpoonright ~\text{is a proposition} ~:~ \underline\mathbb{B}^2 \to \underline\mathbb{B},</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{V1b.}\!</math>
| |
| − | | <math>\downharpoonleft v \Leftrightarrow w \downharpoonright (v, w)</math>
| |
| − | |- style="height:56px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:48px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{V1b.}\!</math>
| |
| − | | <math>v \Leftrightarrow w</math>
| |
| − | |- style="height:56px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:48px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{V1b.}\!</math>
| |
| − | | <math>\downharpoonleft v \Leftrightarrow w \downharpoonright</math>
| |
| − | |- style="height:56px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:48px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>x ~\in~ X</math>
| |
| − | |- style="height:48px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{V1b.}\!</math>
| |
| − | | <math>\downharpoonleft f(x) ~\Leftrightarrow~ g(x) \downharpoonright</math>
| |
| − | |- style="height:56px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:48px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{V1b.}\!</math>
| |
| − | | <math>\downharpoonleft f ~\Leftrightarrow~ g \downharpoonright</math>
| |
| − | |- style="height:56px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:50px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>x ~\in~ X</math>
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | width="14%" style="border-top:1px solid black" |
| |
| − | | width="64%" style="border-top:1px solid black" |
| |
| − | | width="20%" style="border-top:1px solid black; border-left:1px solid black" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |}
| |
| − |
| |
| − | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | | <math>\text{is a sentence about things in the universe}~ X~</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\operatorname{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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:80px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\operatorname{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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~7}</math>
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
| |
| − | | width="60%" style="border-top:1px solid black" | <math>p, q ~:~ X \to \underline\mathbb{B}</math>
| |
| − | | width="20%" style="border-top:1px solid black; border-left:1px solid black" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\operatorname{R7a.}</math>
| |
| − | | width="60%" style="border-top:1px solid black" | <math>p ~=~ q</math>
| |
| − | | width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R7a~:~R6a}</math>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <math>\operatorname{R7b.}</math>
| |
| − | | <math>\overset{X}{\underset{x}{\forall}}~ (p(x) ~=~ q(x))</math>
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R7b~:~R6b}</math>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <math>\operatorname{R7c.}</math>
| |
| − | | <math>\operatorname{Conj_x^X}~ (p(x) ~=~ q(x))</math>
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | <p><math>\operatorname{R7c~:~R6c}</math></p>
| |
| − | <p><math>\operatorname{R7c~:~P1a}</math></p>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{R7d.}</math>
| |
| − | | <math>\operatorname{Conj_x^X}~ (p(x) ~\Leftrightarrow~ q(x))</math>
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R7d~:~P1b}</math>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <math>\operatorname{R7e.}</math>
| |
| − | | <math>\operatorname{Conj_x^X}~ \underline{((}~ p(x) ~,~ q(x) ~\underline{))}</math>
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | <p><math>\operatorname{R7e~:~P1c}</math></p>
| |
| − | <p><math>\operatorname{R7e~:~$1a}</math></p>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{R7f.}</math>
| |
| − | | <math>\operatorname{Conj_x^X}~ \underline{((}~ p ~,~ q ~\underline{))}^\$ (x)</math>
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R7f~:~$1b}</math>
| |
| − | |}
| |
| − | |}
| |
| − |
| |
| − | <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%" |
| |
| − | | width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~8}</math>
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
| |
| − | | width="60%" style="border-top:1px solid black" | <math>s, t ~\text{are sentences about things in}~ X</math>
| |
| − | | width="20%" style="border-top:1px solid black; border-left:1px solid black" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\operatorname{R8a.}</math>
| |
| − | | width="60%" style="border-top:1px solid black" | <math>s ~\Leftrightarrow~ t</math>
| |
| − | | width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" |
| |
| − | <math>\operatorname{R8a~:~D7a}</math>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <math>\operatorname{R8b.}</math>
| |
| − | | <math>\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright</math>
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | <p><math>\operatorname{R8b~:~D7b}</math></p>
| |
| − | <p><math>\operatorname{R8b~:~R7a}</math></p>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <math>\operatorname{R8c.}</math>
| |
| − | | <math>\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))</math>
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8c~:~R7b}</math>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{R8d.}</math>
| |
| − | | <math>\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))</math>
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8d~:~R7c}</math>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{R8e.}</math>
| |
| − | | <math>\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft t \downharpoonright (x))</math>
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8e~:~R7d}</math>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <math>\operatorname{R8f.}</math>
| |
| − | | <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright (x) ~,~ \downharpoonleft t \downharpoonright (x) ~\underline{))}</math>
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8f~:~R7e}</math>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{R8g.}</math>
| |
| − | | <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright ~\underline{))}^\$ (x)</math>
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8g~:~R7f}</math>
| |
| − | |}
| |
| − | |}
| |
| − |
| |
| − | <br>
| |
| − |
| |
| − | ===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%" |
| |
| − | | 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" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\operatorname{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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\operatorname{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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\operatorname{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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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%" |
| |
| − | | 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" |
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:60px"
| |
| − | | style="width:2%; border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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%" |
| |
| − | | 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" |
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:60px"
| |
| − | | style="width:2%; border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\operatorname{D8b.}</math>
| |
| − | | <math>\operatorname{Con}^L</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{D8c.}</math>
| |
| − | | <math>\operatorname{Con}(L)</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{D8d.}</math>
| |
| − | | <math>\operatorname{proj}_{SI}(L)</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\operatorname{D9b.}</math>
| |
| − | | <math>\overset{\smile}{L_{SI}}</math>
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\operatorname{D9c.}</math>
| |
| − | | <math>\overset{\smile}{\operatorname{Con}^L}</math>
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\operatorname{D9d.}</math>
| |
| − | | <math>\overset{\smile}{\operatorname{Con}(L)}</math>
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\operatorname{D9e.}</math>
| |
| − | | <math>\operatorname{proj}_{IS}(L)</math>
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\operatorname{D9f.}</math>
| |
| − | | <math>\operatorname{Conv}(\operatorname{Con}(L))</math>
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\operatorname{D10b.}</math>
| |
| − | | <math>\operatorname{Den}^L</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{D10c.}</math>
| |
| − | | <math>\operatorname{Den}(L)</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{D10d.}</math>
| |
| − | | <math>\operatorname{proj}_{OS}(L)</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\operatorname{D11b.}</math>
| |
| − | | <math>\overset{\smile}{L_{OS}}</math>
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\operatorname{D11c.}</math>
| |
| − | | <math>\overset{\smile}{\operatorname{Den}^L}</math>
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\operatorname{D11d.}</math>
| |
| − | | <math>\overset{\smile}{\operatorname{Den}(L)}</math>
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\operatorname{D11e.}</math>
| |
| − | | <math>\operatorname{proj}_{SO}(L)</math>
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\operatorname{D11f.}</math>
| |
| − | | <math>\operatorname{Conv}(\operatorname{Den}(L))</math>
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\text{and}\!</math>
| |
| − | | <math>x ~\in~ S</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\operatorname{D12b.}</math>
| |
| − | | <math>\operatorname{Den}^L \cdot x</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{D12c.}</math>
| |
| − | | <math>\operatorname{Den}^L |_x</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{D12d.}</math>
| |
| − | | <math>\operatorname{Den}^L (-, x)</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{D12e.}</math>
| |
| − | | <math>\operatorname{Den}(L, x)</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{D12f.}</math>
| |
| − | | <math>\operatorname{Den}(L) \cdot x</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{D12g.}</math>
| |
| − | | <math>\{ o \in O ~:~ (o, x) \in \operatorname{Den}(L) \}</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <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" |
| |
| − | | 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"
| |
| − | |
| |
| − | | <math>\operatorname{D13b.}</math>
| |
| − | | <math>\operatorname{Der}(L)</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{D13c.}</math>
| |
| − | | <math>\{ (x, y) \in S \times I ~:~ \operatorname{Den}^L|_x = \operatorname{Den}^L|_y \}</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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" |
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are identical subsets of}~ S \times I :</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:60px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | 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"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | 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%" |
| |
| − | | 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" |
| |
| − | | 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" |
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:10px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="12%" style="border-top:1px solid black" |
| |
| − | | width="66%" style="border-top:1px solid black" |
| |
| − | | width="20%" style="border-top:1px solid black; border-left:1px solid black" |
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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%" |
| |
| − | | 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" |
| |
| − | | 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" |
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:60px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | 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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <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%" |
| |
| − | | 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" |
| |
| − | | 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" |
| |
| − | |- style="height:50px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:10px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="12%" style="border-top:1px solid black" |
| |
| − | | width="66%" style="border-top:1px solid black" |
| |
| − | | width="20%" style="border-top:1px solid black; border-left:1px solid black" |
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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" |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:100px"
| |
| − | |
| |
| − | | 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> |