存在例化のソースを表示

{{推論規則}}

'''存在例化'''（そんざいれいか、[[英語|英]]: '''Existential instantiation''', '''Existential elimination'''）<ref>Hurley, Patrick. ''A Concise Introduction to Logic''. Wadsworth Pub Co, 2008.</ref><ref>Copi and Cohen</ref><ref>Moore and Parker</ref>は、[[述語論理]]において、<math>(\exists x) \phi(x)</math>という形式を持った式が与えられると、新しい定数記号''c''について<math>\phi(c)</math>を推論することができるという、妥当な[[推論規則]]のひとつである。この規則は、導入された定数cが、証明にはこれまで用いられてこなかった新しい項でなければならないという制約を有する。

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

:<math>(\exists x)\mathcal{F}x :: \mathcal{F}a ,</math>

ここで''a''は、その時点まで証明に現れていない新しい定数記号である。
また、証明の結論部にも現れてはならない。

== 関連項目 ==
* [[存在の誤謬]]

== 脚注 ==
{{reflist}}

{{DEFAULTSORT:そんさいれいか}}
[[Category:推論規則]]
[[Category:述語論理]]
[[Category:数学に関する記事]]