ユニバーサルインスタンス化

ユニバーサルインスタンス化

タイプ	推論のルール
分野	述語論理
象徴的な声明	${\displaystyle \forall x\,A\Rightarrow A\{x\mapsto t\}}$

述語論理において、全称インスタンス化^{[1] [2] [3]}（UI、全称指定または全称消去とも呼ばれ、^[要出典]、時にはdictum de omniと混同される）^[要出典]は、個体のクラスの各メンバーに関する真理からそのクラスの特定の個体に関する真理へと推論する有効な 規則である。これは通常、全称量指定子の量化規則として与えられるが、公理スキーマにエンコードすることもできる。これは量化理論で使用される基本原理の1つである。

例: 「すべての犬は哺乳類です。フィドは犬です。したがって、フィドは哺乳類です。」

正式には、この規則は公理スキームとして次のように与えられる。

${\displaystyle \forall x\,A\Rightarrow A\{x\mapsto t\},}$

あらゆる式Aとあらゆる項tに対して、 はAにおけるxの出現ごとにt を代入した結果である。は、${\displaystyle A\{x\mapsto t\}}$ ${\displaystyle \,A\{x\mapsto t\}}$${\displaystyle \forall x\,A.}$

そして推論のルールとしてそれは

推測から${\displaystyle \vdash \forall xA}$${\displaystyle \vdash A\{x\mapsto t\}.}$

アーヴィング・コピは、普遍的インスタンス化は「1934年にゲルハルト・ゲンツェンとスタニスワフ・ヤシュコフスキが独立して考案した『自然演繹』の規則の変種から導かれる」と指摘した^。[4]

ウィラード・ヴァン・オーマン・クワインによれば、普遍的インスタンス化と存在的一般化は、単一の原理の2つの側面である。なぜなら、「∀ x  x  =  x」が「ソクラテス = ソクラテス」を意味すると言う代わりに、「ソクラテス ≠ ソクラテス」という否定が「∃ x  x  ≠  x 」を意味すると言うこともできるからである。これら2つの操作に具体化された原理は、量化と、インスタンスとしてそれらに関連付けられている特異なステートメントとの間のリンクである。しかし、それは礼儀上の原理にすぎない。それは、用語が名前を付与し、さらに参照的に出現する場合にのみ成立する。^[5]

• 実存的インスタンス化
• 存在定量化