# User:Jon Awbrey/BOX

## Formal Grammars

 $$\mathfrak{C} (\mathfrak{P}) : \text{Grammar 1}\!$$ $$\mathfrak{Q} = \varnothing$$ $$\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}$$

 $$\mathfrak{C} (\mathfrak{P}) : \text{Grammar 2}\!$$ $$\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}$$ $$\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}$$

 $$\mathfrak{C} (\mathfrak{P}) : \text{Grammar 3}\!$$ $$\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, F \, ^{\prime\prime}, \, ^{\backprime\backprime} \, R \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}$$ $$\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}$$

 $$\mathfrak{C} (\mathfrak{P}) : \text{Grammar 4}\!$$ $$\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T' \, ^{\prime\prime} \, \}$$ $$\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}$$

 $$\mathfrak{C} (\mathfrak{P}) : \text{Grammar 5}\!$$ $$\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}$$ $$\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}$$

 $$\mathfrak{C} (\mathfrak{P}) : \text{Grammar 6}\!$$ $$\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, F \, ^{\prime\prime}, \, ^{\backprime\backprime} \, R \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}$$ $$\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}$$

## Proof Schemata

### Definition 1

#### Variant 1

 $$\text{Definition 1}\!$$ $$\text{If}\!$$ $$Q \subseteq X$$ $$\text{then}\!$$ $$\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}$$ $$\text{such that:}\!$$ $$\text{D1a.}\!$$ $$\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ x \in Q$$ $$\forall x \in X$$

#### Variant 2

 $$\text{Definition 1}\!$$
 $$\text{If}\!$$ $$Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}$$ $$\text{such that:}\!$$
 $$\operatorname{D1a.}$$ $$\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ x \in Q$$ $$\forall x \in X$$

### Rule 1

 $$\text{Rule 1}\!$$ $$\text{If}\!$$ $$Q \subseteq X$$ $$\text{then}\!$$ $$\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}$$ $$\text{and if}\!$$ $$x \in X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$ $$\text{R1a.}\!$$ $$x \in Q$$ $$\text{R1b.}\!$$ $$\upharpoonleft Q \upharpoonright (x)$$

### Rule 2

 $$\text{Rule 2}\!$$ $$\text{If}\!$$ $$f : X \to \underline\mathbb{B}$$ $$\text{and}\!$$ $$x \in X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$ $$\text{R2a.}\!$$ $$f(x)\!$$ $$\text{R2b.}\!$$ $$f(x) = \underline{1}$$

### Rule 3

#### Variant 1

 $$\text{Rule 3}\!$$ $$\text{If}\!$$ $$Q \subseteq X$$ $$\text{and}\!$$ $$x \in X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$ $$\text{R3a.}\!$$ $$x \in Q$$ $$\text{R3a : R1a}\!$$ $$::\!$$ $$\text{R3b.}\!$$ $$\upharpoonleft Q \upharpoonright (x)$$ $$\text{R3b : R1b}\!$$ $$\text{R3b : R2a}\!$$ $$::\!$$ $$\text{R3c.}\!$$ $$\upharpoonleft Q \upharpoonright (x) = \underline{1}$$ $$\text{R3c : R2b}\!$$

#### Variant 2

 $$\operatorname{Rule~3}$$
 $$\text{If}\!$$ $$Q ~\subseteq~ X$$ $$\text{and}\!$$ $$x ~\in~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{R3a.}$$ $$x ~\in~ Q$$ $$\operatorname{R3a~:~R1a}$$ $$::\!$$ $$\operatorname{R3b.}$$ $$\upharpoonleft Q \upharpoonright (x)$$ $$\operatorname{R3b~:~R1b}$$ $$\operatorname{R3b~:~R2a}$$ $$::\!$$ $$\operatorname{R3c.}$$ $$\upharpoonleft Q \upharpoonright (x) ~=~ \underline{1}$$ $$\operatorname{R3c~:~R2b}$$

### Corollary 1

 $$\text{Corollary 1}\!$$ $$\text{If}\!$$ $$Q \subseteq X$$ $$\text{and}\!$$ $$x \in X$$ $$\text{then}\!$$ $$\text{the following statement is true:}\!$$ $$\text{C1a.}\!$$ $$x \in Q ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x) = \underline{1}$$ $$\text{R3a} \Leftrightarrow \text{R3c}$$

### Rule 4

 $$\text{Rule 4}\!$$ $$\text{If}\!$$ $$Q \subseteq X ~\text{is fixed}$$ $$\text{and}\!$$ $$x \in X ~\text{is varied}$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$ $$\text{R4a.}\!$$ $$x \in Q$$ $$\text{R4b.}\!$$ $$\downharpoonleft x \in Q \downharpoonright$$ $$\text{R4c.}\!$$ $$\downharpoonleft x \in Q \downharpoonright (x)$$ $$\text{R4d.}\!$$ $$\upharpoonleft Q \upharpoonright (x)$$ $$\text{R4e.}\!$$ $$\upharpoonleft Q \upharpoonright (x) = \underline{1}$$

## Translation Rules

### Logical Translation Rule 0

 $$\text{Logical Translation Rule 0}\!$$
 $$\text{If}\!$$ $$s_j ~\text{is a sentence about things in the universe X}$$ $$\text{and}\!$$ $$p_j ~\text{is a proposition about things in the universe X}$$ $$\text{such that:}\!$$ $$\text{L0a.}\!$$ $$\downharpoonleft s_j \downharpoonright ~=~ p_j, ~\text{for all}~ j \in J,$$ $$\text{then}\!$$ $$\text{the following equations are true:}\!$$
 $$\text{L0b.}\!$$ $$\downharpoonleft \operatorname{Conc}_j^J s_j \downharpoonright$$ $$=\!$$ $$\operatorname{Conj}_j^J \downharpoonleft s_j \downharpoonright$$ $$=\!$$ $$\operatorname{Conj}_j^J p_j$$ $$\text{L0c.}\!$$ $$\downharpoonleft \operatorname{Surc}_j^J s_j \downharpoonright$$ $$=\!$$ $$\operatorname{Surj}_j^J \downharpoonleft s_j \downharpoonright$$ $$=\!$$ $$\operatorname{Surj}_j^J p_j$$

