一階述語論理

出典: フリー百科事典『ウィキペディア（Wikipedia）』

一階述語論理（いっかいじゅつごろんり、first-order predicate logic）あるいは述語論理 (predicate logic) は、数理論理学の体系のひとつであり、命題論理を拡張したものである。述語 (predicate) が変項化されないものを一階述語論理と呼び、述語を変項化したものを二階述語論理（さらに一般化して高階述語論理）と呼ぶ。本項では主に一階述語論理までについて解説する。

一階述語論理の原子式は P(t₁, ..., t_n) という形式であり、これは一つ以上の主語 (subject) を持つ述語とみなすことができる。一方、命題論理では原子式は単に命題としてひとつの記号で表されていた。以下に書かれるように、P(t₁, ..., t_n) の括弧やカンマは省いて表記されることが多い。

命題論理にない一階述語論理の特徴は量化 (quantification) である。φ を任意の論理式としたとき、∀xφ と ∃xφ が新たに導入される。前者は「すべての x について φ である」という意味であり、後者は「ある x が存在し、φ である」という意味である。意図を明確にするために φ を φ(x) と書き、φ(x) 中の x の自由な出現すべてを a で置換した結果を φ(a) で示すものとする。すると ∀xφ(x) は φ(a) が任意の a について真であることを意味し、∃xφ(x) は φ(a) が真となるような a が少なくともひとつ存在することを意味する。変項の値は既知の対象領域から選ばれる。一階述語論理を改良することによって、対象領域を種 (sort) ごとに分割し、それぞれの領域上を動く種別の変項を導入することもできる（詳しくは多種論理を参照せよ）。

二階述語論理（およびそれ以上の高階述語論理）では、述語記号に対して量化子を導入する。例えば、同一性 (equality) は二階述語論理において、x = y ≡_def ∀P(P(x) ↔ P(y)) と定義できる。述語に対する量化は一階述語論理では許されない。

一階述語論理は、数学のほぼ全領域を形式化するのに十分な表現力を持っている。一階述語論理は一般に、有限あるいは再帰的に枚挙可能な公理集合および、そこから導出可能な式から成る。通常使われている集合論の公理系ZFCは一階理論の例であり、古典数学の全体はZFCで形式化できると一般にみなされている。この他にペアノ算術のように、通常、一階述語論理単独で形式化される理論もある（ただし、それらはもちろん集合論内で形式化することもできる）。

[編集] 一階述語論理の定義

述語論理は以下の要素から構成される。

形成規則（整論理式を形成するための再帰的定義）
変形規則（定理を導出するための推論規則）
公理または公理図式の（可算無限な）集合

ここでいう公理とは「論理」公理であり、述語計算の一部である。さらに個々の一階理論には「非論理」公理が追加される。それらは論理的に真であるとはみなされないが、その理論体系内では真とみなされる。

公理の集合が無限の場合、任意の整論理式が公理か否かを判定するアルゴリズムが存在しなければならない。さらに言えば、推論規則の各々の適用が正しいものか否かを判定するアルゴリズムも存在すべきである。

述語論理の表現方法はひとつに限定されない。ここで用いる公理や推論規則は必ずしも規範的な例ではなく、同一の論理を別の形式で表現することも可能である（その場合、与えられた公理から同じ定理が導出される）。

[編集] 語彙

個体定項の集合。一般に次のような小文字 a, b, c, ... で表される。
個体変項の無限集合。一般に次のような小文字 x, y, z, ... で表される。
関数記号の集合。各々1以上のアリティー（引数の数）を持つ。一般に次のような小文字 f, g, h, ... で表される。
述語記号の集合。各々1以上のアリティーを持つ。一般に次のような大文字 P, Q, R, ... で表される。
論理演算記号： ¬（否定）、∧（論理積）、∨（論理和）、→（含意）、↔（同値）
量化子記号： ∀（全称記号）、∃（存在記号）
左右の括弧： (, )
等号 = は、場合によっては語彙に含まれる（常に含まれるわけではない）。

細かいバリエーションとして、以下のようなものがある。

