Thm③

Propの2分割

Prop \({\tt P}\) を２つに分割することがあります。

\(\&\)で分割
\({\tt P}\) = \({\tt R}_1,{\tt R}_2\)　のとき　\(\begin{cases} {\tt P\,\&l} \\ {\tt P\,\&r} \end{cases}\) = \(\begin{cases} {\tt R}_1 \\ {\tt R}_2 \end{cases}\)
\({\tt P}\) = \({\tt Q}\Rightarrow{\tt R}\)　のとき　\(\begin{cases} {\tt P\,\&l} \\ {\tt P\,\&r} \end{cases}\) = \(\begin{cases} {\tt Q}\Rightarrow({\tt R\,\&l}) \\ {\tt Q}\Rightarrow({\tt R\,\&r}) \end{cases}\)
\({\tt P}\) = \(\forall{\tt xQ}\)　のとき　\(\begin{cases} {\tt P\,\&l} \\ {\tt P\,\&r} \end{cases}\) = \(\begin{cases} \forall{\tt x}({\tt Q\,\&l}) \\ \forall{\tt x}({\tt Q\,\&r}) \end{cases}\)

\(\Leftrightarrow\)を分割
\({\tt P}\) = \({\tt R}_1 \Leftrightarrow {\tt R}_2\)　のとき　\(\begin{cases} {\tt P}\,{\tt {\text -}\!\!>} \\ {\tt P}\,{\tt <\!\!{\text -}} \end{cases}\) = \(\begin{cases} {\tt R}_1\Rightarrow{\tt R}_2 \\ {\tt R}_2\Rightarrow{\tt R}_1 \end{cases}\)
\({\tt P}\) = \({\tt Q}\Rightarrow{\tt R}\)　のとき　\(\begin{cases} {\tt P}\,{\tt {\text -}\!\!>} \\ {\tt P}\,{\tt <\!\!{\text -}} \end{cases}\) = \(\begin{cases} {\tt Q}\Rightarrow({\tt R}\,{\tt {\text -}\!\!>}) \\ {\tt Q}\Rightarrow({\tt R}\,{\tt <\!\!{\text -}}) \end{cases}\)
\({\tt P}\) = \(\forall{\tt xQ}\)　のとき　\(\begin{cases} {\tt P}\,{\tt {\text -}\!\!>} \\ {\tt P}\,{\tt <\!\!{\text -}} \end{cases}\) = \(\begin{cases} \forall{\tt x}({\tt Q}\,{\tt {\text -}\!\!>}) \\ \forall{\tt x}({\tt Q}\,{\tt <\!\!{\text -}}) \end{cases}\)

例　\({\emptyset.}\) ≃【\(\forall x \, ( x \in \emptyset {\perp} )\)】

Rite

Prop , \(\mathbb{D}.\) , \({\bf /}\) , \(\rfloor\) , \(\lfloor\) 等から作られるものを Rite と呼びます。Riteもp-Formを指し示します。
Riteのinputでは区切りはスペースとしますが、( ) の前後のスペースは略せます。

Thmの分割

次に注意しましょう。\({\tt P}\) ≡ \({\tt P\,\&l} , {\tt P\,\&r}\)
\({\tt P}\blacktriangleleft\mathcal{A}\) を \({\tt P\,\&l}, {\tt P\,\&r} \,\blacktriangleleft\, \mathcal{A}\) と分割して証明させることが行われます。

\({\tt PX}\blacktriangleleft\mathcal{A},{\tt PY}\blacktriangleleft\mathcal{B}\) を \({\tt P}\big[{\tt X}\blacktriangleleft\mathcal{A} \,\pmb{\big|}\, {\tt Y}\blacktriangleleft\mathcal{B}\big]\) と表します。分配則みたいに。
入れ子にできます。\({\tt P}\) を示すのに \({\tt P}\big[{\tt \&l} \blacktriangleleft \mathcal{A} \,{\big|}\, {\tt \&r} \big[{\tt \&l} \blacktriangleleft \mathcal{B} \,{\big|}\, {\tt \&r} \blacktriangleleft\, \mathcal{C}\big]\big]\) のように3分割したりします。

\({\tt \&l} \blacktriangleleft \text{O}\) や \({\tt {\text -}\!\!>} \blacktriangleleft \text{O}\) は略せます。
\({\tt P}\big[{\tt \&r} \blacktriangleleft \mathcal{A}\big]\) は \({\tt P}\big[{\tt \&l} \blacktriangleleft \text{O} \,{\big|}\, {\tt \&r} \blacktriangleleft \mathcal{A}\big]\) の略です。