### Logical Translation Rule 1

 $$\text{Logical Translation Rule 1}\!$$
 $$\text{If}\!$$ $$s ~\text{is a sentence about things in the universe X}$$ $$\text{and}\!$$ $$p ~\text{is a proposition} ~:~ X \to \underline\mathbb{B}$$ $$\text{such that:}\!$$ $$\text{L1a.}\!$$ $$\downharpoonleft s \downharpoonright ~=~ p$$ $$\text{then}\!$$ $$\text{the following equations hold:}\!$$
 $$\text{L1b}_{00}.\!$$ $$\downharpoonleft \operatorname{false} \downharpoonright$$ $$=\!$$ $$(~)$$ $$=\!$$ $$\underline{0} ~:~ X \to \underline\mathbb{B}$$ $$\text{L1b}_{01}.\!$$ $$\downharpoonleft \operatorname{not}~ s \downharpoonright$$ $$=\!$$ $$(\downharpoonleft s \downharpoonright)$$ $$=\!$$ $$(p) ~:~ X \to \underline\mathbb{B}$$ $$\text{L1b}_{10}.\!$$ $$\downharpoonleft s \downharpoonright$$ $$=\!$$ $$\downharpoonleft s \downharpoonright$$ $$=\!$$ $$p ~:~ X \to \underline\mathbb{B}$$ $$\text{L1b}_{11}.\!$$ $$\downharpoonleft \operatorname{true} \downharpoonright$$ $$=\!$$ $$((~))$$ $$=\!$$ $$\underline{1} ~:~ X \to \underline\mathbb{B}$$

### Geometric Translation Rule 1

 $$\text{Geometric Translation Rule 1}\!$$
 $$\text{If}\!$$ $$Q \subseteq X$$ $$\text{and}\!$$ $$p ~:~ X \to \underline\mathbb{B}$$ $$\text{such that:}\!$$ $$\text{G1a.}\!$$ $$\upharpoonleft Q \upharpoonright ~=~ p$$ $$\text{then}\!$$ $$\text{the following equations hold:}\!$$
 $$\text{G1b}_{00}.\!$$ $$\upharpoonleft \varnothing \upharpoonright$$ $$=\!$$ $$(~)$$ $$=\!$$ $$\underline{0} ~:~ X \to \underline\mathbb{B}$$ $$\text{G1b}_{01}.\!$$ $$\upharpoonleft {}^{_\sim} Q \upharpoonright$$ $$=\!$$ $$(\upharpoonleft Q \upharpoonright)$$ $$=\!$$ $$(p) ~:~ X \to \underline\mathbb{B}$$ $$\text{G1b}_{10}.\!$$ $$\upharpoonleft Q \upharpoonright$$ $$=\!$$ $$\upharpoonleft Q \upharpoonright$$ $$=\!$$ $$p ~:~ X \to \underline\mathbb{B}$$ $$\text{G1b}_{11}.\!$$ $$\upharpoonleft X \upharpoonright$$ $$=\!$$ $$((~))$$ $$=\!$$ $$\underline{1} ~:~ X \to \underline\mathbb{B}$$

