存在例化
表示
演繹の推論規則 |
---|
命題計算 |
モーダスポネンス |
述語計算 |
存在例化 |
カテゴリ:推論規則 |
存在例化(そんざいれいか、英: Existential instantiation, Existential elimination)[1][2][3]は、述語論理において、という形式を持った式が与えられると、新しい定数記号cについてを推論することができるという、妥当な推論規則のひとつである。この規則は、導入された定数cが、証明にはこれまで用いられてこなかった新しい項でなければならないという制約を有する。
例えば、形式的な記法においては、規則は次のように表記される。
ここでaは、その時点まで証明に現れていない新しい定数記号である。