いくつかの記号は原始要素ではなく、省略記法とみなされる場合がある。例えば、(P ↔ Q) は (P → Q) ∧ (Q → P) を略記したものとみなすこともできる（つまり同じ意味である)。最低限必要な記号は三種類（NOR や NAND を定義するなら二種類）であり、例えば ¬、∧、∀ で十分である。
古い本などでは、φ → ψ を φ ⊃ ψ と表記し、∀xφ を Πxφ と表記している場合がある。
同一性関係を一階述語論理の一部とみなす場合もある。その場合、等号も含まれることになる。これを「等号付き一階述語論理」と呼ぶ。
個体定項はアリティー0の関数と同一視できる。そのため、個体定項を無くして、関数が任意（0を含む）のアリティーを持てるように定式化することもできる。しかし、一般に関数が必ず1以上のアリティーを持つとした方が便利である。
上の定義では、述語は少なくとも1以上のアリティーを持つとされている。アリティー0の述語も考えることができ、それらは「真」や「偽」を意味するものと考えることができる。しかし「真」は ∀x(x = x) などと別の方法で表せるので、アリティー0の述語を導入することに大きな意味はない。
括弧の使い方の流儀は様々である。ある人は ∀x を (∀x) と書く。括弧の代わりにコロンや終止符を使う場合もある。非常に珍しい表記法として括弧を全く使わずにポーランド記法を使用する場合がある。これは、∧ や ∨ を先頭に書いて引数を後に続ける書き方である。ポーランド記法はコンパクトで美しいのだが、可読性が低いためにほとんど使われない。
技術的には、アリティー2の関数が順序対を表している場合（あるいはアリティー2の述語が順序対の射影関係を表現している場合）、アリティー3以上の関数や述語を省くことができる。もちろん、その順序対や射影は自然な公理を満足するものでなければならない。

個体定項の集合、関数の集合、述語の集合は一般に言語を構成するが、変項や論理演算子や量化子は論理そのものに属する。例えば群論の言語では、ひとつの個体定項（単位元）、アリティー1のひとつの関数（逆元関数）、アリティー2のひとつの関数（積関数）、アリティー2の関係（同一性関係）から構成される（ただし、等号付き一階述語論理で定式化する場合には、同一性関係は省略できる）。

[編集] 形成規則

形成規則は項、論理式、およびそれらに含まれる自由変項を以下のように定義する。

項 (term) の集合は次の規則から帰納的に定義される。

個体定項は（自由変項を持たない）項である。
個体変項は項である（その唯一の自由変項は自分自身である）。
t₁ , ..., t_n が項であるとき、アリティー n ≥ 1 の関数 f を用いて作られる式 f(t₁, ..., t_n) は項である。このとき、t₁, ..., t_n それぞれの自由変項が、f(t₁, ..., t_n) の自由変項となる。
閉包節： 上記以外は項ではない。

整論理式 (well-formed formula, 通常 wff と略され、単に「論理式」とも呼ばれる) の集合は、次の規則によって帰納的に定義される。

単純な述語と複雑な述語： a_i が項であり、P をアリティーn ≥ 1 の述語記号とするとき、Pa₁ , ..., a_n は整論理式である。a_i のいずれかが自由変項を持つなら、それが Pa₁ , ..., a_n の自由変項となる。等号が論理の一部となっている場合、(a₁ = a₂) は整論理式である。これらはいずれも原子 (atomic) 式と呼ばれる。
帰納節 I： φ が整論理式なら ¬φ も整論理式である。
帰納節 II： φ と ψ が整論理式なら (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) は全て整論理式である。
帰納節 III： φ が整論理式なら、∀xφ と ∃xφ は論理式である（ここで x は任意の個体変項）。φ に含まれる x 以外の自由変項がこれらの式の自由変項である。∀xφ と ∃xφ において、x は自由ではなく「束縛されている」といわれる。
閉包節 上記以外は論理式ではない。

実際には、P がアリティー2の述語である場合に、これを「P a b」ではなく「a P b」と表記することがある。例えば、<1 2 ではなく 1 < 2 のように書く。同様に f がアリティー2の関数である場合、これを「f(a b)」ではなく「a f b」と表記することがある。例えば、+(1 2) ではなく 1 + 2 と書く。また、曖昧さが発生しない限り括弧を省略することも一般的である。

代入： t を項、 φ(x) を（xを自由変項として含む）論理式とする。このとき φ(t) は、φ(x) 中の x の自由な出現すべてを t で置き換えたものと定義される。ただしここで、t に含まれるいかなる自由変項も、この置き換えによって束縛されてしまうことがないようにしなければならない。もし t の自由変項が束縛されるなら、x を t で置換する前に φ 内の束縛変項名を t 内の自由変項名以外のものに変更しなければならない。この条件が必要となる理由を説明するために、以下のような場合を考えてみよう。論理式 φ(x) の中身が ∀y y ≤ x（これは「x は最大値」を意味する）だとする。t が y を自由変項として持たない項であれば、φ(t) はまさに t が最大値であると主張していることになる。しかし、もし t が y である場合、φ(t) は ∀y y ≤ y となり、主張することが変わってしまう。この問題は、自由変項 x に y を代入したときに、φ(x) の中で t の自由変項 y が束縛されてしまうために発生する。そこで、事前に束縛変項 y を他の名前、例えば z に変えて、∀z z ≤ y とすることで問題を回避する。これを忘れるとひどい間違いを犯すことになる。