### Logical Translation Rule 2

 $$\text{Logical Translation Rule 2}\!$$
 $$\text{If}\!$$ $$s, t ~\text{are sentences about things in the universe}~ X$$ $$\text{and}\!$$ $$p, q ~\text{are propositions} ~:~ X \to \underline\mathbb{B}$$ $$\text{such that:}\!$$ $$\text{L2a.}\!$$ $$\downharpoonleft s \downharpoonright ~=~ p \quad \operatorname{and} \quad \downharpoonleft t \downharpoonright ~=~ q$$ $$\text{then}\!$$ $$\text{the following equations hold:}\!$$
 $$\text{L2b}_{0}.\!$$ $$\downharpoonleft \operatorname{false} \downharpoonright$$ $$=\!$$ $$(~)$$ $$=\!$$ $$(~)$$ $$\text{L2b}_{1}.\!$$ $$\downharpoonleft \operatorname{neither}~ s ~\operatorname{nor}~ t \downharpoonright$$ $$=\!$$ $$(\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright)$$ $$=\!$$ $$(p)(q)\!$$ $$\text{L2b}_{2}.\!$$ $$\downharpoonleft \operatorname{not}~ s ~\operatorname{but}~ t \downharpoonright$$ $$=\!$$ $$(\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright$$ $$=\!$$ $$(p) q\!$$ $$\text{L2b}_{3}.\!$$ $$\downharpoonleft \operatorname{not}~ s \downharpoonright$$ $$=\!$$ $$(\downharpoonleft s \downharpoonright)$$ $$=\!$$ $$(p)\!$$ $$\text{L2b}_{4}.\!$$ $$\downharpoonleft s ~\operatorname{and~not}~ t \downharpoonright$$ $$=\!$$ $$\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright)$$ $$=\!$$ $$p (q)\!$$ $$\text{L2b}_{5}.\!$$ $$\downharpoonleft \operatorname{not}~ t \downharpoonright$$ $$=\!$$ $$(\downharpoonleft t \downharpoonright)$$ $$=\!$$ $$(q)\!$$ $$\text{L2b}_{6}.\!$$ $$\downharpoonleft s ~\operatorname{or}~ t, ~\operatorname{not~both} \downharpoonright$$ $$=\!$$ $$(\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright)$$ $$=\!$$ $$(p, q)\!$$ $$\text{L2b}_{7}.\!$$ $$\downharpoonleft \operatorname{not~both}~ s ~\operatorname{and}~ t \downharpoonright$$ $$=\!$$ $$(\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright)$$ $$=\!$$ $$(p q)\!$$ $$\text{L2b}_{8}.\!$$ $$\downharpoonleft s ~\operatorname{and}~ t \downharpoonright$$ $$=\!$$ $$\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright$$ $$=\!$$ $$p q\!$$ $$\text{L2b}_{9}.\!$$ $$\downharpoonleft s ~\operatorname{is~equivalent~to}~ t \downharpoonright$$ $$=\!$$ $$((\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright))$$ $$=\!$$ $$((p, q))\!$$ $$\text{L2b}_{10}.\!$$ $$\downharpoonleft t \downharpoonright$$ $$=\!$$ $$\downharpoonleft t \downharpoonright$$ $$=\!$$ $$q\!$$ $$\text{L2b}_{11}.\!$$ $$\downharpoonleft s ~\operatorname{implies}~ t \downharpoonright$$ $$=\!$$ $$(\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright))$$ $$=\!$$ $$(p (q))\!$$ $$\text{L2b}_{12}.\!$$ $$\downharpoonleft s \downharpoonright$$ $$=\!$$ $$\downharpoonleft s \downharpoonright$$ $$=\!$$ $$p\!$$ $$\text{L2b}_{13}.\!$$ $$\downharpoonleft s ~\operatorname{is~implied~by}~ t \downharpoonright$$ $$=\!$$ $$((\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright)$$ $$=\!$$ $$((p) q)\!$$ $$\text{L2b}_{14}.\!$$ $$\downharpoonleft s ~\operatorname{or}~ t \downharpoonright$$ $$=\!$$ $$((\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright))$$ $$=\!$$ $$((p)(q))\!$$ $$\text{L2b}_{15}.\!$$ $$\downharpoonleft \operatorname{true} \downharpoonright$$ $$=\!$$ $$((~))$$ $$=\!$$ $$((~))$$

### Geometric Translation Rule 2

 $$\text{Geometric Translation Rule 2}\!$$
 $$\text{If}\!$$ $$P, Q \subseteq X$$ $$\text{and}\!$$ $$p, q ~:~ X \to \underline\mathbb{B}$$ $$\text{such that:}\!$$ $$\text{G2a.}\!$$ $$\upharpoonleft P \upharpoonright ~=~ p \quad \operatorname{and} \quad \upharpoonleft Q \upharpoonright ~=~ q$$ $$\text{then}\!$$ $$\text{the following equations hold:}\!$$
 $$\text{G2b}_{0}.\!$$ $$\upharpoonleft \varnothing \upharpoonright$$ $$=\!$$ $$(~)$$ $$=\!$$ $$(~)$$ $$\text{G2b}_{1}.\!$$ $$\upharpoonleft \overline{P} ~\cap~ \overline{Q} \upharpoonright$$ $$=\!$$ $$(\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright)$$ $$=\!$$ $$(p)(q)\!$$ $$\text{G2b}_{2}.\!$$ $$\upharpoonleft \overline{P} ~\cap~ Q \upharpoonright$$ $$=\!$$ $$(\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright$$ $$=\!$$ $$(p) q\!$$ $$\text{G2b}_{3}.\!$$ $$\upharpoonleft \overline{P} \upharpoonright$$ $$=\!$$ $$(\upharpoonleft P \upharpoonright)$$ $$=\!$$ $$(p)\!$$ $$\text{G2b}_{4}.\!$$ $$\upharpoonleft P ~\cap~ \overline{Q} \upharpoonright$$ $$=\!$$ $$\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright)$$ $$=\!$$ $$p (q)\!$$ $$\text{G2b}_{5}.\!$$ $$\upharpoonleft \overline{Q} \upharpoonright$$ $$=\!$$ $$(\upharpoonleft Q \upharpoonright)$$ $$=\!$$ $$(q)\!$$ $$\text{G2b}_{6}.\!$$ $$\upharpoonleft P ~+~ Q \upharpoonright$$ $$=\!$$ $$(\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright)$$ $$=\!$$ $$(p, q)\!$$ $$\text{G2b}_{7}.\!$$ $$\upharpoonleft \overline{P ~\cap~ Q} \upharpoonright$$ $$=\!$$ $$(\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright)$$ $$=\!$$ $$(p q)\!$$ $$\text{G2b}_{8}.\!$$ $$\upharpoonleft P ~\cap~ Q \upharpoonright$$ $$=\!$$ $$\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright$$ $$=\!$$ $$p q\!$$ $$\text{G2b}_{9}.\!$$ $$\upharpoonleft \overline{P ~+~ Q} \upharpoonright$$ $$=\!$$ $$((\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright))$$ $$=\!$$ $$((p, q))\!$$ $$\text{G2b}_{10}.\!$$ $$\upharpoonleft Q \upharpoonright$$ $$=\!$$ $$\upharpoonleft Q \upharpoonright$$ $$=\!$$ $$q\!$$ $$\text{G2b}_{11}.\!$$ $$\upharpoonleft \overline{P ~\cap~ \overline{Q}} \upharpoonright$$ $$=\!$$ $$(\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright))$$ $$=\!$$ $$(p (q))\!$$ $$\text{G2b}_{12}.\!$$ $$\upharpoonleft P \upharpoonright$$ $$=\!$$ $$\upharpoonleft P \upharpoonright$$ $$=\!$$ $$p\!$$ $$\text{G2b}_{13}.\!$$ $$\upharpoonleft \overline{\overline{P} ~\cap~ Q} \upharpoonright$$ $$=\!$$ $$((\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright)$$ $$=\!$$ $$((p) q)\!$$ $$\text{G2b}_{14}.\!$$ $$\upharpoonleft P ~\cup~ Q \upharpoonright$$ $$=\!$$ $$((\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright))$$ $$=\!$$ $$((p)(q))\!$$ $$\text{G2b}_{15}.\!$$ $$\upharpoonleft X \upharpoonright$$ $$=\!$$ $$((~))$$ $$=\!$$ $$((~))$$

### 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

 $$\text{Value Rule 1}\!$$
 $$\text{If}\!$$ $$v, w ~\in~ \underline\mathbb{B}$$ $$\text{then}\!$$ $$^{\backprime\backprime} v = w \, ^{\prime\prime} ~\text{is a sentence about pairs of values}~ (v, w) \in \underline\mathbb{B}^2,$$ $$\downharpoonleft v = w \downharpoonright ~\text{is a proposition} ~:~ \underline\mathbb{B}^2 \to \underline\mathbb{B},$$ $$\text{and}\!$$ $$\text{the following are identical values in}~ \underline\mathbb{B}:$$
 $$\text{V1a.}\!$$ $$\downharpoonleft v = w \downharpoonright (v, w)$$ $$\text{V1b.}\!$$ $$\downharpoonleft v \Leftrightarrow w \downharpoonright (v, w)$$ $$\text{V1c.}\!$$ $$\underline{((}~ v ~,~ w ~\underline{))}$$

#### Variant 2

 $$\text{Value Rule 1}\!$$
 $$\text{If}\!$$ $$v, w ~\in~ \underline\mathbb{B}$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\text{V1a.}\!$$ $$v = w\!$$ $$\text{V1b.}\!$$ $$v \Leftrightarrow w$$ $$\text{V1c.}\!$$ $$\underline{((}~ v ~,~ w ~\underline{))}$$

#### Variant 3

A rule that allows one to turn equivalent sentences into identical propositions:

 $$(s ~\Leftrightarrow~ t) \quad \Leftrightarrow \quad (\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright)$$

Consider the following pair of expressions:

 $$\downharpoonleft v ~=~ w \downharpoonright (v, w)$$ $$\downharpoonleft v(x) ~=~ w(x) \downharpoonright (x)$$

 $$\text{Value Rule 1}\!$$
 $$\text{If}\!$$ $$v, w ~\in~ \underline\mathbb{B}$$ $$\text{then}\!$$ $$\text{the following are identical values in}~ \underline\mathbb{B}:$$
 $$\text{V1a.}\!$$ $$\downharpoonleft v = w \downharpoonright$$ $$\text{V1b.}\!$$ $$\downharpoonleft v \Leftrightarrow w \downharpoonright$$ $$\text{V1c.}\!$$ $$\underline{((}~ v ~,~ w ~\underline{))}$$

#### Variant 4

 $$\text{Value Rule 1}\!$$
 $$\text{If}\!$$ $$f, g ~:~ X \to \underline\mathbb{B}$$ $$\text{and}\!$$ $$x ~\in~ X$$ $$\text{then}\!$$ $$\text{the following are identical values in}~ \underline\mathbb{B}:$$
 $$\text{V1a.}\!$$ $$\downharpoonleft f(x) ~=~ g(x) \downharpoonright$$ $$\text{V1b.}\!$$ $$\downharpoonleft f(x) ~\Leftrightarrow~ g(x) \downharpoonright$$ $$\text{V1c.}\!$$ $$\underline{((}~ f(x) ~,~ g(x) ~\underline{))}$$

#### Variant 5

 $$\text{Value Rule 1}\!$$
 $$\text{If}\!$$ $$f, g ~:~ X \to \underline\mathbb{B}$$ $$\text{then}\!$$ $$\text{the following are identical propositions on}~ X:$$
 $$\text{V1a.}\!$$ $$\downharpoonleft f ~=~ g \downharpoonright$$ $$\text{V1b.}\!$$ $$\downharpoonleft f ~\Leftrightarrow~ g \downharpoonright$$ $$\text{V1c.}\!$$ $$\underline{((}~ f ~,~ g ~\underline{))}^\$$

### Evaluation Rule 1

 $$\operatorname{Evaluation~Rule~1}$$
 $$\text{If}\!$$ $$f, g ~:~ X \to \underline\mathbb{B}$$ $$\text{and}\!$$ $$x ~\in~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{E1a.}$$ $$f(x) ~=~ g(x)$$ $$\operatorname{E1a~:~V1a}$$ $$::\!$$ $$\operatorname{E1b.}$$ $$f(x) ~\Leftrightarrow~ g(x)$$ $$\operatorname{E1b~:~V1b}$$ $$::\!$$ $$\operatorname{E1c.}$$ $$\underline{((}~ f(x) ~,~ g(x) ~\underline{))}$$ $$\operatorname{E1c~:~V1c}$$ $$\operatorname{E1c~:~1a}$$ $$::\!$$ $$\operatorname{E1d.}$$ $$\underline{((}~ f ~,~ g ~\underline{))}^\ (x)$$ $$\operatorname{E1d~:~1b}$$

### Definition 2

#### Variant 1

 $$\operatorname{Definition~2}$$
 $$\text{If}\!$$ $$P, Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{D2a.}$$ $$P ~=~ Q$$ $$\operatorname{D2b.}$$ $$x \in P ~\Leftrightarrow~ x \in Q$$ $$\forall x \in X$$

#### Variant 2

 $$\operatorname{Definition~2}$$
 $$\text{If}\!$$ $$P, Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{D2a.}$$ $$P ~=~ Q$$ $$\operatorname{D2b.}$$ $$\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)$$

