V. 述語論理の意味論

述語論理はもともと数学の理論の記述を目的として生まれたもので, どのような数学的内容も記述できることが経験的に知られている. この高い記述能力は数学以外の知識体系にも応用できる可能性を示している. たとえば,計算機プログラミングの基本的形態の一つである「論理プログラミング」 は基本的には述語論理の考え方を応用したものである.計算機科学では 論理プログラミング以外にもさまざまな場面で述語論理やその拡張・変形が 用いられている.

この章では述語論理の意味論を扱う.最初に述語論理の記号化の考え方, 特に述語や量化子など述語論理で新たに登場する概念を説明する. 次に,論理式の構文と解釈の枠組について,より明確な形で定式化する. それに基づいて同値性,恒真性,充足関係など,命題論理でも論じた 意味論的諸概念を論じる.最後に,さまざまな知識体系を述語論理の枠組で 記述する際の基本的な考え方を紹介する.

目次

1. 述語論理は何を記号化したものか
2. 論理式の構文と意味解釈
3. 同値性・恒真性・充足関係
4. 理論とモデル

総目次に戻る


1. 述語論理は何を記号化したものか

1.1 述語論理の特徴

命題論理では「命題」(あるいはその記号化である「命題記号」) が基本的な構成要素であった.命題論理が得意とするのは, 論理回路のように,記述対象が有限個の状態のみをもち, しかもそれらの状態が有限個の命題変数の真理値割り当て(つまりビット列) として表現できる場合である.

命題論理は論理回路などよりも複雑な対象を記述する場合には 力不足である.たとえば,対象が無限に多くの状態をもつか, あるいは,有限個であってもその上限が不定であるような場合を 考えよう.そのような対象を命題論理の枠組で記述しようとすれば, おそらく無限個の命題変数とそれらに関する無限個の論理式を 同時に扱うことが必要になるだろう.これは命題論理の通常の 枠組から逸脱している.さらに,命題論理には対象そのものを 記述する要素が含まれておらず,対象の状態を命題変数でいわば 「間接的に」記述することしかできない(「箱とボール」の パズルを思い出されたい).

命題の代わりに「述語」を基礎にするのが述語論理である. 述語は変項をもち,変項に代入されるものによって真理値が 決まるもので,対象の性質や対象間の関係を表現している. 変項に代入するものを構成するため「変数」・「定数」・ 「函数」・「演算」など(いずれも実体というよりは 単なる記号である)が用意されるが, これらは記述する対象や対象に関する函数・演算などを 表現している.述語論理の論理式はこのような述語から 構成される.以上のようなものによって命題に内部構造 を持ち込むことができる.

さらに,論理記号として新たに「量化子」(「限量子」 ともいう)が導入されることも大きな特徴である. 量化子は記述対象を指す変数(「対象変数」)を 修飾する記号で,すべての対象に対して主張が 成立することを意味する「全称量化子」と, 少なくとも一つの対象に対して主張が成立する ことを意味する「特称量化子」の二種類がある. 対象変数に関するこの種の論理記号はこの二つ以外にも 考えられているが(たとえば,「様相論理」では「様相記号」 と呼ばれるものが新たに導入される), 数学の定理などを定式化する際にはこの二種類の量化子で 十分なことが経験上わかっている.

1.2 述語とは何か

述語の概念には「集合上の n 項関係」の形ですでに出会っているが, これは述語そのものというよりも述語の解釈というべきものである. ここで記号論理に即した形で述語の概念を見直しておくことにしよう.

一般に述語とは変項 t1, ..., tn に応じて真偽(真理値)の定まる主張 P(t1, ..., tn) のことである.変項を n 個含む述語をn 項述語という.

この意味では命題とは「0 項述語」に他ならない.

【注意】

【例】

1.3 箱とボールのパズル再論

命題論理と述語論理の考え方の違いを見るため,「箱とボール」 のパズルを再び採り上げることにしよう.今回は箱として A,B,C,... を用意するだけでなく,ボールにも赤,緑,青の 三色があるとする.話を簡単にするため,各箱にはボールは高々 一つしか入らないとする.

命題論理の場合

このような状況を命題論理で定式化するにはいろいろなやり方が あるが,たとえば,箱ごとに

ARed = 「箱Aに赤色のボールがある」
AGreen = 「箱Aに緑色のボールがある」
ABlue = 「箱Aに青色のボールがある」
という命題変数を用意すればとりあえず記述はできる.

この記述法には,箱ごとに命題変数を用意しなければならない, ボールの属性が増えるにつれて記述が次第に煩雑になる,などの 問題点がある.たとえば,ボールの大きさに大,中,小の三種類があれば