例：アーベル群の言語は個体定項 0, 単項関数 −, 二項関数 +, 二項述語 ≤ から構成される。ここで、

0, x, y は原子項である。
+(x, y), +(x + (y −(z))) は項であり、通常 x + y, x + (y + −z) と書かれる。
+(x, y) = 0, ≤ +(x +(y −(z))) +(x, y) は原子式であり、通常 x + y = 0, x + y − z ≤ x + y と書かれる。
(∀x ∃y ≤ +(x y) z ∧ ∃x +(x, y) = 0) は論理式であり、通常 (∀x ∃y x + y ≤ z) ∧ (∃x x + y = 0) と書かれる。

[編集] 同一性

一階述語論理での同一性に関する規約には様々なものがあるが、ここではそのうち主なものを要約する。どの規約に従っても同じ結果が（ほぼ同じ手数で）得られ、違うのは主に用語法だけである。

最も一般的な規約は、等号を原始論理記号に含め、同一性の公理を一階述語論理の公理に追加するというものである。同一性の公理とは、次のものをいう。

x = x
任意の関数 f について、x = y → f(..., x, ...) = f(..., y, ...)
任意の述語 P について、x = y → (P(..., x, ...) → P(..., y, ...))

次に一般的な規約は、等号を理論の関係のひとつとして含め、同一性の公理を理論の公理に付け加えるものである。実際には、理論が同一性概念を持っていない特殊なケースを除けば、この規約を上の規約と区別するのはほとんど不可能である。全体として公理は同じであり、単にそれを論理の公理と呼ぶか理論の公理と呼ぶかの違いだけとなる。
関数を持たず、有限個の関係しか持たない理論では、ふたつの項 s と t について、s と t を入れ替えてもいかなる関係も変化しないこととして、関係を使って同一性を定義することができる。例えば、一種類の関係記号 ∈ を持つ集合論では、s = t は ∀x(s ∈ x ↔ t ∈ x) ∧ ∀x(x ∈ s ↔ x ∈ t) の略記法として定義できる。この同一性の定義は、同一性の公理を自動的に満足する。
理論によっては同一性にその場限りの定義を与えることもある。例えば一種類の述語 ≤ を持つ半順序の理論では、s = t を s ≤ t ∧ t ≤ s の言い換えであると定義できる。
「P(x) は唯一の x について成り立つ」ということを論じるのは時に有用である。このことは次のように表現できる。

∃x(P(x) ∧ ∀y(P(y) → (x = y)))

これは一般に、∃!xP(x) と略記される。

[編集] 推論規則

ここでの定式化で用いられる命題論理の推論規則は、モーダス・ポネンスのみである。これは、φ と φ → ψ がともに証明されていれば、ψ を導いてよいというものである。

汎化と呼ばれる推論規則は述語論理に特有のものである。これは、以下のように定義される。

├ φ ならば ├ ∀xφ

ここで φ は証明済みの定理である。

汎化は様相論理の必然化規則と似ている点に注意されたい。

├ P ならば ├ □P

[編集] 量化子の公理

以下の4つの論理公理が述語計算を特徴付けている。

PRED-1: ∀xZ(x) → Z(y)
PRED-2: Z(y) → ∃xZ(x)
PRED-3: ∀x(W → Z(x)) → (W → ∀xZ(x))
PRED-4: ∀x(Z(x) → W) → (∃xZ(x) → W)

これらは実際には公理図式である。ここで、表現 W は任意の整論理式であり、x は自由変項ではない。また、表現 Z(x) は任意の整論理式であり、Z(y) は同じ論理式中の x の自由な出現を全て y で置換したものを表す。

[編集] 述語計算

述語計算は命題計算を拡張したもので、一階述語論理のどの文が証明可能なのかを定義するものである。命題計算が適当な公理系と唯一の推論規則（モーダス・ポネンス）で定義されているとき（これには様々なやり方がある）、述語計算はそれにいくつかの公理と汎化の推論規則を追加することで定義される。より正確にいえば、述語計算で採用される公理は以下のものである。