### Definition 3

#### Variant 1

 $$\operatorname{Definition~3}$$
 $$\text{If}\!$$ $$f, g ~:~ X \to Y$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{D3a.}$$ $$f ~=~ g$$ $$\operatorname{D3b.}$$ $$f(x) ~=~ g(x)$$ $$\forall x \in X$$

#### Variant 2

 $$\operatorname{Definition~3}$$
 $$\text{If}\!$$ $$f, g ~:~ X \to Y$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{D3a.}$$ $$f ~=~ g$$ $$\operatorname{D3b.}$$ $$\overset{X}{\underset{x}{\forall}}~ (f(x) ~=~ g(x))$$

#### Variant 3

 $$\operatorname{Definition~3}$$
 $$\text{If}\!$$ $$f, g ~:~ X \to Y$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{D3a.}$$ $$f ~=~ g$$ $$\operatorname{D3b.}$$ $$\prod_x^X~ (f(x) ~=~ g(x))$$

### Definition 4

 $$\operatorname{Definition~4}$$
 $$\text{If}\!$$ $$Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are identical subsets of}~ X \times \underline\mathbb{B}:$$
 $$\operatorname{D4a.}$$ $$\upharpoonleft Q \upharpoonright$$ $$\operatorname{D4b.}$$ $$\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in Q \downharpoonright$$

### Definition 5

#### Variant 1

 $$\operatorname{Definition~5}$$
 $$\text{If}\!$$ $$Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are identical propositions:}\!$$
 $$\operatorname{D5a.}$$ $$\upharpoonleft Q \upharpoonright$$ $$\operatorname{D5b.}$$ $$\begin{array}{lcl} f & : & X \to \underline\mathbb{B} \\ f(x) & = & \downharpoonleft x \in Q \downharpoonright \quad (\forall x \in X) \end{array}$$

