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}\)
|
|
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
Variant 1
\(\text{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}\)
|
|
Variant 2
\(\text{Evaluation Rule 1}\!\)
|
|
|
|
\(\text{If}\!\)
|
\(s, t ~\text{are sentences about things in the universe}~ X\)
|
|
|
\(f, g ~\text{are propositions} ~:~ 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
|
\(\text{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\)
|
|
Definition 3
Definition 3
If f, g : U -> V,
then the following are equivalent:
D3a. f = g.
D3b. f(u) = g(u), for all u C U.
Definition 4
Definition 4
If X c U,
then the following are identical subsets of UxB:
D4a. {X}
D4b. {<u, v> C UxB : v = [u C X]}
Definition 5
Definition 5
If X c U,
then the following are identical propositions:
D5a. {X}.
D5b. f : U -> B
: f(u) = [u C X], for all u C U.
Definition 6
Definition 6
If Sj is a sentence
about things in the universe U,
for all j C J,
then the following are equivalent:
D6a. Sj, for all j C J.
D6b. For all j C J, Sj.
D6c. Conj(j C J) Sj.
D6d. ConjJ,j Sj.
D6e. ConjJj Sj.
Definition 7
Definition 7
If S, T are sentences
about things in the universe U,
then the following are equivalent:
D7a. S <=> T.
D7b. [S] = [T].
Rule 5
Rule 5
If X, Y c U,
then the following are equivalent:
R5a. X = Y. :D2a
::
R5b. u C X <=> u C Y, for all u C U. :D2b
:D7a
::
R5c. [u C X] = [u C Y], for all u C U. :D7b
:???
::
R5d. {<u, v> C UxB : v = [u C X]}
=
{<u, v> C UxB : v = [u C Y]}. :???
:D5b
::
R5e. {X} = {Y}. :D5a
Rule 6
Rule 6
If f, g : U -> V,
then the following are equivalent:
R6a. f = g. :D3a
::
R6b. f(u) = g(u), for all u C U. :D3b
:D6a
::
R6c. ConjUu (f(u) = g(u)). :D6e
Rule 7
Rule 7
If P, Q : U -> B,
then the following are equivalent:
R7a. P = Q. :R6a
::
R7b. P(u) = Q(u), for all u C U. :R6b
::
R7c. ConjUu (P(u) = Q(u)). :R6c
:P1a
::
R7d. ConjUu (P(u) <=> Q(u)). :P1b
::
R7e. ConjUu (( P(u) , Q(u) )). :P1c
:$1a
::
R7f. ConjUu (( P , Q ))$(u). :$1b
Rule 8
Rule 8
If S, T are sentences
about things in the universe U,
then the following are equivalent:
R8a. S <=> T. :D7a
::
R8b. [S] = [T]. :D7b
:R7a
::
R8c. [S](u) = [T](u), for all u C U. :R7b
::
R8d. ConjUu ( [S](u) = [T](u) ). :R7c
::
R8e. ConjUu ( [S](u) <=> [T](u) ). :R7d
::
R8f. ConjUu (( [S](u) , [T](u) )). :R7e
::
R8g. ConjUu (( [S] , [T] ))$(u). :R7f
Rule 9
Rule 9
If X, Y c U,
then the following are equivalent:
R9a. X = Y. :R5a
::
R9b. {X} = {Y}. :R5e
:R7a
::
R9c. {X}(u) = {Y}(u), for all u C U. :R7b
::
R9d. ConjUu ( {X}(u) = {Y}(u) ). :R7c
::
R9e. ConjUu ( {X}(u) <=> {Y}(u) ). :R7d
::
R9f. ConjUu (( {X}(u) , {Y}(u) )). :R7e
::
R9g. ConjUu (( {X} , {Y} ))$(u). :R7f
Rule 10
Rule 10
If X, Y c U,
then the following are equivalent:
R10a. X = Y. :D2a
::
R10b. u C X <=> u C Y, for all u C U. :D2b
:R8a
::
R10c. [u C X] = [u C Y]. :R8b
::
R10d. For all u C U,
[u C X](u) = [u C Y](u). :R8c
::
R10e. ConjUu ( [u C X](u) = [u C Y](u) ). :R8d
::
R10f. ConjUu ( [u C X](u) <=> [u C Y](u) ). :R8e
::
R10g. ConjUu (( [u C X](u) , [u C Y](u) )). :R8f
::
R10h. ConjUu (( [u C X] , [u C Y] ))$(u). :R8g
Rule 11
Rule 11
If X c U
then the following are equivalent:
R11a. X = {u C U : S}. :R5a
::
R11b. {X} = { {u C U : S} }. :R5e
::
R11c. {X} c UxB
: {X} = {<u, v> C UxB : v = [S](u)}. :R
::
R11d. {X} : U -> B
: {X}(u) = [S](u), for all u C U. :R
::
R11e. {X} = [S]. :R
Fact 1
Fact 1
If X,Y c U,
then the following are equivalent:
F1a. S <=> X = Y. :R9a
::
F1b. S <=> {X} = {Y}. :R9b
::
F1c. S <=> {X}(u) = {Y}(u), for all u C U. :R9c
::
F1d. S <=> ConjUu ( {X}(u) = {Y}(u) ). :R9d
:R8a
::
F1e. [S] = [ ConjUu ( {X}(u) = {Y}(u) ) ]. :R8b
:???
::
F1f. [S] = ConjUu [ {X}(u) = {Y}(u) ]. :???
::
F1g. [S] = ConjUu (( {X}(u) , {Y}(u) )). :$1a
::
F1h. [S] = ConjUu (( {X} , {Y} ))$(u). :$1b
///
{u C U : (f, g)$(u)}
= {u C U : (f(u), g(u))}
= {u C
///