User:Jon Awbrey/BOX

Blank Form


   
       
       
       
       
   
       
   
       
   
       
   
       
   
       


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}\)