#### Variant 2

 $$\operatorname{Definition~5}$$
 $$\text{If}\!$$ $$Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are identical propositions:}\!$$
 $$\operatorname{D5a.}$$ $$\upharpoonleft Q \upharpoonright$$ $$\operatorname{D5b.}$$ $$\begin{array}{ccccl} f & : & X & \to & \underline\mathbb{B} \\ f & : & x & \mapsto & \downharpoonleft x \in Q \downharpoonright \end{array}$$

#### Variant 3

 $$\operatorname{Definition~5}$$
 $$\text{If}\!$$ $$Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are identical propositions} ~:~ X \to \underline\mathbb{B}$$
 $$\operatorname{D5a.}$$ $$\upharpoonleft Q \upharpoonright$$ $$\operatorname{D5b.}$$ $$\downharpoonleft x \in Q \downharpoonright$$

### Definition 6

 $$\operatorname{Definition~6}$$
 $$\text{If}\!$$ $$\text{each string}~ s_j, ~\text{as}~ j ~\text{ranges over the set}~ J,$$ $$\text{is a sentence about things in the universe}~ X~$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{D6a.}$$ $$\overset{J}{\underset{j}{\forall}}~ s_j$$ $$\operatorname{D6b.}$$ $$\operatorname{Conj}_j^J s_j$$

### Definition 7

 $$\operatorname{Definition~7}$$
 $$\text{If}\!$$ $$s, t ~\text{are sentences about things in the universe}~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{D7a.}$$ $$s ~\Leftrightarrow~ t$$ $$\operatorname{D7b.}$$ $$\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright$$

### Rule 5

 $$\operatorname{Rule~5}$$
 $$\text{If}\!$$ $$P, Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{R5a.}$$ $$P ~=~ Q$$ $$\operatorname{R5a~:~D2a}$$ $$::\!$$ $$\operatorname{R5b.}$$ $$\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)$$ $$\operatorname{R5b~:~D2b}$$ $$\operatorname{R5b~:~D7a}$$ $$::\!$$ $$\operatorname{R5c.}$$ $$\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright)$$ $$\operatorname{R5c~:~D7b}$$ $$\operatorname{R5c~:~\_\_?\_\_}$$ $$::\!$$ $$\operatorname{R5d.}$$ $$\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}$$ $$\operatorname{R5d~:~\_\_?\_\_}$$ $$\operatorname{R5d~:~D5b}$$ $$::\!$$ $$\operatorname{R5e.}$$ $$\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright$$ $$\operatorname{R5e~:~D5a}$$

### Rule 6

 $$\operatorname{Rule~6}$$
 $$\text{If}\!$$ $$f, g ~:~ X \to Y$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{R6a.}$$ $$f ~=~ g$$ $$\operatorname{R6a~:~D3a}$$ $$::\!$$ $$\operatorname{R6b.}$$ $$\overset{X}{\underset{x}{\forall}}~ (f(x) ~=~ g(x))$$ $$\operatorname{R6b~:~D3b}$$ $$\operatorname{R6b~:~D6a}$$ $$::\!$$ $$\operatorname{R6c.}$$ $$\operatorname{Conj_x^X}~ (f(x) ~=~ g(x))$$ $$\operatorname{R6c~:~D6b}$$

### Rule 7

 $$\operatorname{Rule~7}$$
 $$\text{If}\!$$ $$p, q ~:~ X \to \underline\mathbb{B}$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{R7a.}$$ $$p ~=~ q$$ $$\operatorname{R7a~:~R6a}$$ $$::\!$$ $$\operatorname{R7b.}$$ $$\overset{X}{\underset{x}{\forall}}~ (p(x) ~=~ q(x))$$ $$\operatorname{R7b~:~R6b}$$ $$::\!$$ $$\operatorname{R7c.}$$ $$\operatorname{Conj_x^X}~ (p(x) ~=~ q(x))$$ $$\operatorname{R7c~:~R6c}$$ $$\operatorname{R7c~:~P1a}$$ $$::\!$$ $$\operatorname{R7d.}$$ $$\operatorname{Conj_x^X}~ (p(x) ~\Leftrightarrow~ q(x))$$ $$\operatorname{R7d~:~P1b}$$ $$::\!$$ $$\operatorname{R7e.}$$ $$\operatorname{Conj_x^X}~ \underline{((}~ p(x) ~,~ q(x) ~\underline{))}$$ $$\operatorname{R7e~:~P1c}$$ $$\operatorname{R7e~:~1a}$$ $$::\!$$ $$\operatorname{R7f.}$$ $$\operatorname{Conj_x^X}~ \underline{((}~ p ~,~ q ~\underline{))}^\ (x)$$ $$\operatorname{R7f~:~1b}$$

### Rule 8

 $$\operatorname{Rule~8}$$
 $$\text{If}\!$$ $$s, t ~\text{are sentences about things in}~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{R8a.}$$ $$s ~\Leftrightarrow~ t$$ $$\operatorname{R8a~:~D7a}$$ $$::\!$$ $$\operatorname{R8b.}$$ $$\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright$$ $$\operatorname{R8b~:~D7b}$$ $$\operatorname{R8b~:~R7a}$$ $$::\!$$ $$\operatorname{R8c.}$$ $$\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))$$ $$\operatorname{R8c~:~R7b}$$ $$::\!$$ $$\operatorname{R8d.}$$ $$\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))$$ $$\operatorname{R8d~:~R7c}$$ $$::\!$$ $$\operatorname{R8e.}$$ $$\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft t \downharpoonright (x))$$ $$\operatorname{R8e~:~R7d}$$ $$::\!$$ $$\operatorname{R8f.}$$ $$\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright (x) ~,~ \downharpoonleft t \downharpoonright (x) ~\underline{))}$$ $$\operatorname{R8f~:~R7e}$$ $$::\!$$ $$\operatorname{R8g.}$$ $$\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright ~\underline{))}^\ (x)$$ $$\operatorname{R8g~:~R7f}$$

