存在導入
論理式\(A\)が変数\(x\in X\)の自由な現れを持つ開論理式\(A\left( x\right) \)である状況を想定します。開論理式\(A\left( x\right) \)の真偽を判定するためには変数\(x\)に何らかの値を代入する必要があります。そこで、ある値\(c\in X\)のもとで\(A\left( c\right) \)が真である状況を想定します。この場合、以下の推論規則\begin{equation*}A\left( c\right) \ \models \ \exists x\in X:A\left( x\right)
\end{equation*}が成り立つものと定め、これを存在導入（existential introduction）や\(\exists \)導入（\(\exists \) introduction）、存在汎化（existential generalization）などと呼びます。
繰り返しになりますが、存在導入中の\(c\)は命題\(A\left( c\right) \)が真になるような値を表す記号です。この値は具体的な値であってもよいし、その値を表す記号でもよいです。命題\(A\left( c\right) \)が真であることは、論理式\(A\left( x\right) \)が真になるような\(x\)の値が\(X\)に存在することを意味するため、ここから、\begin{equation*}\exists x\in X:A\left( x\right)
\end{equation*}を導出できるということです。
\end{equation*}が与えられているものとします。これは変数\(x\)の自由な現れを持つ開論理式です。ある値\(c\in X\)のもとで、\begin{equation*}P\left( c\right) \wedge Q\left( c\right)
\end{equation*}が真であるものとします。この場合、存在導入より、\begin{equation*}
\exists x\in X:\left( P\left( x\right) \wedge Q\left( x\right) \right)
\end{equation*}が導かれます。
\right)
\end{equation*}が与えられているものとします。これは変数\(x\)の自由な現れを持つ開論理式です。ある値\(c\in X\)のもとで、\begin{equation*}\exists y\in X:\left( P\left( c,y\right) \rightarrow Q\left( c\right)
\right)
\end{equation*}が真であるものとします。この場合、存在導入より、\begin{equation*}
\exists x\in X,\ \exists y\in X:\left( P\left( x,y\right) \rightarrow
Q\left( x\right) \right)
\end{equation*}が導かれます。
\end{equation*}が成り立つということです。この場合、存在導入より、\begin{equation*}
\exists x\in \mathbb{R} :x>0
\end{equation*}が導かれます。\(c\)の値をより具体的に特定するのであれば、例えば、\begin{equation*}1>0\ \models \ \exists x\in \mathbb{R} :x>0
\end{equation*}もまた成り立ちます。
&&\text{太郎は日本人である} \\
&&\text{したがって、日本人が存在する}
\end{eqnarray*}ただし、変数\(x\)の定義域\(X\)はすべての人間からなる集合です。以下の命題関数\begin{equation*}P\left( x\right) :x\text{は日本人である}
\end{equation*}を定義すると、与えられた推論は、\begin{equation*}
P\left( \text{太郎}\right) \ \therefore \ \exists x\in X:P\left(
x\right)
\end{equation*}と定式化されます。前提である、\begin{equation*}
P\left( \text{太郎}\right)
\end{equation*}に存在導入を適用すると、\begin{equation*}
\exists x\in X:P\left( x\right)
\end{equation*}を得ます。したがって、与えられた推論が妥当であることが示されました。
存在導入に関する制約
論理式\(A\)が変数\(x\in X\)の自由な現れを持つ開論理式\(A\left( x\right) \)である場合、存在導入とは、\begin{equation*}A\left( c\right) \ \models \ \exists x\in X:A\left( x\right)
\end{equation*}と定義される推論規則です。ただし、\(c\in X\)は命題\(A\left( c\right) \)が真であるような対象を表す記号です。この推論規則の前提\(A\left( c\right) \)の中に変数\(x\)の自由な現れが残存している場合、存在導入を適用して変数\(x\)に関する存在命題を導くことはできません。存在量化しようとしている変数\(x\)が推論の前提において自由変数として残っていてはいけないということです。変数\(x\)に関する存在命題\begin{equation*}\exists x\in X:A\left( x\right)
\end{equation*}を導く前に、前提\(A\left(c\right) \)の中に変数\(x\)の自由な現れが残っていないことを確認する必要があります。
\end{equation}が与えられているものとします。開論理式\(\left( 1\right) \)には変数\(x\)の自由な現れが残存しています。それにも関わらず存在導入を適用して変数\(x\)に関する存在命題\begin{equation}\exists x\in \mathbb{R} :\left( x\not=x\vee x>x\right) \quad \cdots (2)
\end{equation}を導出すると何がおこるでしょうか。つまり、\begin{equation}
\left( x\not=c\vee x>c\right) \ \models \ \exists x\in \mathbb{R} :\left( x\not=x\vee x>x\right) \quad \cdots (3)
\end{equation}を得るということです。実際には\(\left( 2\right) \)は偽であるため、\(\left( 3\right) \)は成り立ちません。このような問題をもたらした原因は、\(\left(3\right) \)の前提である\(\left( 1\right) \)の中に変数\(x\)の自由な現れが残っているにも関わらず、\(c\)から\(\exists x\in \mathbb{R} \)を導いてしまったことにあります。ちなみに、変数\(x\)とは異なる変数\(y\)を選んだ場合、\(\left( 1\right) \)には変数\(y\)の自由な現れが存在しないため、\(\left( 1\right) \)から変数\(y\)に関する存在命題\begin{equation*}\exists y\in \mathbb{R} :\left( x\not=y\vee x>y\right)
\end{equation*}を導出することはできます。つまり、\begin{equation*}
\left( x\not=c\vee x>c\right) \ \models \ \exists y\in \mathbb{R} :\left( x\not=y\vee x>y\right)
\end{equation*}は妥当な推論規則です。
演習問題
&&\text{すべての人間は死ぬ} \\
&&\text{ソクラテスは人間である} \\
&&\text{したがって、死ぬ者が存在する}
\end{eqnarray*}
