存在例化

演繹の推論規則
命題計算
モーダスポネンス モーダストレンス モーダスポネンストレンス（英語版） 連言導入 簡単化 選言導入 選言除去 選言三段論法 仮言三段論法 構成的ジレンマ（英語版） 破壊的ジレンマ（英語版） 二条件導入（英語版） 二条件除去（英語版）
述語計算
普遍汎化 普遍例化 存在汎化 存在例化
カテゴリ:推論規則
表 話 編 歴

存在例化（そんざいれいか、英: Existential instantiation, Existential elimination）^[1][2][3]は、述語論理において、${\displaystyle (\exists x)\phi (x)}$という形式を持った式が与えられると、新しい定数記号cについて${\displaystyle \phi (c)}$を推論することができるという、妥当な推論規則のひとつである。この規則は、導入された定数cが、証明にはこれまで用いられてこなかった新しい項でなければならないという制約を有する。

例えば、形式的な記法においては、規則は次のように表記される。

${\displaystyle (\exists x){\mathcal {F}}x::{\mathcal {F}}a,}$

ここでaは、その時点まで証明に現れていない新しい定数記号である。

• 存在の誤謬