### Rule 9

 $$\operatorname{Rule~9}$$
 $$\text{If}\!$$ $$P, Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{R9a.}$$ $$P ~=~ Q$$ $$\operatorname{R9a~:~R5a}$$ $$::\!$$ $$\operatorname{R9b.}$$ $$\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright$$ $$\operatorname{R9b~:~R5e}$$ $$\operatorname{R9b~:~R7a}$$ $$::\!$$ $$\operatorname{R9c.}$$ $$\overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))$$ $$\operatorname{R9c~:~R7b}$$ $$::\!$$ $$\operatorname{R9d.}$$ $$\operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))$$ $$\operatorname{R9d~:~R7c}$$ $$::\!$$ $$\operatorname{R9e.}$$ $$\operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x))$$ $$\operatorname{R9e~:~R7d}$$ $$::\!$$ $$\operatorname{R9f.}$$ $$\operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}$$ $$\operatorname{R9f~:~R7e}$$ $$::\!$$ $$\operatorname{R9g.}$$ $$\operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\ (x)$$ $$\operatorname{R9g~:~R7f}$$

### Rule 10

 $$\operatorname{Rule~10}$$
 $$\text{If}\!$$ $$P, Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{R10a.}$$ $$P ~=~ Q$$ $$\operatorname{R10a~:~D2a}$$ $$::\!$$ $$\operatorname{R10b.}$$ $$\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)$$ $$\operatorname{R10b~:~D2b}$$ $$\operatorname{R10b~:~R8a}$$ $$::\!$$ $$\operatorname{R10c.}$$ $$\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright$$ $$\operatorname{R10c~:~R8b}$$ $$::\!$$ $$\operatorname{R10d.}$$ $$\overset{X}{\underset{x}{\forall}}~ \downharpoonleft x \in P \downharpoonright (x) ~=~ \downharpoonleft x \in Q \downharpoonright (x)$$ $$\operatorname{R10d~:~R8c}$$ $$::\!$$ $$\operatorname{R10e.}$$ $$\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~=~ \downharpoonleft x \in Q \downharpoonright (x))$$ $$\operatorname{R10e~:~R8d}$$ $$::\!$$ $$\operatorname{R10f.}$$ $$\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft x \in Q \downharpoonright (x))$$ $$\operatorname{R10f~:~R8e}$$ $$::\!$$ $$\operatorname{R10g.}$$ $$\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft x \in P \downharpoonright (x) ~,~ \downharpoonleft x \in Q \downharpoonright (x) ~\underline{))}$$ $$\operatorname{R10g~:~R8f}$$ $$::\!$$ $$\operatorname{R10h.}$$ $$\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft x \in P \downharpoonright ~,~ \downharpoonleft x \in Q \downharpoonright ~\underline{))}^\ (x)$$ $$\operatorname{R10h~:~R8g}$$

### Rule 11

 $$\operatorname{Rule~11}$$
 $$\text{If}\!$$ $$Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{R11a.}$$ $$Q ~=~ \{ x \in X ~:~ s \}$$ $$\operatorname{R11a~:~R5a}$$ $$::\!$$ $$\operatorname{R11b.}$$ $$\upharpoonleft Q \upharpoonright ~=~ \upharpoonleft \{ x \in X ~:~ s \} \upharpoonright$$ $$\operatorname{R11b~:~R5e}$$ $$::\!$$ $$\operatorname{R11c.}$$ $$\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}$$ $$\operatorname{R11c~:~\_\_?\_\_}$$ $$\operatorname{R11c~:~\_\_?\_\_}$$ $$::\!$$ $$\operatorname{R11d.}$$ $$\begin{array}{ccccl} \upharpoonleft Q \upharpoonright & : & X & \to & \underline\mathbb{B} \\ \upharpoonleft Q \upharpoonright & : & x & \mapsto & \downharpoonleft s \downharpoonright (x) \end{array}$$ $$\operatorname{R11d~:~\_\_?\_\_}$$ $$\operatorname{R11d~:~\_\_?\_\_}$$ $$::\!$$ $$\operatorname{R11e.}$$ $$\overset{X}{\underset{x}{\forall}}~ \upharpoonleft Q \upharpoonright (x) ~=~ \downharpoonleft s \downharpoonright (x)$$ $$\operatorname{R11e~:~\_\_?\_\_}$$ $$\operatorname{R11e~:~\_\_?\_\_}$$ $$::\!$$ $$\operatorname{R11f.}$$ $$\upharpoonleft Q \upharpoonright ~=~ \downharpoonleft s \downharpoonright$$ $$\operatorname{R11f~:~\_\_?\_\_}$$

### Fact 1

#### Variant 1

 $$\operatorname{Fact~1}$$
 $$\text{If}\!$$ $$P, Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{F1a.}$$ $$s \quad \Leftrightarrow \quad (P ~=~ Q)$$ $$\operatorname{F1a~:~R9a}$$ $$::\!$$ $$\operatorname{F1b.}$$ $$s \quad \Leftrightarrow \quad (\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright)$$ $$\operatorname{F1b~:~R9b}$$ $$::\!$$ $$\operatorname{F1c.}$$ $$s \quad \Leftrightarrow \quad \overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))$$ $$\operatorname{F1c~:~R9c}$$ $$::\!$$ $$\operatorname{F1d.}$$ $$s \quad \Leftrightarrow \quad \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))$$ $$\operatorname{F1d~:~R9d}$$ $$\operatorname{F1d~:~R8a}$$ $$::\!$$ $$\operatorname{F1e.}$$ $$\downharpoonleft s \downharpoonright \quad = \quad \downharpoonleft \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright$$ $$\operatorname{F1e~:~R8b}$$ $$\operatorname{F1e~:~\_\_?\_\_}$$ $$::\!$$ $$\operatorname{F1f.}$$ $$\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \downharpoonleft (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright$$ $$\operatorname{F1f~:~\_\_?\_\_}$$ $$\operatorname{F1f~:~\_\_?\_\_}$$ $$::\!$$ $$\operatorname{F1g.}$$ $$\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}$$ $$\operatorname{F1g~:~\_\_?\_\_}$$ $$\operatorname{F1g~:~\_\_?\_\_}$$ $$::\!$$ $$\operatorname{F1h.}$$ $$\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\ (x)$$ $$\operatorname{F1h~:~~\_\_?\_\_}$$