ALarge = 「箱Aのボールは大きい」
AMedium = 「箱Aのボールは中くらい」
ASmall = 「箱Aのボールは小さい」
などという命題変数を箱ごとに導入して組み合わせるか,あるいは
ARedLarge = ARed∧ALarge = 「箱Aに赤色の大ボールがある」
などを原子式として用意することになる.これでは, 命題変数の個数が増えるだけでなく,問題を非常に 不自然な形で表現しているように思える.

述語論理の場合

述語を用いる記述にもいろいろなやり方が考えられるが, 次のように箱やボールの各属性に一つの述語を対応させるのが わかりやすい:

ContainsBall(x) = 「箱 x にはボールがある」
ColorOfBall(x,y) = 「箱 x のボールの色は y である」
SizeOfBall(x,z) = 「箱 x のボールの大きさは z である」
あるいはボールの属性はまとめてしまって
ContainsBall(x) = 「箱 x にはボールがある」
AttribOfBall(x,y,z) = ColorOfBall(x,y)∧SizeOfBall(x,z) = 「箱 x のボールの色は y で大きさは z である」
を用いる考え方もある.もちろん,これら以外の述語の 選び方もあり得るし,述語の解釈にも変更の余地がある. たとえば,ContainsBall(x,y) を使うことはやめて, ColorOfBall(x,y), SizeOfBall(x,z) を「ボールがある」という 意味に用いれば,ColorOfBall(x,Red) ∧ColorOfBall(x,Green) は 「箱 x には赤色のボールと緑色のボールが一つずつある」と解釈 できる.

このような述語を用意しておけば,たとえば 「箱 A には赤色の大ボールがある」という状況は

ContainsBall(A)∧ColorOfBall(A,Red)∧SizeOfBall(A,Large)

あるいは

ContainsBall(A)∧AttribOfBall(A,Red,Large)

と表わされる.なお,この例に示されているように, 論理結合子∧,∨,¬,→,↔は述語論理の場合も 命題論理の場合と同様の構文と意味で用いられる.

このような述語による記述の考え方は,PROLOGなどによる 論理プログラミングの基礎であるのみならず,C言語などで 分岐・繰り返しの条件式を組むときにも必要である. 述語による記述は命題変数による記述よりも自然言語に近く, 論理的な内容が理解しやすい,ということに注意されたい.

1.4 量化子の使い方

すでに触れたように,量化子には全称量化子特称量化子の二種類がある:
演算子使い方意味
全称量化子∀∀x P すべての x に対して P である
特称量化子∃∃x P ある x に対して P である
x は記述対象を指す変数(対象変数), P は x を含む論理式である(x 以外の対象変数を 含んでいても構わない).量化子の修飾を受けている変数を 束縛変数,そうでない変数を自由変数という. 量化子には否定演算子¬と同じ優先順位を与える.

【例】 「x は人間である」を Human(x),「x は死ぬものである」を Mortal(x) で表わすとき,「人は皆死ぬ.そしてソクラテスは 人である.」という文は

(∀x (Human(x) → Mortal(x)))∧ Human(ソクラテス)

と表現される.

【例】 前述の箱と玉のパズルで「各箱にはボールが少なくとも一つ 入っている」という状況は

∀x (IsBox(x) → ContainsBall(x))

と表わされる.ただし IsBox(x) で「x は箱である」という述語を 表わした.「∀x」では x が(箱以外のものも含めて)すべてのもの にわたって走るので,IsBox(x) を省いて

∀x ContainsBall(x)

とするのは正しくない.「IsBox(x) →」を入れることによって, x の走る範囲を実質的に箱だけに限定しているわけである.

同様に,IsColor(x) で「y は色である」という述語と表わせば, 「どの色のボールもどこかの箱に入っている」という状況は

∀y ∃x (IsBox(x)∧IsColor(y) → ContainsBall(x)∧ColorOfBall(x,y))

と表現される.∀y ∃x (...) は ∀y(∃x (...)) の意味で 解釈されるということに注意.∀y と ∃x の順序を入れ替えたもの

∃x ∀y (IsBox(x)∧IsColor(y) → ContainsBall(x)∧ColorOfBall(x,y))

は「ある箱にはすべての色のボールが入っている」という意味になる.

【例】 「函数 f(x) は 点 x = a で連続である」を IsContinuous(f,a) で 表わすと,

IsContinuous(f,a) ↔ ∀ε∃δ∀x (|x - a|<δ → |f(x) - f(a)|<ε)

は連続性の概念を定義する論理式である.なお,ここでは, 論理式の内容を見やすくするため,論理式を通常の数学の 記法に近い形に書き直してある.

なお,全称量化子と特称量化子が否定演算によって

¬(∀x P) ≡ ∃x (¬P),
¬(∃x P) ≡ ∀x (¬P)

と結ばれていることに注意されたい(「≡」は論理的に同値 であることを意味する).

