\(\mathfrak{g}_{\dagger\ddagger} {}^\dagger\!\mathit{l}_\parallel {}^\parallel\!\mathrm{w} {}^\ddagger\!\mathrm{h}\)
Cactus TeX
\(\begin{array}{l}
\texttt{ } \\
\texttt{~} \\
\texttt{()} \\
\texttt{(~)} \\
\texttt{(( ))} \\
\texttt{( )( )} \\
\texttt{a b c} \\
\texttt{a~b~c} \\
\texttt{a(a)~=~(~)} \\
\texttt{a((b)(c))~=~((ab)(ac))} \\
\end{array}\)
\(\begin{array}{l}
\texttt{d}^2 \texttt{x} \\
\texttt{d}^\text{2} \texttt{x} \\
\texttt{d}^\texttt{2} \texttt{x} \\
\end{array}\)
| \(\texttt{uv~(du~dv) ~+~ u(v)~(du (dv)) ~+~ (u)v~((du) dv) ~+~ (u)(v)~((du)(dv))}\)
|
| \(\texttt{uv} \cdot \texttt{(du~dv)} + \texttt{u(v)} \cdot \texttt{(du (dv))} + \texttt{(u)v} \cdot \texttt{((du) dv)} + \texttt{(u)(v)} \cdot \texttt{((du)(dv))}\)
|
\(\begin{matrix}
\bar{(} \ldots \bar{)} &
\bar{|} \ldots \bar{|} \\
\\
\dot{(} \ldots \dot{)} &
\dot{|} \ldots \dot{|} \\
\\
\hat{(} \ldots \hat{)} &
\hat{|} \ldots \hat{|} \\
\\
\check{(} \ldots \check{)} &
\check{|} \ldots \check{|} \\
\\
\tilde{(} \ldots \tilde{)} &
\tilde{|} \ldots \tilde{|} \\
\\
\downharpoonleft \ldots \downharpoonright &
\upharpoonleft \ldots \upharpoonright \\
\\
\overline{(} \ldots \overline{)} &
\overline{|} \ldots \overline{|} \\
\\
\underline{(} \ldots \underline{)} &
\underline{|} \ldots \underline{|} \\
\\
\overline{\underline{(}} \ldots \overline{\underline{)}} &
\overline{\underline{|}} \ldots \overline{\underline{|}} \\
\\
\end{matrix}\)
|
\(\begin{array}{lllll}
{}^{_\sim}\!X
& = &
U - X
& = &
\{ \, u \in U : \underline{(} u \in X \underline{)} \, \}.
\end{array}\)
|
|
\(\begin{array}{lllll}
{}^{_\sim}\!X
& = &
U - X
& = &
\{ \, u \in U : \tilde{(} u \in X \tilde{)} \, \}.
\end{array}\)
|
- \[X = \{\ (\!|u|\!)(\!|v|\!),\ (\!|u|\!) v,\ u (\!|v|\!),\ u v\ \} \cong \mathbb{B}^2.\]
- \[X = \{\ \underline{(u)(v)},\ \underline{(u)~v},\ \underline{u~(v)},\ \underline{u~v}\ \} \cong \mathbb{B}^2.\]
- \[X = \{\!\]
(u)(v)\(,\) (u)v\(,\) u(v)\(,\) uv \(\} \cong \mathbb{B}^2.\)
- \[X = \{\!\]
(u)(v) \(,\) (u)v \(,\) u(v) \(,\) uv \(\} \cong \mathbb{B}^2.\)
- \(X = \{\!\)
(u)(v) \(,\) (u)v \(,\) u(v) \(,\) uv \(\} \cong \mathbb{B}^2.\)
- \(X = \{\!\)
(u)(v) , (u)v , u(v) , uv \(\} \cong \mathbb{B}^2.\)
Examples of Logical Orbits
Version 1
|
\(\begin{array}{ccc}
\texttt{u}' & = & \texttt{((u)(v))}
\\
\texttt{v}' & = & \texttt{((u,~v))}
\end{array}\)
|
|
\(\begin{matrix}
\text{Orbit 1}
\\
\text{Initial Point :}~ (u, v) = (1, 1)
\end{matrix}\)
|
|
\(\begin{array}{c|cc}
t & u & v \\
\\
0 & 1 & 1 \\
1 & 1 & 1 \\
2 & '' & '' \\
\end{array}\)
|
|
\(\begin{matrix}
\text{Orbit 2}
\\
\text{Initial Point :}~ (u, v) = (0, 0)
\end{matrix}\)
|
|
\(\begin{array}{c|cc}
t & u & v \\
\\
0 & 0 & 0 \\
1 & 0 & 1 \\
2 & 1 & 0 \\
3 & 1 & 0 \\
4 & '' & '' \\
\end{array}\)
|
Version 2
| \(\text{Orbit 1. Intitial Point :}~ (u, v) = (1, 1)\)
|
|
\(\begin{array}{c|cc|cc|cc|cc|cc|c}
t & u & v & du & dv & d^2 u & d^2 v & d^3 u & d^3 v & d^4 u & d^4 v & \ldots \\
\\
0 & 1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
4 & '' & '' & '' & '' & '' & '' & '' & '' & '' & '' & \ldots \\
\end{array}\)
|
| \(\text{Orbit 2. Intitial Point :}~ (u, v) = (0, 0)\)
|
|
\(\begin{array}{c|cc|cc|cc|cc|cc|c}
t & u & v & du & dv & d^2 u & d^2 v & d^3 u & d^3 v & d^4 u & d^4 v & \ldots \\
\\
0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 & 1 & 1 & 0 & \ldots \\
1 & 0 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & \ldots \\
2 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
3 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
4 & '' & '' & '' & '' & '' & '' & '' & '' & '' & '' & \ldots \\
\end{array}\)
|
Version 3
| \(\text{Orbit 1}\!\)
|
|
\(\begin{array}{c|cc|cc|}
t & u & v & du & dv \\[8pt]
0 & 1 & 1 & 0 & 0 \\
1 & '' & '' & '' & '' \\
\end{array}\)
|
|
|
| \(\text{Orbit 2}\!\)
|
|
\(\begin{array}{c|cc|cc|cc|}
t & u & v & du & dv & d^2 u & d^2 v \\[8pt]
0 & 0 & 0 & 0 & 1 & 1 & 0 \\
1 & 0 & 1 & 1 & 1 & 1 & 1 \\
2 & 1 & 0 & 0 & 0 & 0 & 0 \\
3 & '' & '' & '' & '' & '' & '' \\
\end{array}\)
|
Type Markers
Composer P
|
\(\begin{array}{l}
((x \underset{A}{:} ~y \overset{B}{\underset{A}{:}}) \underset{B}{:} ~z \overset{C}{\underset{B}{:}}) \underset{C}{:}
\end{array}\)
|
|
\(\begin{array}{l}
((x \overset{A}{:} ~y \overset{B}{\underset{A}{:}}) \overset{B}{:} ~z \overset{C}{\underset{B}{:}}) \overset{C}{:}
\end{array}\)
|
|
\(\begin{array}{l}
((x \overset{A}{\Uparrow} ~y \overset{B}{\underset{A}{\Uparrow}}) \overset{B}{\Uparrow} ~z \overset{C}{\underset{B}{\Uparrow}}) \overset{C}{\Uparrow}
\end{array}\)
|
|
\(\begin{array}{l}
((x \underset{A}{\Downarrow} ~y \overset{A}{\underset{B}{\Downarrow}}) \underset{B}{\Downarrow} ~z \overset{B}{\underset{C}{\Downarrow}}) \underset{C}{\Downarrow}
\end{array}\)
|
|
\(\begin{array}{l}
((x \overset{ }{\underset{A}{\Downarrow}} ~
y \overset{A}{\underset{B}{\Downarrow}}
) \overset{ }{\underset{B}{\Downarrow}} ~
z \overset{B}{\underset{C}{\Downarrow}}
) \overset{ }{\underset{C}{\Downarrow}}
\\ \\
=
\\ \\
(x \overset{ }{\underset{A}{\Downarrow}} ~
(y \overset{A}{\underset{B}{\Downarrow}} ~
(z \overset{B}{\underset{C}{\Downarrow}} ~
P \overset{B \Rightarrow C}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}}
) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}}
) \overset{A}{\underset{C}{\Downarrow}}
) \overset{ }{\underset{C}{\Downarrow}}
\end{array}\)
|
Transposer T
|
\(\begin{array}{l}
(y \overset{ }{\underset{B}{\Downarrow}} ~
(x \overset{ }{\underset{A}{\Downarrow}} ~
z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}
) \overset{B}{\underset{C}{\Downarrow}}
) \overset{ }{\underset{C}{\Downarrow}}
\\ \\
=
\\ \\
(x \overset{ }{\underset{A}{\Downarrow}} ~
(y \overset{ }{\underset{B}{\Downarrow}} ~
(z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~
T \overset{A \Rightarrow (B \Rightarrow C)}{\underset{B \Rightarrow (A \Rightarrow C)}{\Downarrow}}
) \overset{B}{\underset{A \Rightarrow C}{\Downarrow}}
) \overset{A}{\underset{C}{\Downarrow}}
) \overset{ }{\underset{C}{\Downarrow}}
\end{array}\)
|
Proof Example
|
\(\begin{array}{l}
(y \overset{ }{\underset{B}{\Downarrow}} ~
(x \overset{ }{\underset{A}{\Downarrow}} ~
z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}
) \overset{B}{\underset{C}{\Downarrow}}
) \overset{ }{\underset{C}{\Downarrow}}
\\ \\
=
\\ \\
((x \overset{ }{\underset{A}{\Downarrow}} ~
(y \overset{ }{\underset{B}{\Downarrow}} ~
K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}}
) \overset{A}{\underset{B}{\Downarrow}}
) \overset{ }{\underset{B}{\Downarrow}} ~
(x \overset{ }{\underset{A}{\Downarrow}} ~
z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}
) \overset{B}{\underset{C}{\Downarrow}}
) \overset{ }{\underset{C}{\Downarrow}}
\\ \\
=
\\ \\
(x \overset{ }{\underset{A}{\Downarrow}} ~
((y \overset{ }{\underset{B}{\Downarrow}} ~
K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}}
) \overset{A}{\underset{B}{\Downarrow}} ~
(z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~
S \overset{A \Rightarrow (B \Rightarrow C)}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}}
) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}}
) \overset{A}{\underset{C}{\Downarrow}}
) \overset{ }{\underset{C}{\Downarrow}}
\\ \\
=
\\ \\
\ldots
\end{array}\)
|
Over And Under Setting
-
The conjunction \(\overset{J}{\underset{j}{\operatorname{Conj}}}\ q_j\) of a set of propositions, \(\{ q_j : j \in J \},\) is a proposition that is true if and only if every one of the \(q_j\!\) is true.
\(\overset{J}{\underset{j}{\operatorname{Conj}}}\ q_j\) is true \(\Leftrightarrow\) \(q_j\!\) is true for every \(j \in J.\)
-
The surjunction \(\overset{J}{\underset{j}{\operatorname{Surj}}}\ q_j\) of a set of propositions, \(\{ q_j : j \in J \},\) is a proposition that is true if and only if exactly one of the \(q_j\!\) is untrue.
\(\overset{J}{\underset{j}{\operatorname{Surj}}}\ q_j\) is true \(\Leftrightarrow\) \(q_j\!\) is untrue for unique \(j \in J.\)
Equation Sequences
|
\(\begin{array}{lll}
[| \downharpoonleft s \downharpoonright |]
& = & [| F |]
\\[6pt]
& = & F^{-1} (\underline{1})
\\[6pt]
& = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ s ~\}
\\[6pt]
& = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ F(x, y) = \underline{1} ~\}
\\[6pt]
& = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ F(x, y) ~\}
\\[6pt]
& = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \underline{(}~x~,~y~\underline{)} = \underline{1} ~\}
\\[6pt]
& = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \underline{(}~x~,~y~\underline{)} ~\}
\\[6pt]
& = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x ~\operatorname{exclusive~or}~ y ~\}
\\[6pt]
& = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \operatorname{just~one~true~of}~ x, y ~\}
\\[6pt]
& = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x ~\operatorname{not~equal~to}~ y ~\}
\\[6pt]
& = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x \nLeftrightarrow y ~\}
\\[6pt]
& = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x \neq y ~\}
\\[6pt]
& = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x + y ~\}.
\end{array}\)
|
|
\(\begin{array}{lll}
[| F^\$ (p, q) |]
& = & [| \underline{(}~p~,~q~\underline{)}^\$ |]
\\[6pt]
& = & (F^\$ (p, q))^{-1} (\underline{1})
\\[6pt]
& = & \{~ x \in X ~:~ F^\$ (p, q)(x) ~\}
\\[6pt]
& = & \{~ x \in X ~:~ \underline{(}~p~,~q~\underline{)}^\$ (x) ~\}
\\[6pt]
& = & \{~ x \in X ~:~ \underline{(}~p(x)~,~q(x)~\underline{)} ~\}
\\[6pt]
& = & \{~ x \in X ~:~ p(x) + q(x) ~\}
\\[6pt]
& = & \{~ x \in X ~:~ p(x) \neq q(x) ~\}
\\[6pt]
& = & \{~ x \in X ~:~ \upharpoonleft P \upharpoonright (x) ~\neq~ \upharpoonleft Q \upharpoonright (x) ~\}
\\[6pt]
& = & \{~ x \in X ~:~ x \in P ~\nLeftrightarrow~ x \in Q ~\}
\\[6pt]
& = & \{~ x \in X ~:~ x \in P\!-\!Q ~\operatorname{or}~ x \in Q\!-\!P ~\}
\\[6pt]
& = & \{~ x \in X ~:~ x \in P\!-\!Q ~\cup~ Q\!-\!P ~\}
\\[6pt]
& = & \{~ x \in X ~:~ x \in P + Q ~\}
\\[6pt]
& = & P + Q ~\subseteq~ X
\\[6pt]
& = & [|p|] + [|q|] ~\subseteq~ X
\end{array}\)
|
Multiline TeX Formats
\(
\begin{cases}
a \\
b \\
c \\
\begin{cases}
d \\
e \\
f \\
\end{cases} \\
g \\
h \\
i \\
\end{cases}
\)
\(\begin{alignat}{2}
x & = (y - z)(y + z) \\
& = y^2 - z^2 \\
\end{alignat}\)
\(\begin{align}
\operatorname{Der}^L
& = & \{ & (x, y) \in S \times I ~: \\
& & & \begin{align}
\underset{o \in O}{\operatorname{Conj}} \\
& \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) & = \\
& \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) & \\
\end{align} \\
& & \} & \\
\end{align}\)
\(\begin{align}
\operatorname{Der}^L
& = & \{ & (x, y) \in S \times I ~: \\
& & & \underset{o \in O}{\operatorname{Conj}}~ (\upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o)) \\
& & \} & \\
\end{align}\)
\(\begin{align}
\operatorname{F2.2a.} \quad \operatorname{Der}^L
& = & \{ & (x, y) \in S \times I ~: \\
& & & \underset{o \in O}{\operatorname{Conj}}~ (\upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o)) \\
& & \} & \\
\end{align}\)
\(\begin{array}{lllll}
\operatorname{F2.2a.} & \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\
& & & & \underset{o \in O}{\operatorname{Conj}}~ (\upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o)) \\
& & & \} & \\
\end{array}\)
Box Displays
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
| \(\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}\)
|
|
|