#### Variant 2

 $$\operatorname{Fact~1}$$
 $$\text{If}\!$$ $$P, Q ~\subseteq~ X$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{F1a.}$$ $$s \quad \Leftrightarrow \quad (P ~=~ Q)$$ $$\operatorname{F1a~:~R9a}$$ $$::\!$$ $$\operatorname{F1b.}$$ $$s \quad \Leftrightarrow \quad (\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright)$$ $$\operatorname{F1b~:~R9b}$$ $$::\!$$ $$\operatorname{F1c.}$$ $$s \quad \Leftrightarrow \quad \overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))$$ $$\operatorname{F1c~:~R9c}$$ $$::\!$$ $$\operatorname{F1d.}$$ $$s \quad \Leftrightarrow \quad \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))$$ $$\operatorname{F1d~:~R9d}$$ $$\operatorname{F1d~:~R8a}$$ $$::\!$$ $$\operatorname{F1e.}$$ $$\downharpoonleft s \downharpoonright \quad = \quad \downharpoonleft \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright$$ $$\operatorname{F1e~:~R8b}$$ $$\operatorname{F1e~:~\_\_?\_\_}$$ $$::\!$$ $$\operatorname{F1f.}$$ $$\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \downharpoonleft (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright$$ $$\operatorname{F1f~:~\_\_?\_\_}$$ $$\operatorname{F1f~:~\_\_?\_\_}$$ $$::\!$$ $$\operatorname{F1g.}$$ $$\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}$$ $$\operatorname{F1g~:~\_\_?\_\_}$$ $$\operatorname{F1g~:~\_\_?\_\_}$$ $$::\!$$ $$\operatorname{F1h.}$$ $$\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\ (x)$$ $$\operatorname{F1h~:~~\_\_?\_\_}$$

### Definition 8

 $$\operatorname{Definition~8}$$
 $$\text{If}\!$$ $$L ~\subseteq~ O \times S \times I$$ $$\text{then}\!$$ $$\text{the following are identical subsets of}~ S \times I \, :$$
 $$\operatorname{D8a.}$$ $$L_{SI}\!$$ $$\operatorname{D8b.}$$ $$\operatorname{Con}^L$$ $$\operatorname{D8c.}$$ $$\operatorname{Con}(L)$$ $$\operatorname{D8d.}$$ $$\operatorname{proj}_{SI}(L)$$ $$\operatorname{D8e.}$$ $$\{ (s, i) \in S \times I ~:~ (o, s, i) \in L ~\operatorname{for~some}~ o \in O \}$$

### Definition 9

 $$\operatorname{Definition~9}$$
 $$\text{If}\!$$ $$L ~\subseteq~ O \times S \times I$$ $$\text{then}\!$$ $$\text{the following are identical subsets of}~ I \times S \, :$$
 $$\operatorname{D9a.}$$ $$L_{IS}\!$$ $$\operatorname{D9b.}$$ $$\overset{\smile}{L_{SI}}$$ $$\operatorname{D9c.}$$ $$\overset{\smile}{\operatorname{Con}^L}$$ $$\operatorname{D9d.}$$ $$\overset{\smile}{\operatorname{Con}(L)}$$ $$\operatorname{D9e.}$$ $$\operatorname{proj}_{IS}(L)$$ $$\operatorname{D9f.}$$ $$\operatorname{Conv}(\operatorname{Con}(L))$$ $$\operatorname{D9g.}$$ $$\{ (i, s) \in I \times S ~:~ (o, s, i) \in L ~\operatorname{for~some}~ o \in O \}$$

### Definition 10

 $$\operatorname{Definition~10}$$
 $$\text{If}\!$$ $$L ~\subseteq~ O \times S \times I$$ $$\text{then}\!$$ $$\text{the following are identical subsets of}~ O \times S \, :$$
 $$\operatorname{D10a.}$$ $$L_{OS}\!$$ $$\operatorname{D10b.}$$ $$\operatorname{Den}^L$$ $$\operatorname{D10c.}$$ $$\operatorname{Den}(L)$$ $$\operatorname{D10d.}$$ $$\operatorname{proj}_{OS}(L)$$ $$\operatorname{D10e.}$$ $$\{ (o, s) \in O \times S ~:~ (o, s, i) \in L ~\operatorname{for~some}~ i \in I \}$$

### Definition 11

 $$\operatorname{Definition~11}$$
 $$\text{If}\!$$ $$L ~\subseteq~ O \times S \times I$$ $$\text{then}\!$$ $$\text{the following are identical subsets of}~ S \times O \, :$$
 $$\operatorname{D11a.}$$ $$L_{SO}\!$$ $$\operatorname{D11b.}$$ $$\overset{\smile}{L_{OS}}$$ $$\operatorname{D11c.}$$ $$\overset{\smile}{\operatorname{Den}^L}$$ $$\operatorname{D11d.}$$ $$\overset{\smile}{\operatorname{Den}(L)}$$ $$\operatorname{D11e.}$$ $$\operatorname{proj}_{SO}(L)$$ $$\operatorname{D11f.}$$ $$\operatorname{Conv}(\operatorname{Den}(L))$$ $$\operatorname{D11g.}$$ $$\{ (s, o) \in S \times O ~:~ (o, s, i) \in L ~\operatorname{for~some}~ i \in I \}$$

### Definition 12

 $$\operatorname{Definition~12}$$
 $$\text{If}\!$$ $$L ~\subseteq~ O \times S \times I$$ $$\text{and}\!$$ $$x ~\in~ S$$ $$\text{then}\!$$ $$\text{the following are identical subsets of}~ O \, :$$
 $$\operatorname{D12a.}$$ $$L_{OS} \cdot x$$ $$\operatorname{D12b.}$$ $$\operatorname{Den}^L \cdot x$$ $$\operatorname{D12c.}$$ $$\operatorname{Den}^L |_x$$ $$\operatorname{D12d.}$$ $$\operatorname{Den}^L (-, x)$$ $$\operatorname{D12e.}$$ $$\operatorname{Den}(L, x)$$ $$\operatorname{D12f.}$$ $$\operatorname{Den}(L) \cdot x$$ $$\operatorname{D12g.}$$ $$\{ o \in O ~:~ (o, x) \in \operatorname{Den}(L) \}$$ $$\operatorname{D12h.}$$ $$\{ o \in O ~:~ (o, x, i) \in L ~\operatorname{for~some}~ i \in I \}$$