1.5 変数の出現位置と視野

上の例に見るように,曖昧さを避けるためには束縛の及ぶ範囲を 括弧で明示する必要がある.

【例】(∀x P(x))∧Q(x) と ∀x (P(x)∧Q(x)) は意味が異なる:

  1. (∀x P(x))∧Q(x) において∀x が束縛するのは P(x) の中の 変数 x である.(∀x P(x)) は (∀y P(y)) と論理的に同値であるから, 曖昧さを避けるためには (∀y P(y))∧Q(x) と書き直す方がよい. これはさらに ∀y P(y)∧Q(x) に同値変形される.
  2. ∀x (P(x)∧Q(x)) において∀x が束縛するのは P(x), Q(x) の 両方に共通の変数 x である.
【注意】
  1. ∀x P(x) を ∀y P(y) に書き換えることはしばしば定積分に 例えられる.定積分では積分変数は仮のもので,別の変数に 置き換えても意味は変わらない:

    ab dx f(x) = ∫ab dy f(y)

    (ここでは量化記号との対応を見やすくするため,dx, dt を左側に 置く記法を使っている).

  2. 「λ(ラムダ)計算」はチューリング機械と並んで代表的な 計算概念のモデル化で,プログラミング言語LISP(あるいはscheme) の原型でもあるが,そこで用いられる「λ記号」も上と同様な 変数束縛の機能をもつ.λ記号は λx. f (f はλ計算の式) という形で用いられるが,このとき x は束縛変数と呼ばれる. λ記号は平たく言えば函数定義のためのもので,λx. f は 数学で函数を x → f(x) と表わすことに対応している. 函数 x --> f(x) における変数 x は仮の名前で,y --> f(y) と 読み替えても函数の実体は変わらない.そこでλ計算では, λx. f(x) を λy. f(y) に書き換えてもよい,という規則を おくのである(この書き換えを「α変換」あるいは「α同値」 という).

このように,自由変数と束縛変数の違いは変数の名前 (変数記号)では決まらず,論理式の中での出現位置 で決まる.その結果,上の例のように,同じ記号 x を 用いていても,表わすもの自体が異なることさえある. 曖昧さを避けるためにはこのような意味の異なる変数には あらかじめ違う記号を割り当てておく方がよいが,論理式を さらに論理結合子で結ぶときに再び記号の重複が生じ得るので, あらかじめあらゆる変数記号の重複を避けることは不可能である. したがって,必要が生じたときに書き換えるというやり方を とることになる.

