一階述語論理

索引トップ用語の索引ランキングカテゴリー

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/05/15 09:03 UTC 版)

形式的証明

命題論理においては、論理公理 (logical axiom) と呼ぶ論理式の集合と、ある論理式たちから新たな論理式を導出する規則（推論規則）を導入し、論理公理から推論規則の有限回の適用によって得られる論理式全体とトートロジー全体が一致するようにすることができる（命題論理の健全性と完全性）。一階述語論理においても、適切に論理公理と推論規則を導入することで、論理公理から推論規則を使って導出される論理式全体と恒真論理式全体が一致するようにできる。

形式的証明の定義の仕方はひとつではなく、様々な異なる（等価な）方法がある。ここで述べる定義はヒルベルト流計算の典型例であり、これは異なる公理を多数用意して推論規則を少なくするスタイルをとっている。ゲンツェン流の形式的証明では逆に、公理を少なくして推論規則を多く用いている。ここで述べるものと異なる証明可能性の定義については「自然演繹」「シークエント計算」などを参照。

論理公理

以下の形の論理式すべてを論理公理とする。ここで、x, y は変数、t, t₁ , ..., t_n は項、φ, ψ は論理式を表す：

トートロジー（命題論理におけるトートロジーの命題記号を一階の論理式で置き換えて得られる論理式）
量化記号に関する公理

∀x φ → φ_x [ t ] 　（ただし、φ において t が x に代入可能（後述）の場合に限る）
∀x (φ → ψ) → (∀x φ → ∀x ψ)
∀x (¬ φ) ↔ (¬ ∃x φ)

等号に関する公理（言語が等号を持つ場合に限る）

x = x
x = y → (P t₁ … t_n → P u₁ … u_n) 　（ただし、P は n 変数述語記号で、u_i は t_i における x のいくつかを y で置き換えて得られる項である）

量化記号に関する公理 1. における φ_x [ t ] とは、論理式 φ において "束縛されていない" 変数 x をすべて項 t で置き換えて得られる論理式を表す（正確な定義は後述）。

推論規則

推論規則とは、あるいくつかの論理式から別の論理式を導出するための規則である。これは正確には、論理式全体の集合の上の関係として定義される。推論規則には様々なものが考えられるが、ここで用いる推論規則はモーダス・ポーネンス (modus ponens) と呼ぶ規則と全称化 (generalization) と呼ぶ規則の二つである。

モーダス・ポーネンス (MP)

モーダス・ポーネンスとは、φ と (φ → ψ) から ψ を導出してよいという規則である。これは、論理式全体の集合の上の関係としては次のように定義することができる：

MP = { (φ, (φ → ψ), ψ) | φ と ψ は論理式 } 。

(φ₁, φ₂, φ₃) ∈ MP であるとき、φ₃ は φ₁, φ₂ からのモーダス・ポーネンスによる導出であるという。

全称化 (GEN)

全称化規則とは、x が変数のとき、φ から ∀x φ を導出してよいという規則である。これは、論理式全体の集合の上の関係としては次のように定義することができる：

GEN = { (φ, ∀x φ) | φ は論理式かつ x は変数 } 。

(φ₁, φ₂) ∈ GEN であるとき、φ₂ は φ₁ からの全称化による導出であるという。

証明可能性

論理式 φ が論理式の集合 Σ から証明可能であるとは、Σ に属する論理式と論理公理から推論規則の有限回の適用によって φ が得られることを意味する。そして、Σ に属する論理式と論理公理から φ を導出する仮定を示した論理式の有限列を、Σ からの φ の形式的証明とよぶ。これらの概念は次のように厳密に定義することができる。

φ を論理式、Σ を論理式の集合とする。Σ からの φ の形式的証明 (formal proof) あるいは証明 (proof) とは、論理式の有限列 (φ₀, ..., φ_n) で次をみたすものをいう：

φ_n = φ 。
n 以下の任意の自然数 k に対して、次のいずれかが成り立つ：

(a) φ_k ∈ Σ 。

(b) φ_k は論理公理である。

(d) ある i < k が存在して、φ_k は φ_i からの全称化による導出である。

Σ からの φ の証明が存在するとき、φ は Σ から証明可能 (provable) である、あるいは φ は Σ の定理 (theorem) であるといい、

\Sigma \vdash \varphi

と書く。

代入について

φ_x [ t ] は、論理式 φ において "束縛されていない" 変数 x をすべて項 t で置き換えて得られる論理式を表すと述べた。正確には、φ_x [ t ] は再帰によって次に述べるような仕方で定義される。

