存在例化

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