命題論理の全ての恒真文（命題変項は論理式に置き換える）
量化子についての上述の公理
同一性についての上述の公理（同一性を論理に含める場合）

ある文が一階述語論理で証明可能と言えるのは、述語計算の公理系から始めて推論規則（モーダス・ポネンスと汎化）を繰り返し適用して、その文が得られる場合である。

理論 T（公理と呼ばれる文の集合）が与えられたとき、文 φ が理論 T 内で証明可能であるとは、a ∧ b ∧ ... → φ（ただしここで、a, b, ... は理論 T の有限個の公理とする）が一階述語論理で証明可能であることとして定義される。

この証明可能性の定義が持つ明らかな問題点は、それが場当たり的に見えることである。つまり、証明に使用する公理や推論規則はなんとなく選んでいるため、本来必要な公理あるいは推論規則を見逃しているかもしれないのである。ゲーデルの完全性定理は、実際にはそのような心配は無用であることを保証する。それによれば、任意のモデルで真である文はすべて一階述語論理で証明可能である。一階述語論理における「証明可能性」のいかなる適法な定義も、上述の定義と等価なものでなければならない（ただし証明可能性の定義の仕方によって、証明の長さが大きく異なることはありうるが）。

証明可能性については様々な異なる（しかし互いに等価な）定義の方法がある。上述の定義はヒルベルト流計算の典型例であり、これは異なる公理を多数用意して推論規則を少なくするスタイルをとっている。ゲンツェン流の述語計算では逆に、公理を少なくして推論規則を豊富に用意している。

[編集] 一階述語論理のメタ論理的定理

以下、重要なメタ論理的定理を列挙する。

命題計算とは異なり、一階述語論理は（高々アリティー2の述語が一つでも含まれていると）決定不能である。つまり、任意の論理式 P について、P が恒真であるか否かを決定する一般的なアルゴリズムは存在しない（チューリングマシンの停止問題を参照せよ）。この結果はアロンゾ・チャーチとアラン・チューリングがそれぞれ独立に導き出した。
ただし、与えられた文（論理式）が恒真であるとき、かつそのときにのみ停止するチューリングマシンは存在する。逆に恒真でない論理式の場合は判定が停止しないかもしれない。これを「部分決定性がある」という。
単項述語論理（単項の述語だけからなる述語論理）は決定可能である。

[編集] 他の論理との比較

型つき一階述語論理は変項や項に型または種を導入したものである。型の個数が有限個であれば普通の一階述語論理と大きな違いはなく、有限個の単項述語で型を記述し、いくつかの公理を追加すればよい。真理値として Ω という特殊な型を持つ場合があるが、その場合の論理式は Ω 型の項となる。
弱二階述語論理は有限個の部分集合の量化を許すものである。
単項二階述語論理は部分集合、すなわち単項述語の量化のみを許すものである。
二階述語論理は部分集合および関係、すなわち全ての述語の量化を許すものである。
高階述語論理は述語を引数とする述語など、さらに一般化したものの量化を許す。
直観主義的一階述語論理は古典命題計算ではなく直観主義を導入するものである。例えば、¬¬φ は必ずしも φ と等しいとは限らない。
様相論理は様相演算子を追加したものである。これは、直観的に説明すれば、「～は必然的である」および「～は可能である」を意味する演算子である。
無限論理は無限に長い文を許す。例えば無限個の論理式の連言や選言が許されたり、無限個の変項を量化できたりする。
新たな量化子を加えた一階述語論理は、例えば「……であるような多くの x が存在する」といった意味の新たな量化子 Qx, ..., を持つ。

こうした論理の多くは、一階述語論理の何らかの拡張と言える。これらは、一階述語論理の論理演算子と量化子を全て含んでいて、それらの意味も同じである。リンドストレムは、一階述語論理の拡張には、レーヴェンハイム＝スコーレムの下降定理とコンパクト性定理の両方を満足するものが存在しないことを示した。この定理の内容を精確に述べるには、論理が満たしていなければならない条件を数ページにわたって列挙する必要がある。例えば、言語の記号を変更しても各文の真偽が基本的に変わらないようになっていなければならない。

一階述語論理のいくぶんエキゾチックな等価物には、次のものがある。順序対構成をもつ一階述語論理は、特別な関係として順序対の射影を持つ関係代数（これはタルスキと Givant によって構築された）と精確に等価である。