実存的インスタンス化

実存的インスタンス化

タイプ	推論のルール
分野	述語論理
象徴的な声明	${\displaystyle \exists xP\left({x}\right)\implies P\left({a}\right)}$

述語論理において、存在的具体化（存在的消去とも呼ばれる）^{[1] [2] [3]}は、形式の式が与えられたときに、新しい定数記号cを推論できるという推論規則である。この規則には、規則によって導入される定数c は、証明のこれまでの段階では現れていない新しい項でなければならない、また、証明の結論部にも現れてはならないという制約がある。また、 にバインドされる のすべてのインスタンスは、一様にcに置き換えられなければならない。これは表記 によって暗示されているが、説明では明示的に述べられないことが多い。 ${\displaystyle (\exists x)\phi (x)}$${\displaystyle \phi (c)}$${\displaystyle x}$${\displaystyle \exists x}$${\displaystyle P\left({a}\right)}$

正式な表記法の一つでは、この規則は次のように表される。

${\displaystyle \exists xP\left({x}\right)\implies P\left({a}\right)}$

ここで、a は証明には登場していない新しい定数記号です。

• 実存的誤謬
• ユニバーサルインスタンス化
• 推論規則のリスト