まず、それぞれの項 u に対して u_x [ t ] を次のように再帰的に定義する：

x_x [ t ] = t 。
y が x と異なる変数ならば、y_x [ t ] = y 。
c 定数記号ならば、c_x [ t ] = c 。
t₁ , ..., t_n が項で、f がアリティ n の関数記号ならば、(f t₁ … t_n)_x [ t ] = f (t₁)_x [ t ] … (t_n)_x [ t ] 。

そして、φ_x [ t ] を次のように再帰的に定義する：

原子論理式 P t₁ … t_n に対しては、(P t₁ … t_n)_x [ t ] = P (t₁)_x [ t ] … (t_n)_x [ t ] 。
(¬ φ)_x [ t ] = (¬ φ_x [ t ])
(φ ∧ ψ)_x [ t ] = (φ_x [ t ] ∧ ψ_x [ t ])
(φ ∨ ψ)_x [ t ] = (φ_x [ t ] ∨ ψ_x [ t ])
(φ → ψ)_x [ t ] = (φ_x [ t ] → ψ_x [ t ])
(φ ↔ ψ)_x [ t ] = (φ_x [ t ] ↔ ψ_x [ t ])
(∀x φ)_x [ t ] = ∀x φ 、(∃x φ)_x [ t ] = ∃x φ 。
y が x と異なる変数ならば、(∀y φ)_x [ t ] = ∀y φ_x [ t ] 、(∃y φ)_x [ t ] = ∃y φ_x [ t ] 。

次に、論理式 φ において項 t が変数 x に代入可能であるということを定義する。このことの直観的な意味は、φ が x について述べていることと同じことを φ_x [ t ] が t について述べているということである。例えば、。これに対して、。代入可能性の正式な定義は次の通りである。

論理式 φ において項 t が変数 x に代入可能 (substitutable) であるということを次のように再帰的に定義する：

原子論理式においては、常に t は x に代入可能である。
(¬ φ) において t が x に代入可能　⇔　 φ において t が x に代入可能。
(φ ∧ ψ) において t が x に代入可能　⇔　 φ と ψ において t が x に代入可能。
(φ ∨ ψ) において t が x に代入可能　⇔　 φ と ψ において t が x に代入可能。
(φ → ψ) において t が x に代入可能　⇔　 φ と ψ において t が x に代入可能。
(φ ↔ ψ) において t が x に代入可能　⇔　 φ と ψ において t が x に代入可能。
∀y φ において t が x に代入可能　⇔　 x ≠ y または x ∉ fr(φ) または（φ において t が x に代入可能かつ t の中に y が現れない）。
∃y φ において t が x に代入可能　⇔　 x ≠ y または x ∉ fr(φ) または（φ において t が x に代入可能かつ t の中に y が現れない）。

等号に関する公理について

等号に関する公理の 2. は、

x = y → (P t₁ … t_n → P u₁ … u_n) 　（ただし、P は n 変数述語記号で、u_i は t_i における x のいくつかを y で置き換えて得られる項である）

となっている。ここで、項 u が項 t における x のいくつかを y で置き換えて得られる項であるということは正確には次のように定義される。

変数 x と y を固定し、項の間の関係 ≈ を次のように再帰的に定義する：

x ≈ u 　⇔　 u = x または u = y 。
z が x と異なる変数ならば、z ≈ u 　⇔　 u = z 。
c 定数記号ならば、c ≈ u 　⇔　 u = c 。
t₁ , ..., t_n が項で、f がアリティ n の関数記号ならば、f t₁ … t_n ≈ u 　⇔　 t₁ ≈ u₁ , ..., t_n ≈ u_n であるような u₁ , ..., u_n が存在して u = f u₁ … u_n 。

t ≈ u であるとき、u は t における x のいくつかを y で置き換えて得られる項であるという。

脚注

^ 「アリティ」という用語は通常、関係や関数がとる変数の個数を表す言葉として用いられるが、ここでの意味はそれとは異なることに注意しなければならない。述語記号や関数記号は単なる記号であって関係や関数ではなく、アリティというのはそれらの記号が持っているある正の整数という意味にすぎない。
^ 読みやすさを優先させて $ft_{1},\,\cdots ,\,t_{n}$ の代わりに $f(t_{1},\,\cdots ,\,t_{n})$ を用いる流儀も存在する。その場合は言語にカンマ "," を含めておく必要がある。