論理同値
\(\text{O}\,{\blacktriangleright}\,{\tt P}\Leftrightarrow{\tt Q}\) となるとき、\({\tt P}\)と\({\tt Q}\)は論理同値と言われ、\({\tt P}\) ≡ \({\tt Q}\) と書かれます。例 \({\tt P}\Rightarrow{\tt Q}\) ≡ \(\neg{\tt P}\,{\rm o\!r}\,{\tt Q}\)
\({\tt P} \stackrel{\rm v}= {\tt Q}\) なら \({\tt P}\) ≡ \({\tt Q}\) です。
特に論理同値でより短いものを論理短縮と言うことがあります。例 \(\neg\neg{\tt P}\) ≡ \({\tt P}\) \(\neg{\tt P}\Rightarrow\neg{\tt Q}\) ≡ \({\tt Q}\Rightarrow{\tt P}\)
\(\emptyset{.}{.}\)【\(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\)】
これは【\(x \neq \emptyset \Longleftrightarrow \exists y \, ( y \in x )\)】と論理同値ですが、これにしてしまうと \({\bf /}\emptyset{.}{.}\) が使いにくくなってしまいます。
Propの紹介
「数学の教科書」での紹介時には、それが指し示すp-Formよりきれいなものの表記が現れることがあります。
濃度が等しいことを表すword(ss,p)に \(\stackrel{\#}=\) があり、次のように紹介されています。\(\stackrel{\#}=.\)【\(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\)】\({\bf /}\emptyset{.}{.}\)
実際に\(\stackrel{\#}=.\) が指し示すp-Formは
【\(X \stackrel{\#}= Y \Longleftrightarrow \neg \neg \exists f \, ( f \in X \stackrel{\rm IS}\to Y )\)】
のさらに論理短縮である
【\(X \stackrel{\#}= Y \Longleftrightarrow \exists f \, ( f \in X \stackrel{\rm IS}\to Y )\)】
と登録されています。
Propの2分割
Prop \({\tt P}\) を２つに分割するProp関数があり、証明のためのヒントを記述する際に多く使用されます。
\(\&\)で分割
\({\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}\)
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]\) の略です。