存在導入
論理式\(A\)が変数\(x\in X\)の自由な現れを持つ開論理式\(A\left( x\right) \)であるものとします。定義域\(X\)に属するある対象\(c\in X\)のもとで、\begin{equation*} A\left( c\right)
\end{equation*}が真である場合、\begin{equation*}
\exists x\in X:A\left( x\right)
\end{equation*}が成り立つものと定めます。このような推論規則\begin{equation*}
A\left( c\right) \ \models \ \exists x\in X:A\left( x\right)
\end{equation*}を存在導入（existential introduction）や\(\exists \)導入（\(\exists \) introduction）、存在汎化（existential generalization）などと呼びます。
存在導入を適用するためには前提として\(A\left( c\right) \)が真であることを示す必要がありますが、ここでの\(c\)は定義域\(X\)に属する具体的な対象であっても、\(X\)に属するある対象を表す抽象的な記号であっても構いません。ただし、存在命題\begin{equation*} \exists x\in X:A\left( x\right)
\end{equation*}は\(X\)に属する対象の中に\(A\)を満たすものが存在する、という主張であるため、その根拠となる\(A\left( c\right) \)中の\(c\)は\(X\)の要素である必要があります。\(X\)に属さない対象を存在導入の根拠として利用することはできません。
また、存在導入を用いて\(A\left( c\right) \)から存在命題\(\exists x\in X:A\left( x\right) \)を導出する際には、存在導入によって一般化する対象\(c\)とは関係のない、もともとの自由変数まで誤って束縛しないように注意する必要があります。この注意点については後述します。
例（存在導入）
変数\(x\in X\)および命題関数\(P\left( x\right) ,Q\left( x\right) \)に関する論理式\begin{equation*} P\left( x\right) \wedge Q\left( x\right)
\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*}が導かれます。
\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*}が導かれます。
例（存在導入）
変数\(x,y\in X\)および命題関数\(P\left( x,y\right) ,Q\left( x\right) \)に関する論理式\begin{equation*} \exists y\in X:\left( P\left( x,y\right) \rightarrow Q\left( x\right) \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*}が与えられているものとします。これは変数\(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*}が導かれます。
例（存在導入）
正の実数\(c\in \mathbb{R} \)が与えられているものとします。つまり、\begin{equation*} c>0
\end{equation*}が成り立つということです。この場合、存在導入より、\begin{equation*}
\exists x\in \mathbb{R} :x>0
\end{equation*}が導かれます。また、具体的な値\(c=1\)について、\begin{equation*} 1>0
\end{equation*}が成り立つため、この場合にも存在導入より、\begin{equation*}
\exists x\in \mathbb{R} :x>0
\end{equation*}が導かれます。
\end{equation*}が成り立つということです。この場合、存在導入より、\begin{equation*}
\exists x\in \mathbb{R} :x>0
\end{equation*}が導かれます。また、具体的な値\(c=1\)について、\begin{equation*} 1>0
\end{equation*}が成り立つため、この場合にも存在導入より、\begin{equation*}
\exists x\in \mathbb{R} :x>0
\end{equation*}が導かれます。
例（存在導入）
以下の推論について考えます。\begin{eqnarray*}
&&\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*}と定式化されます。太郎は\(X\)の要素であるため、\begin{equation*} P\left( \text{太郎}\right)
\end{equation*}に存在導入を適用でき、その結果、\begin{equation*}
\exists x\in X:P\left( x\right)
\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*}と定式化されます。太郎は\(X\)の要素であるため、\begin{equation*} P\left( \text{太郎}\right)
\end{equation*}に存在導入を適用でき、その結果、\begin{equation*}
\exists x\in X:P\left( x\right)
\end{equation*}が得られます。したがって、与えられた推論が妥当であることが示されました。
存在導入に関する制約
存在導入を適用する際に、もともと自由に現れていた変数まで新たな量化記号の作用域に取り込んでしまうことを変数の捕獲と呼びます。変数の捕獲が生じると論理式の意味が変わってしまうため、変数の捕獲を伴う形で存在導入を適用することはできません。
例（変数の捕獲）
変数\(x\)の定義域はすべての実数からなる集合\(\mathbb{R} \)であり、\(c\in \mathbb{R} \)であるものとします。以下の論理式\begin{equation} \left( x\not=c\vee x>c\right) \quad \cdots (1)
\end{equation}が与えられているものとします。開論理式\(\left( 1\right) \)には変数\(x\)の自由な現れが残存しています。\(c\)は存在導入によって一般化しようとしている対象ですが、\(c\)を存在量化する際に、もともと自由変数として使われている\(x\)と同じ変数を用いて、\begin{equation} \exists x\in \mathbb{R} :\left( x\not=x\vee x>x\right) \quad \cdots (2)
\end{equation}とすることはできません。\(\left( 2\right) \)では、もとの式\(\left( 1\right) \)に自由変数として現れていた\(x\)が存在記号\(\exists x\in \mathbb{R} \)によって束縛されており、変数の捕獲が生じています。変数の捕獲が生じると論理式の意味が変わってしまいます。実際、\(\left( 1\right) \)は\(x\)と\(c\)の値の選び方によっては真になる一方で、\(\left( 2\right) \)は常に偽であるため、\begin{equation*} \left( x\not=c\vee x>c\right) \ \models \ \exists x\in \mathbb{R} :\left( x\not=x\vee x>x\right)
\end{equation*}は成り立ちません。これは存在導入の誤用です。一方、もともとの自由変数\(x\)とは異なる変数\(y\)を用いれば、変数の捕獲を避けることができます。つまり、\(\left( 1\right) \)から変数\(y\)に関する存在命題\begin{equation*} \exists y\in \mathbb{R} :\left( x\not=y\vee x>y\right)
\end{equation*}を導くことはできます。この場合、もとの自由変数\(x\)は自由なまま残り、\(c\)に対して導入された変数\(y\)だけが存在記号によって束縛されているため、変数の捕獲は生じていません。したがって、\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*}は成り立ちます。
\end{equation}が与えられているものとします。開論理式\(\left( 1\right) \)には変数\(x\)の自由な現れが残存しています。\(c\)は存在導入によって一般化しようとしている対象ですが、\(c\)を存在量化する際に、もともと自由変数として使われている\(x\)と同じ変数を用いて、\begin{equation} \exists x\in \mathbb{R} :\left( x\not=x\vee x>x\right) \quad \cdots (2)
\end{equation}とすることはできません。\(\left( 2\right) \)では、もとの式\(\left( 1\right) \)に自由変数として現れていた\(x\)が存在記号\(\exists x\in \mathbb{R} \)によって束縛されており、変数の捕獲が生じています。変数の捕獲が生じると論理式の意味が変わってしまいます。実際、\(\left( 1\right) \)は\(x\)と\(c\)の値の選び方によっては真になる一方で、\(\left( 2\right) \)は常に偽であるため、\begin{equation*} \left( x\not=c\vee x>c\right) \ \models \ \exists x\in \mathbb{R} :\left( x\not=x\vee x>x\right)
\end{equation*}は成り立ちません。これは存在導入の誤用です。一方、もともとの自由変数\(x\)とは異なる変数\(y\)を用いれば、変数の捕獲を避けることができます。つまり、\(\left( 1\right) \)から変数\(y\)に関する存在命題\begin{equation*} \exists y\in \mathbb{R} :\left( x\not=y\vee x>y\right)
\end{equation*}を導くことはできます。この場合、もとの自由変数\(x\)は自由なまま残り、\(c\)に対して導入された変数\(y\)だけが存在記号によって束縛されているため、変数の捕獲は生じていません。したがって、\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*}は成り立ちます。
演習問題
問題（存在導入）
変数\(x\)の定義域はすべての整数からなる集合\(\mathbb{Z} \)であるものとします。「\(4\)は偶数である」という命題に対して存在導入を適用することにより得られる論理式を記述し、その意味を説明してください。
問題（存在導入）
実数\(a,b\in \mathbb{R} \)について\(a+b=5\)が成り立っているものとします。このとき、存在導入を1回だけ使用することにより得られる論理式をすべて書き出してください。
問題（存在導入）
以下の推論が妥当であることを示してください。\begin{eqnarray*}
&&\text{すべての人間は死ぬ} \\
&&\text{ソクラテスは人間である} \\
&&\text{したがって、死ぬ者が存在する}
\end{eqnarray*}
&&\text{すべての人間は死ぬ} \\
&&\text{ソクラテスは人間である} \\
&&\text{したがって、死ぬ者が存在する}
\end{eqnarray*}
問題（存在導入）
変数\(x\)の定義域を整数全体からなる集合\(\mathbb{Z} \)とします。命題 \begin{equation*}
3^{2}=9
\end{equation*}に存在導入を適用して得られる存在命題を1つ記述してください。
3^{2}=9
\end{equation*}に存在導入を適用して得られる存在命題を1つ記述してください。
問題（存在導入と自由変数）
変数\(x,y\)の定義域をともに\(X\)とします。ある\(c\in X\)について、 \begin{equation*}
P\left( x,c\right)
\end{equation*}が真であるものとします。このとき、存在導入によって変数\(y\)に関する存在命題を導いてください。
P\left( x,c\right)
\end{equation*}が真であるものとします。このとき、存在導入によって変数\(y\)に関する存在命題を導いてください。
問題（存在導入と変数の捕獲）
ある\(c\in X\)について、 \begin{equation*}
P\left( x,c\right)
\end{equation*}が真であるものとします。この式から、単に\(c\)を\(x\)に置き換えることによって、 \begin{equation*}
\exists x\in X:P\left( x,x\right)
\end{equation*}を導くことができるでしょうか。
P\left( x,c\right)
\end{equation*}が真であるものとします。この式から、単に\(c\)を\(x\)に置き換えることによって、 \begin{equation*}
\exists x\in X:P\left( x,x\right)
\end{equation*}を導くことができるでしょうか。
問題（存在導入と定義域）
変数\(x\)の定義域を整数全体からなる集合\(\mathbb{Z} \)とします。命題 \begin{equation*}
\left( \frac{1}{2}\right) ^{2}>0
\end{equation*}から、
\begin{equation*}
\exists x\in \mathbb{Z} :x^{2}>0
\end{equation*}を存在導入によって導くことができるでしょうか。
\left( \frac{1}{2}\right) ^{2}>0
\end{equation*}から、
\begin{equation*}
\exists x\in \mathbb{Z} :x^{2}>0
\end{equation*}を存在導入によって導くことができるでしょうか。
問題（存在導入の反復）
実数\(a,b\in \mathbb{R} \)について、 \begin{equation*}
a<b
\end{equation*}が成り立つものとします。存在導入を2回適用することにより、\(a\)と\(b\)の両方を存在量化してください。
a<b
\end{equation*}が成り立つものとします。存在導入を2回適用することにより、\(a\)と\(b\)の両方を存在量化してください。
問題（存在導入）
以下の推論が妥当であることを示してください。
\begin{eqnarray*}
&&\text{太郎は学生である。} \\
&&\text{太郎は数学を学んでいる。} \\
&&\text{したがって、数学を学んでいる学生が存在する。}
\end{eqnarray*}
\begin{eqnarray*}
&&\text{太郎は学生である。} \\
&&\text{太郎は数学を学んでいる。} \\
&&\text{したがって、数学を学んでいる学生が存在する。}
\end{eqnarray*}
