量化子の推論規則｜述語論理での証明方法 - 記号論理学

述語論理の推論規則は、命題論理の規則に加えて、量化子を扱う規則を持ちます。全称量化子と存在量化子それぞれに導入規則と除去規則があり、これらを使って量化を含む証明を構築します。

量化子の規則の概要

量化子には、命題論理の結合子と同様に、導入規則と除去規則があります。

これらの規則は、変数の扱いに関する条件が付くため、命題論理の規則よりも注意が必要です。

全称除去（∀E）

全称除去は、「すべての x について φ(x)」から、特定の項 t について φ(t) を導く規則です。

$$\frac{\forall x\varphi (x)}{\varphi (t)}(\forall E)$ 「すべての人は死ぬ」から「ソクラテスは死ぬ」を導くようなものです。t は任意の項でよく、定項でも変項でも関数項でも構いません。 <!-- outer_1 --> ## 全称導入（∀I） 全称導入は、任意の x について φ(x) が成り立つことを示して、∀x φ(x) を導く規則です。 $\frac{\varphi (a)}{\forall x\varphi (x)}(\forall I)$ ただし、a は「任意の」対象を表す新しい定項で、証明の他の部分や仮定に現れていないものでなければなりません。この a を固有変数（eigenvariable）と呼びます。 <!-- outer_2 --> ## 存在導入（∃I） 存在導入は、特定の項 t について φ(t) が成り立つとき、∃x φ(x) を導く規則です。 $\frac{\varphi (t)}{\exists x\varphi (x)}(\exists I)$ 「2 は偶数である」から「偶数が存在する」を導くようなものです。一つでも例があれば、存在が言えます。 ## 存在除去（∃E） 存在除去は、「φ(x) を満たす x が存在する」という情報から、何かを導くための規則です。 $\frac{\exists x\varphi (x)[\varphi (a)]⋮\psi }{\psi }(\exists E)$$

∃x φ(x) が成り立つとき、φ(a) を満たす何か a があるとして推論し、ψ を導けるなら、ψ が結論できます。ただし a は固有変数で、ψ に現れてはなりません。

証明の例

∀x(P(x) → Q(x)), ∃x P(x) ⊢ ∃x Q(x) を証明してみましょう。

まず ∃x P(x) があります。存在除去を使うため、P(a) を仮定します。

∀x(P(x) → Q(x)) に全称除去を適用して P(a) → Q(a) を得ます。

P(a) と P(a) → Q(a) からモーダスポネンスで Q(a) を得ます。

存在導入で ∃x Q(x) を得ます。

存在除去により、仮定 P(a) を解消して ∃x Q(x) を結論します。

次回は、等号を含む論理について学びます。