存在例化

存在例化（そんざいれいか、英: 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は、その時点まで証明に現れていない新しい定数記号である。 また、証明の結論部にも現れてはならない。

関連項目

• 存在の誤謬