∀x や ∃x が変数 x を束縛する範囲をその変数束縛の 作用域あるいは視野という. たとえば (∀x (P(x)∧Q(x))∨R(x) における ∀x の 視野は P(x)∧Q(x) である.なお,「視野」はもともと プログラミング言語を論じるときに用いられる言葉であり, その意味も近い.


2. 論理式の構文と意味解釈

述語論理の論理式の概念はこれまでの説明で概ね明らかに なっているが,函数記号・演算記号などの記号の使い方は まだ明確に説明していない.その点を明確にすることも兼ねて, 改めて論理式の概念を正確に定義しておこう.

そのあとで論理式の意味解釈について説明する.命題論理では 論理式の意味付け(解釈)を命題変数の真理値割り当てによって行ったが, 述語論理の論理式は対象記述のためのさまざまな記号を 含むため,意味解釈ははるかに大掛かりなものとなる.

今までの説明では記号とそれが表わすものをあまり厳密に 区別しなかったが,これからはその区別が必要になる. 論理式は単なる文字列(記号の並び)であり, 「変数記号」・「定数記号」・「函数記号」・「演算記号」・ 「述語記号」などから一定の規則で構成されたものである. この規則(構文規則)は「帰納的定義」の形で 定式化することができる.

2.1 項の帰納的定義

まず「項」の概念を定義する.「項」は最終的に述語に 変項として代入され得るものすべてを指し,普通の数学 でいう「項」とは意味が異なる.たとえば,述語論理を 数学の理論の記述に適用するとき,「項」とは

A*sin(k1*x + w1) + B*cos(k2*x + w2) + C

のように変数記号・定数記号・函数記号・演算記号など からなる通常の数式のことを意味する.

【定義】次のようにして帰納的に定義されるものを という.

  1. 変数記号は項である.
  2. 定数記号は項である.
  3. f が n 項の函数記号・演算記号,t1, ..., tn が項であれば,f(t1, ..., tn) も項である.

【注意】

2.2 論理式の帰納的定義

【定義】次のようにして帰納的に定義されるものを 「論理式」という.
  1. P が n 項述語記号,t1, ..., tn が項であれば,P(t1, ..., tn) は 論理式である.この形の論理式を原子論理式略して 原子式という.
  2. φとψが論理式ならば φ∧ψ, φ∨ψ, ¬φ, φ→ψ, φ↔ψ はそれぞれ論理式である.
  3. φが論理式で x が変数記号ならば,∀xφ, ∃xφ は それぞれ論理式である.

【記法上の注意】

  1. x<y のように中置記法で表わされることが多い述語(関係記号) については,見やすくするため中置記法も許すことにする.
  2. {¬,∀,∃}>{∧, ∨}>{→, ↔} の順に優先順位を 設け,曖昧さが生じるところには括弧をつける.
  3. 複数の量化子 Q1, Q2, ... (それぞれ∀,∃のいずれかをあらわす)が (Q1 x1 (Q2 x2 (...(φ)...) というように現れる論理式は Q1 x1 Q2 x2 ...φ と略記する.
  4. 同じ量化子が ∀x1 ∀x2 ... あるいは ∃x1∃x2 ... というように続くときには ∀x1, x2, ... や ∃x1,x2,... と略記することもある. たとえば ∀x,y ∃z (x<y → x<z ∧ z<y) は ∀x (∀y (∃z (x<y → (x<z ∧ z<y)))) の略記である.
【定義】 論理式に含まれる変数がすべて束縛されているものを 閉論理式という.閉論理式は各記号の意味が 定まれば真偽が確定するので,いわば「完成された文」 である.その意味で,閉論理式のことを と呼ぶこともある.

2.3 意味解釈のための構造

述語論理の論理式には対象記述のための記号 (変数記号,定数記号,函数記号)ならびにそれらからなる 項を変項とする述語記号が含まれている.論理式の意味は これらの記号と具体的な対象との対応付けを与えることに よって定まる.この対応付け(真理値割り当てに M という名前を付けた ように,この対応付けにも M という名前を付けよう) を行うために,ある集合 D(「対象領域」と呼ばれる) とその上の次のような対象を用意する:

記号  対応するもの
定数記号 c  要素 cM ∈ D
函数記号 f  函数 fM: Dn --> D
述語記号 P  述語 PM: Dn --> {T,F}

もう少し正確に述べると次のようになる:

【定義】論理式を構成するのに用意された変数記号・定数記号・ 函数記号・述語記号の集合をそれぞれ Var,Const, Func, Pred と表わし,それらをまとめたものを 記号集合 L = (Var, Const,Func,Pred) と呼ぶことにする.次のようなものからなる集合・対応の組 M = (D,MConst,MFunc,MPred) をL-構造という:

  1. D (対象領域)は集合である.D を Dom(M) とも表わす.
  2. MConst は,各 c ∈ Const に対して, D の要素 cM = MConst[c] を対応させる
  3. MFunc は,各 f ∈ Funct に対して, ある個数(f によって決まる)n の変数をもつ函数 fM = MFunc[f]: Dn --> D を対応させる.
  4. MPred は,各 P ∈ Pred に対して, ある個数(P によって決まる)n の変数をもつ函数 PM = MPred[P]: Dn --> {T,F} を対応させる.

【注意】この定義では対象領域 D は一つしか用意されていないが, 実際の例では対象領域が複数あると考える方が自然な場合が多い. たとえば,数学のでは,自然数,整数,有理数,実数,複素数,など さまざまな基本的集合がある.このような種類の異なる対象領域を許す L-構造の定義も可能であるが,通常は種類を表わす述語を

Natural(x): x は自然数である
Integer(x): x は整数である
Rational(x): x は有理数である
Real(x): x は実数である
Complex(x): x は複素数である
etc...
というように用意して使えば一つの対象領域で事足りる.

2.4 論理式の意味解釈

L-構造 M が一つ与えられれば,変数記号を対象領域上を動く 対象変数と解釈することによって,項と論理式の 解釈が(それらの帰納的定義に基づいて)順次定まる. 最終的に,項は対象領域上の函数に,論理式は 対象領域上の述語(言い替えれば関係)に解釈される. ただし,論理式を {T,F} への函数と解釈するとき 変数として残るのは自由変数のみである.特に, 閉論理式は命題(T, F のいずれかの値をとる) として解釈される
記号列  解釈
n 個の変数を含む項 t 函数 M[t]: Dn --> D
n 個の自由変数を含む論理式 φ 述語 M[φ]: Dn --> {T,F}
閉論理式 φ 命題 M[φ] ∈ {T,F}

厳密には帰納的定義に即して説明すべきであるが, 前章の説明(特に量化子の意味)に照らせば いずれも明らかであろう.

【例その1】

記号集合 L
Const = {zero,one}
Funct = {add,mul}
Pred = {Eq}

L-構造
対象領域 D = N(自然数の集合)
定数記号・函数記号・述語記号の解釈
これは自然数の加法と乗法として解釈する例であるが, その他の数の集合も同様に解釈を与えるし,ブール代数 として解釈する(add ----> ∨,mul ----> ∨)こともできる.

【例その2】

記号集合 L
Const = {A,B,C,Red,Green,Bluel}
Funct = {}
Pred = {Eq, IsBox, IsColor, ColorOfBall}

L-構造
対象領域 D = {a,b,c,red,green,blue}
定数記号・述語記号の解釈

これは箱とボールのパズルを想定した例である. 一群の与えられた論理式(制約条件)をすべて真にするような L-構造を見いだすことがパズルを解くことに他ならない.


3. 同値性・恒真性・充足関係

命題論理の場合にならって,論理式の同値性・恒真性・充足関係 の概念を導入する.閉論理式の場合,これらの概念の取り扱いは 命題論理の場合とほぼ同様であるが,論理式に自由変数が含まれる 場合には注意が必要である.

3.1 自由変数への代入

議論を進める前に,「自由変数への代入」の概念を導入しておく. これは今の議論に限らず広く用いられる.

【定義】x1, ..., xn を論理式φの 自由変数(の一部),t1, ..., tn を任意の項とする.φの中の x1, ..., xn が現れる箇所を x1 --> t1, ..., xn --> tn と置き換えて得られる論理式を φ[t1/x1, ..., tn/xn] と表わす.

【注意】このような場合,φを φ(x1, ..., xn) と表わして, φ[x1/x1, ..., tn/xn] の代わりに φ(t1, ..., tn) と書くこともある,

【例】φ = ∃y (P1(x,y)∧P2(x,y,z)) に対して φ[f(t)/x] = ∃y(P1(f(t),y)∧P2(f(t),y,z)) となる.

3.2 自由変数の値割り当て

命題論理の場合には命題変数に対して真理値の割り当てを考えた. 述語論理の場合にこれに相当するものを二種類考えることになる.

一つはL−構造を与えて定数記号・函数記号・述語記号の意味解釈を 決めることである.これによって論理式の意味は確定する.ただし, 論理式が自由変数 x1, …, xn を含む場合には 論理式を意味解釈したものは対象領域 D 上の述語となるので, その真理値はまだ決まらない.

自由変数が含まれる場合には各自由変数に対象領域の要素 a1, …, an∈D を割り当てること

x1 ----> a1, …, xn ----> an

によって論理式の真理値が最終的に確定する. これを「自由変数の値割り当て」という. これが命題論理の場合の値割り当てに相当する もう一つの概念である.

【定義】このように自由変数に対象領域 D の要素を割り当てることを 自由変数の値割り当てと呼ぶ.L-構造 M と 自由変数の値割り当て v のもとでの論理式 φ の真理値を (M,v)[φ], v[φ]M, などと書くことにする.

3.3 論理式の同値性

意味解釈上まったく同じことを表わす論理式は 「論理的に同値である」という.正確な定義は 次の通りである.

【定義】論理式φとψが すべての L-構造 M と 自由変数のすべての値割り当て v に対して同じ真理値をもつ (すなわち等式 (M,v)[φ] = (M,v)[ψ] が成立する)とき, 論理的に同値であるという.この関係を記号的に φ ≡ ψ と表わす.

【例】命題論理の場合に示した例はすべてそのままの形で 述語論理の論理式についても成り立つ.

  1. 可換律:φ∧ψ ≡ ψ∧φ, φ∨ψ ≡ ψ∨φ
  2. 結合律:(φ∧ψ)∧χ ≡ φ∧(ψ∧χ) , (φ∨ψ)∨χ ≡ φ∨(ψ∨χ)
  3. 分配律:(φ∧ψ)∨χ ≡ (φ∨χ)∧(ψ∨χ), (φ∨ψ)∧χ ≡ (φ∧χ)∨(ψ∧χ)
  4. 吸収律:φ∧(φ∨ψ) ≡ φ, φ∨(φ∧ψ) ≡φ
  5. →の別表現:φ→ψ ≡ (¬φ)∨ψ
  6. ↔の別表現:φ↔ψ ≡ (φ→ψ)∧(ψ→φ)
  7. 二重否定の除去:¬¬φ ≡φ
  8. ド・モルガンの法則:¬(φ∨ψ) ≡ ¬φ∧¬ψ, ¬(φ∧ψ) ≡ ¬φ∨¬ψ
  9. 対偶の法則:φ→ψ ≡ ¬ψ→¬φ

【例】量化子に関して次のような関係が成り立つ:

  1. 束縛変数の取り替え(α同値):x は論理式φの自由変数, y はφに(自由変数としても束縛変数としても)含まれない 変数であるとすると,

  2. 量化子と否定の関係:任意の論理式φに対して

  3. 量化子と連言・選言との関係: φ,ψを任意の論理式とすると

    さらに,φが x を自由変数として含まないならば

いずれも容易に確かめられる.

【練習問題】次のことを示せ.

  1. (∀x φ)∨(∀x ψ)と∀x(φ∨ψ) は論理的に同値ではない.
  2. (∃x φ)∧(∃x ψ)と∃x(φ∧ψ) は論理的に同値ではない.

これらの関係を利用して論理式の「同値変形」を考える ことができる.命題論理の場合には任意の論理式を 連言標準形・選言標準形に同値変形できたことを思い出そう. 述語論理の場合,量化子が存在することが命題論理との 大きな違いであるが,上に示した公式を利用すれば, 任意の論理式を「冠頭標準形」と呼ばれる形に同値変形できる (ただし一意的ではない). 冠頭標準形とは量化子を先頭に集めた形をいう:

【定義】一群の量化子Q1, ..., Qm (それぞれ∀,∃のいずれかをあらわす)と量化子を含まない論理式ψ によって

Q1x1 ... Qmxmψ

の形に表わされるものを冠頭標準形の論理式という.

【例】∃y ψ(x,y)∧¬∃z φ(y,z) は次のようにして冠頭標準形に同値変形する ことができる(y が出現位置によって異なる意味をもつので要注意):

∃y ψ(x,y)∧¬∃z φ(y,z)
∃y ψ(x,y)∧∀z ¬φ(y,z) (¬∃を∀¬に書き換える)
∀z (∃y ψ(x,y)∧¬φ(y,z)) (∀z を外に出す)
∀z (∃w ψ(x,w)∧¬φ(y,z)) (∃y を ∃w にα変換する)
∀z ∃w (ψ(x,w)∧¬φ(y,z)) (∃w を外に出す)

【練習問題】次のそれぞれを冠頭標準形へ同値変形せよ.

  1. (∀x P(x)∧Q(y))→∀y P(y)
  2. ∀x P(x,y) → ∃y(¬∃y Q(z) ∨ R(y))
  3. ∀x(∃y(P(y)→Q(x,z))∧∀z(Q(x,z)∨¬∀w R(z,w)))

【注意】「原子式」を述語論理の意味での原子式(すなわち述語記号 に任意の項を代入したもの)と解釈すれば,冠頭標準形の量化子を 含まない部分ψは連言あるいは選言標準形に同値変形できる. さらに,ここでは詳しい説明を省くが,充足問題(モデルの存在) を論じる場合には,新たな定数記号(スコーレム定数) や函数記号(スコーレム函数)を導入して, ∃を消去することもできる(これは同値変形ではない). たとえば

∃w ∀x ∀y ∃z P(w,x,y,z)

という論理式に対しては定数記号 c と函数記号 f を新たに導入して

∀x ∀y P(c,x,y, f(x,y))

という論理式を対応させれば∃を消去した論理式が得られる. この c,f がそれぞれスコーレム定数とスコーレム函数である. これとは解釈が異なるが,同様の手順で∀を消去することも行われる. このような書き換えは計算機による論理プログラミングや定理証明の際に 必要になる.また,述語論理や数学基礎論の理論面でも重要な技法である.

3.4 論理式の恒真性・恒偽性

論理式の「恒真性」あるいは「恒偽性」も同様である.

【定義】論理式φがすべての L-構造 Mと 自由変数のすべての値割り当て vに対して真の値をとる (すわなち等式 (M,v)[φ] = T が成立する)とき φは恒真式であるという.この関係を記号的に |= φ と表わす.¬φ が恒真式であるときφは 恒偽式であるという.

【注意】

【例】命題論理の恒真式をそのまま述語論理に焼き直すこともできる. たとえば

  1. 排中律: |= φ∨¬φ
  2. 矛盾律:|= ¬(φ∧¬φ)
  3. modus ponens:|= (φ∧(φ→ψ))→ψ
  4. modus tollens:|= (¬ψ∧(φ→ψ))→¬φ
  5. 選言三段論法:|= (¬φ∧(φ∨ψ))→ψ
  6. 仮言三段論法:|= ((φ→ψ)∧(ψ→χ))→(φ→χ)

【例】次の例は量化子に関するもので,いくつかを除けば, すでに示した同値な式の例の言い替えである.

  1. 束縛変数の取り替え:x は論理式φの自由変数, y はφに(自由変数としても束縛変数としても)含まれない 変数であるとすると,

  2. 量化子と否定の関係:任意の論理式φに対して

  3. 量化子と連言・選言との関係: φ, ψを任意の論理式とすると,

    さらに φが x を自由変数として含まなければ

【練習問題】次のことを確かめよ.

  1. (∀x φ)∨(∀x ψ)→∀x(φ∨ψ) および ∃x(φ∧ψ)→(∃x φ)∧(∃x ψ) は恒真である.
  2. ∀x(φ∨ψ)→(∀x φ)∨(∀x ψ)および (∃x φ)∧(∃x ψ)→∃x(φ∧ψ)は恒真ではない.

3.5 L-構造と論理式の充足関係

【定義】論理式φが L-構造 M による解釈のもとで 自由変数の任意の値割り当てに対して真であるとき M はφを充足すると言う.この関係 を記号的にM |= φと表わす.

【注意】φ に含まれる自由変数が x1, ..., xn であれば,M |= φと M |= ∀x1,x2,...,xnφ は同じことである.この意味で充足関係を閉論理式に限って 考える流儀もある.

【例】 1.4 節の例のような L-構造を考える(ColorOfBallの解釈が未定).

φ = ∀x ∀y ∀z ∀w (IsBox(x)∧IsBox(y)∧IsColor(z)∧IsColor(w)∧ ColorOfBox(x,z)∧ColorOfBox(y,w)∧(¬Eq(x,y)→¬Eq(z,w)))
という論理式φを考える.普通の文で言えば,これは要するに 「箱が違えば入っているボールの色は違う」という条件である. M がこれを充足するような M[ColorOfBall] の決め方には, 次に示す例を初めとして全部で6通りある(問:残りの5つを求めよ). ただしこの表は M[ColorOfBall](x,y) を2次元に配列したものである.

箱\色redgreenblue
aTFF
bFTF
cFFT
φ を充足する例


4. 理論とモデル

ここまでの議論ではどのような場合にも成立する一般的な法則を扱ってきた. これらが論理法則として基本的であることは言うまでもない.だが, どのような場合にも通用する法則は,特定の事実や知識について語らない, という意味では無内容でもある.述語論理はもともと 数学の諸理論の記述を目的として生まれた記号論理の体系であり, その本領はさまざまな知識体系の記述の問題にある. この節では述語論理のそのような側面を簡単に紹介する.

4.1 理論とモデル

【定義】一般に閉論理式からなる集合Tを 理論という.L-構造 M がTに属する任意の論理式 φを充足する(すなわち M |=φ となる)とき, M はTのモデルであると言う. この関係を記号的に M |=T と表わす.

【注意】

「理論」という言葉は数学のさまざまな理論(たとえば自然数論) に由来する.記号論理で数学の「理論」というときには, 「公理」や「定義」などの集まり(いわば理論の基本的設定) を意味する場合と,そこから導かれる「定理」を含めたもの (いわば知識の集積としての理論)を考える場合がある.

逆に,L-構造を与えてそれが充足する閉論理式の集合を 考えることもできる:

【定義】L-構造 M に対して

T(M) = { φ | φは L の閉論理式で M |= φ が成立する }

M の定める理論という.

この T(M) は M において成立する事実をすべてを集めたものである. 数学の場合には,公理や定義だけでなく定理も含まれていることになる.

4.2 公理と定理

4.2.1 公理の例

数学において議論の出発点として証明なしに認める主張のことを 公理という.数学において一つの理論を論理的に構成するには 議論の出発点としていくつかの公理を公理系として用意し, そこから証明によってさまざまな定理を導き出す.よく知られた公理系には 初等幾何学における公理系(「ユークリッド幾何学」の公理系)があるが, その定式化は大掛かりになるので,以下ではもっと簡単な公理系の例をいくつか示す.

【例1】自然数論では

  1. ∀x¬ (S(x) = 0)
  2. ∀x∀y (S(x) = S(y) → x = y)
  3. ∀x (x + 0 = x)
  4. ∀x∀y (x + S(y) = S(x + y))
  5. ∀x (x * 0 = 0)
  6. ∀x∀y (x * S(y)) = x * y + x)
  7. ∀x ¬(x < 0)
  8. ∀x∀y (x < S(y) ↔ x < y ∨ x = y)
  9. φ[0 / x]∧∀x(φ→φ[S(x) / x]) → ∀xφ (φは任意の論理式)
という公理系を選ぶことが多い.これはペアノが考えた公理系 (ペアノの公理系)に演算 +, * と順序 < の公理を付け加えたもので 「ペアノ算術」の公理系と呼ばれる.ここで 0 は定数記号,S, +, * は 函数記号,=, < は述語記号である.S は「後者函数」と呼ばれるもので, 意味上は S(x) = x + 1 と解釈される.また,+,* はもちろん加法演算と 乗法演算である.なお,正確に言えば,これらの公理に現れる等号「=」 に関しては次のような「等号公理」を別途設定しておく必要がある.

【例2】述語記号としての等号 = (これは自然数など記述対象の等号であり, 論理式の等号などと混同してはならない)も次のような公理系(等号公理) によって特徴づけられる:

  1. ∀x (x = x)
  2. ∀x∀y (x = y → y = x)
  3. n 個の自由変数 x1, …, xn を もつ任意の項 t(x1,…,xn) に対して ∀x1…∀xn∀y1…∀yn (x1=y1∧…∧xn=yn → t(x1,…,xn) = t(y1,…,yn) )
  4. n 個の自由変数 x1, …, xn を もつ任意の論理式φ(x1,…,xn) に対して ∀x1…∀xn∀y1…∀yn (x1=y1∧…∧tn=yn →(P(x1,…,xn)↔ P(y1,…,yn)) )
最初の二つの公理は反射律と対称律であり, 残りの二つは関数や述語への代入についての性質である. 推移律 ∀x∀y∀z (x = y ∧ y = z → x = z) はこれらを 組み合わせると導出できる(述語への代入の公理から, x = y のもとで x = z ↔ y = z が成立することによる).

【例3】数学における「定義」も記号論理的には公理(正確には, 既存の公理系に新たに付け加える公理)である.それは定義対象 (函数,関係など)の基本的な性質を述べた論理式からなる. たとえば,普通の数学(自然数論,初等整数論,など)では 「x は y を割り切る」という関係 x | y を

x | y ↔ ∃z (x*z = y)

というように定義するが,述語論理の立場ではこの関係記号 | を 記号系 L に加えた上で

∀x ∀y (x | y ↔ ∃z (x*z = y))

という論理式を公理系に加える. 函数の定義の取り扱いはもう少し複雑になるが (スコーレム函数の取り扱いに準じて考えればよい), 定義を閉論理式の形に書いて公理系に加えるという点では同様である.

4.2.2 定理の導出

数学の理論を考える場合,定理も含めた理論全体を最初から与えることは あまり意味がない.通常は少数の「公理」からなる集合 T0 をまず与えて,そこから証明によって論理的帰結を導き出す. そのようにして導出される帰結が「定理」であり,公理と定理の全体が 一つの理論 T (すなわち数学的知識の一つの体系)を構成する.

意味論的に考えれば,T0からの論理的帰結とは, T0の任意のモデル M に対して成立する主張 (閉論理式)である.そのような閉論理式φを T0の「意味論的帰結」と呼ぶ:

【定義】T0 の任意のモデル M がφを満たす(M |=φ が成立する)とき φを T0意味論的帰結と呼び, T0 とφのこの関係を T0|=φ と表わす.

数学で定理を証明するときには,公理や仮定を満たす対象(すなわちモデル) を任意に選んでそれが結論を満たすことを示すことが多い. これは上の意味での意味論的証明に他ならない.

ところで,そのような数学の証明における推論をよく反省してみれば, その骨格は実は場合分け・三段論法・消去法・背理法などごく少数の 基本的な推論の形式を繰り返しているに過ぎないことがわかる.しかも, 数学的帰納法のように扱っている対象(自然数など)と密接に関連するものは 別として,それらの基本的な推論パターンの多くは扱っているモデルとは 独立である(言い換えればどのようなモデルにも当てはまる). そのような基本的な推論パターンを抽出したものを推論規則と言う (これもまた恒真式や同値性とは別の意味で「論理法則」と呼ぶべきものである). これらの一般的な推論規則が十分に解明されれば,今度はそれを「機械的に」 適用することによってさまざまな証明が誤りなく遂行できると期待される. ちなみに,このような考え方自体は記号論理学の出現以前から存在した (よく知られた例としてアリストテレスによる三段論法の分類がある).

次章以降で解説する「論理の形式化」はこのような「機械的な証明」 の考え方を記号的に定式化したものである.そこでは推論規則を 論理式の「変形規則」として用意し,公理として用意された論理式や すでに定理として導出した論理式に対してそれを適用して 新たな定理の証明を行う.一般に, 閉論理式φが公理系 T0 からそのような形式的証明 によって導出できることを T0|-φ と表わす.

このような形式化証明と意味論的証明が同等の能力を有する (すなわちT0|-φ と T0|=φ が同値になる) かどうかはもちろん形式化の仕方に依存する.1階述語論理の場合には, どのような理論 T に対しても T|-φ と T|=φ が同値になるような形式化 (「完全な形式化」と言う)が知られている.


キーワード

述語,量化子(全称・特称),対象変数,束縛変数,自由変数, 出現位置,作用域,視野,変数記号,定数記号,函数記号, 演算記号,述語記号,項,原子式,論理式,閉論理式,文, 記号集合,対象領域,L-構造,解釈,自由変数への代入, (自由変数の)値割り当て,論理的に同値,冠頭標準形, スコーレム定数・関数,恒真式,恒偽式,充足関係,理論,モデル, 公理,定義,意味論的帰結・証明,推論規則,形式的証明