一階述語論理

一階述語論理

一階述語論理は、数理[[論理学]]における中心的な論理体系であり、個体に対する量化のみを認める述語論理です。命題論理を拡張したもので、より複雑な推論を可能にします。ここでは、一階述語論理の概要、命題論理との差異、表現力、形式的定義、および関連する重要な概念について解説します。

概要

一階述語論理は、命題論理の枠組みを超え、個体の性質や関係を扱うことができます。命題論理では、文を最小単位である命題記号で表しますが、一階述語論理では、述語記号と項の組み合わせである原子論理式を用いて命題を表現します。また、量化の概念を導入することで、「すべての～」や「ある～」といった表現を扱うことができるようになります。

命題論理との差異

命題論理では、文を構成する最も基本的な命題は単一の記号（命題記号）で表されます。一方、一階述語論理では、原子論理式と呼ばれる記号列で基本的な命題を表します。原子論理式は、述語記号と、項（個体を表す記号）の列から構成されます。例えば、`P(t1, t2, ..., tn)`という形式で、これは個体間の関係を示します。

また、一階述語論理の重要な特徴として量化があります。命題論理では扱えない、「すべての～」や「ある～」といった概念を、全称量化記号（∀）と存在量化記号（∃）を用いることで表現します。

例えば、「すべての人間は死ぬ」という文は、一階述語論理では`∀x[P(x) ⇒ Q(x)]`と表現できます。ここで、`P(x)`は「xは人間である」、`Q(x)`は「xは死ぬ」を表します。

一階述語論理の表現力

一階述語論理は、数学のほぼ全領域を形式化するのに十分な表現力を持っています。現代の標準的な集合論の公理系ZFCは一階述語論理を用いて形式化されており、数学の大部分はそのように形式化されたZFCの中で行うことができます。

一階述語論理の形式的定義

一階の言語

一階述語論理の言語は、論理記号と非論理記号から構成されます。

• - 論理記号

- 変数：`V = {x1, x2, ...}`
- 結合記号：`¬, ∧, ∨, ⇒, ⇔`
- 量化記号：`∀, ∃`
- 括弧：`( ), [ ], { }`
- 等号：`=`

• - 非論理記号

- 述語記号（アリティを持つ）
- 関数記号（アリティを持つ）
- 定数記号

一階の言語は、等号を含むか、非論理記号として何を持つかによって定義されます。例えば、集合論では、等号とアリティ2の述語記号`∈`を持つ言語が使われます。

項

一階述語論理の項は、次のように帰納的に定義されます。

1. 変数と定数記号はすべて項です。
2. `t1, ..., tn`が項で、`f`がアリティ`n`の関数記号ならば、`f(t1, ..., tn)`は項です。

項は、議論領域に属する対象を表す名前のような役割を持ちます。

論理式

論理式は、原子論理式から結合記号と量化記号を用いて構成される、命題を表す記号列です。

1. 原子論理式：アリティ`n`の述語記号`P`と`n`個の項`t1, ..., tn`を用いて、`P(t1, ..., tn)`と表される記号列。
2. 論理式の構成：`φ`と`ψ`が論理式ならば、
- `(¬φ)`
- `(φ ∧ ψ)`
- `(φ ∨ ψ)`
- `(φ ⇒ ψ)`
- `(φ ⇔ ψ)`
も論理式です。また、`φ`が論理式で`x`が変数ならば、
- `(∀x φ)`
- `(∃x φ)`
も論理式です。

自由変数

論理式中の変数は、量化記号によって束縛されているか、そうでないか（自由変数）に区別されます。自由変数のない論理式は、閉論理式あるいは文と呼ばれ、真偽が定まります。

論理式の真偽

構造

一階述語論理の論理式の解釈は、構造によって与えられます。構造は、議論領域（空でない集合）と、各非論理記号に対する「意味」の割り当てからなります。具体的には、

• - 領域（universe, domain）：`D`
• - 非論理記号を定義域とする関数`F`
• - 述語記号`P`に対して、`F(P)`は`D`上の関係。
• - 関数記号`f`に対して、`F(f)`は`D`上の関数。
• - 定数記号`c`に対して、`F(c)`は`D`の要素。

論理式の充足

構造`M`を与え、変数から`M`の領域への割り当て関数`s`を定めると、各論理式の真偽が定義できます。特に、自由変数を含まない文については、`M`において真か偽かが一意に定まります。

論理的帰結

論理式の集合`Σ`のすべての要素を真にするような構造と割り当て関数の組において、別の論理式`φ`も真になる時、`φ`は`Σ`の論理的帰結であるといいます。また、論理式`φ`が常に真となるとき、`φ`は恒真であるといいます。

形式的証明

論理公理

一階述語論理においても、論理公理と呼ばれる論理式の集合と、推論規則を用いることで形式的な証明を行うことができます。論理公理には、以下のようなものがあります。

• - トートロジー（命題論理におけるトートロジーを拡張したもの）
• - 量化記号に関する公理
• - 等号に関する公理（等号を含む場合）

推論規則

推論規則は、既知の論理式から新しい論理式を導き出すための規則です。ここでは、モーダス・ポーネンス（MP）と全称化（GEN）の2つの規則を用います。

• - モーダス・ポーネンス (MP)：`φ`と`(φ ⇒ ψ)`から`ψ`を導出する規則
• - 全称化 (GEN)：`φ`から`∀x φ`を導出する規則

証明可能性

論理式`φ`が論理式の集合`Σ`から証明可能であるとは、`Σ`の要素と論理公理から推論規則を有限回適用して`φ`が得られることを意味します。

健全性と完全性

• - 健全性: 証明可能な論理式はすべて論理的帰結であること
• - 完全性: 論理的帰結である論理式はすべて証明可能であること

古典一階述語論理は健全かつ完全であることが知られています。

一階述語論理に関する定理

• - コンパクト性定理：文の集合`Σ`のすべての有限部分[[集合]]がモデルを持つならば、`Σ`自身もモデルを持つ。
• - レーヴェンハイム・スコーレムの定理：無限基数`κ`に対して、濃度`κ`の言語における文の集合がモデルを持つなら、濃度`κ`以下のモデルも持つ。
• - 恒真論理式全体の集合は決定可能でない（ゲーデルの不完全性[[定理]]と関連）。

他の論理との比較

一階述語論理は、様々な論理体系の基礎となっています。

• - 型付き一階述語論理：変数や項に型を導入。
• - 弱二階述語論理：有限個の部分[[集合]]の量化を許容。
• - 単項二階述語論理：単項述語の量化を許容。
• - 二階述語論理：すべての述語の量化を許容。
• - 高階述語論理：述語を引数とする述語の量化を許容。
• - 直観主義的一階述語論理：古典論理ではなく直観主義を採用。
• - 様相論理：様相演算子（「～は必然的である」「～は可能である」など）を追加。
• - 無限論理：無限に長い文を許容。
• - 新たな量化子を加えた一階述語論理：新しい量化子を追加。

これらの論理体系の多くは、一階述語論理を拡張したものと見なすことができます。

参考文献

• - D.ヒルベルト、W.アッケルマン 著、伊藤誠（訳） 編『記号論理学の基礎（第３版 ）』大阪教育図書社、1954年。

関連項目

• - 命題論理
• - 二階述語論理
• - 形式的証明
• - 数理[[論理学]]
• - ゲーデルの不完全性[[定理]]

この解説では、一階述語論理の基本的な概念を網羅的に紹介しました。より深く理解するためには、関連文献を参照し、具体的な例を通じて学習を進めることを推奨します。

もう一度検索