### Definition 13

 $$\operatorname{Definition~13}$$
 $$\text{If}\!$$ $$L ~\subseteq~ O \times S \times I$$ $$\text{then}\!$$ $$\text{the following are identical subsets of}~ S \times I \, :$$
 $$\operatorname{D13a.}$$ $$\operatorname{Der}^L$$ $$\operatorname{D13b.}$$ $$\operatorname{Der}(L)$$ $$\operatorname{D13c.}$$ $$\{ (x, y) \in S \times I ~:~ \operatorname{Den}^L|_x = \operatorname{Den}^L|_y \}$$ $$\operatorname{D13d.}$$ $$\{ (x, y) \in S \times I ~:~ \operatorname{Den}(L, x) = \operatorname{Den}(L, y) \}$$

### Fact 2.1

 $$\operatorname{Fact~2.1}$$
 $$\text{If}\!$$ $$L ~\subseteq~ O \times S \times I$$ $$\text{then}\!$$ $$\text{the following are identical subsets of}~ S \times I :$$
 $$\operatorname{F2.1a.}$$ $$\operatorname{Der}^L$$ $$\operatorname{F2.1a~:~D13a}$$ $$::\!$$ $$\operatorname{F2.1b.}$$ $$\operatorname{Der}(L)$$ $$\operatorname{F2.1b~:~D13b}$$ $$::\!$$ $$\operatorname{F2.1c.}$$ $$\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \operatorname{Den}(L, x) ~=~ \operatorname{Den}(L, y) \\ \} & \\ \end{array}$$ $$\operatorname{F2.1c~:~D13c}$$ $$\operatorname{F2.1c~:~R9a}$$ $$::\!$$ $$\operatorname{F2.1d.}$$ $$\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \upharpoonleft \operatorname{Den}(L, x) \upharpoonright ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright \\ \} & \\ \end{array}$$ $$\operatorname{F2.1d~:~R9b}$$ $$::\!$$ $$\operatorname{F2.1e.}$$ $$\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}$$ $$\operatorname{F2.1e~:~R9c}$$ $$::\!$$ $$\operatorname{F2.1f.}$$ $$\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}$$ $$\operatorname{F2.1f~:~R9d}$$ $$::\!$$ $$\operatorname{F2.1g.}$$ $$\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}$$ $$\operatorname{F2.1g~:~R9e}$$ $$::\!$$ $$\operatorname{F2.1h.}$$ $$\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}$$ $$\operatorname{F2.1h~:~R9f}$$ $$\operatorname{F2.1h~:~D12e}$$ $$::\!$$ $$\operatorname{F2.1i.}$$ $$\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}$$ $$\operatorname{F2.1i~:~D12a}$$

### Fact 2.2

#### Variant 1

 $$\operatorname{Fact~2.2}$$
 $$\text{If}\!$$ $$L ~\subseteq~ O \times S \times I$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{F2.2a.}$$ $$\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}$$ $$\operatorname{F2.2a~:~R11a}$$ $$::\!$$ $$\operatorname{F2.2b.}$$ $$\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}$$ $$\operatorname{F2.2b~:~R11b}$$ $$::\!$$ $$\operatorname{F2.2c.}$$ $$\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}$$ $$\operatorname{F2.2c~:~R11c}$$ $$::\!$$ $$\operatorname{F2.2d.}$$ $$\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}$$ $$\operatorname{F2.2d~:~Log}$$ $$::\!$$ $$\operatorname{F2.2e.}$$ $$\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}$$ $$\operatorname{F2.2e~:~Log}$$ $$::\!$$ $$\operatorname{F2.2f.}$$ $$\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}$$ $$\operatorname{F2.2f~:~~}$$

#### Variant 2

 $$\operatorname{Fact~2.2}$$
 $$\text{If}\!$$ $$L ~\subseteq~ O \times S \times I$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 \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} $$\operatorname{F2.2a~:~R11a}$$ $$::\!$$ $$\operatorname{F2.2b.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright$$ $$\operatorname{F2.2b~:~R11b}$$ $$::\!$$ $$\operatorname{F2.2c.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright$$ $$\operatorname{F2.2c~:~R11c}$$ $$::\!$$ $$\operatorname{F2.2d.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright$$ $$\operatorname{F2.2d~:~Log}$$ $$::\!$$ $$\operatorname{F2.2e.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright$$ $$\operatorname{F2.2e~:~Log}$$ $$::\!$$ $$\operatorname{F2.2f.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright$$ $$\operatorname{F2.2f~:~~}$$

### Fact 2.3

 $$\operatorname{Fact~2.3}$$
 $$\text{If}\!$$ $$L ~\subseteq~ O \times S \times I$$ $$\text{then}\!$$ $$\text{the following are equivalent:}\!$$
 $$\operatorname{F2.3a.}$$ $$\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}$$ $$\operatorname{F2.3a~:~R11a}$$ $$::\!$$ $$\operatorname{F2.3b.}$$ $$\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}$$ $$\operatorname{F2.3b~:~R11d}$$ $$::\!$$ $$\operatorname{F2.3c.}$$ $$\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}$$ $$\operatorname{F2.3c~:~Log}$$ $$::\!$$ $$\operatorname{F2.3d.}$$ $$\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}$$ $$\operatorname{F2.3d~:~Def}$$ $$::\!$$ $$\operatorname{F2.3e.}$$ $$\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}$$ $$\operatorname{F2.3e~:~Log}$$ $$\operatorname{F2.3e~:~D10b}$$ $$::\!$$ $$\operatorname{F2.3f.}$$ $$\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}$$ $$\operatorname{F2.3f~:~D10a}$$