Langphilia! / Study / Logic in Computer Science

計算機科学における論理学

{Michael Huth, Mark Ryan}, Logic in Computer Science: Modelling and Reasoning about Systems, 2000. www.cs.bham.ac.uk/research/lics/

このページは、上記の本の一部をてきとーに日本語意訳したものです。原文の著作権は、原著者にあります。このページの著作権は私にあります。翻訳許可をもらってないので、引用とかしない方が無難でしょう。

2.4 述語論理の意味論

命題論理の自然な演繹［証明］を述語論理に拡大適用する方法［2.3節］が分かったところで、述語論理の意味論の仕組みを見てみよう。命題論理と同様に、論理の、異なるが結局は等価な性質を、意味論は与えるべきだ。

「異なる」とは、演算子の意味を異なる方法で定義するという意味だ。証明論においては、証明規則を 操作的に 記述することによって演算子の意味を定義した。意味論においては、真理値表のようなものが欲しい。
「等価」とは、健全性と完全性とを証明できるべきだという意味だ。命題論理では証明できた。（もっとも、述語論理の健全性と完全性とを全く新しく証明するのは、この本の範囲を超えている。）

	簡単	難しい
証明論	Γ \|- φ	Γ \|/- φ
意味論	Γ \|/= φ	Γ \|= φ

述語論理の意味論の説明を始める前に、意味と証明とが本当に違うのをもっと良く見ておこう。証明論において、基本的に組み立てるものは証明だ。 Γ と書いて、論理式のリスト φ₁, .., φ_n を表すことにしよう。

Γ |- φ を示すには、 Γ から φ を証明する必要がある。
しかし、φ が Γ の帰結でないことはどう示せるか？直観的に、これは難しい。あることの 証明がない ことをどう示せるか？全ての証明「候補」を考えて、それが証明でないことを示さなければならない。

証明論は論理の「正の」性質を与える。証明論は Γ |- φ のような言明に根拠を与えるが、 Γ |/- φ を示すにはそれほど役に立たない。

一方、意味論の働きは逆向きだ。

φ が Γ の帰結でないことを示すのは簡単だ。 Γ のモデルであって φ のモデルでない例を挙げるだけで良い。
一方、φ が Γ の帰結であることを示すのは原理的に難しい。命題論理では、Γ を真にするような valuation （関連アトムに対する真理値代入）が φ も真にすることを示す必要があった。 valuation が少数なら、問題ではない。しかし、述語論理では、無限個のモデルが考えられる。（命題論理における valuation に対応する概念をモデルと呼ぶ。）

意味論では、論理の「負の」性質を与える。 Γ |/= φ（φ は Γ における全ての論理式の論理的帰結でない）という形の言明を示すのは、 Γ |= φ（φ は Γ の論理的帰結）を示すのよりも簡単なことが分かる。なぜなら、前者は1つのモデルについて言うだけで良いのに、後者は無限個のモデルについて言わなければならないからだ。

この話で分かるが、証明論と意味論との両方を学ぶことが重要だ。例えば、φ が Γ の帰結でないことを示そうとして苦戦していたら、 Γ |- φ を証明するように作戦を変えると良い。証明できれば、φ は Γ の帰結であることが分かる。証明できない場合、証明しようとしている間に反例を組み立てる直感が湧くだろう。証明論と意味論とが等価であることは驚きだが、事実、証明論と意味論とは論理において異なる役割を持ち、一緒に学ぶのが役に立つ。

2.4.1 モデル

命題論理における論理式の評価方法を思い出そう。例えば、命題論理式
(p ∨ ￢q) → (q → p)
を評価するとは、与えられた valuation （p と q の真偽値）から論理式の真偽値 (T or F) を計算することだった。この行為は本質的には、 (p ∨ ￢q) → (q → p) の真偽値表のうち 1行を作ることになる。
述語論理における論理式の評価方法はどうか？上の論理式を変えてみよう。
∀x ∃y ((P(x) ∨ ￢Q(y)) → (Q(x) → P(y)))
単純に P(x), Q(y), Q(x), P(y) の真偽値を決め、論理式の真偽値を計算できるだろうか？否、限量子 ∀x と ∃y の意味、 依存性［スコープ］および、P と Q の実引数を反映しなければならない。論理式 ∀x ∃y R(x, y) は一般に ∃y ∀x R(x, y) とは違う。なぜか？問題は、変数が入れ物であって、何でもとか、何かとか、はっきりしない具体値が入ることだ。ほとんどどんな種類の値も入り得る。学生、鳥、数、複雑な数学オブジェクト、データ構造、プログラム、など。

論理式	評価方法
∃yφ	y を1個見つける。
∀xφ	x にすべての値を入れてみる。

論理式 ∃yφ があるとき、 y について φ が成り立つような具体値 y を見つければよい。成功したら、∃yφ を T と評価する。失敗したら（φ を成り立たせる具体値 y がなければ）、 F と評価する。
対して ∀xφ を評価するには、 x が取り得るすべての値について φ が成り立つことを示せばよい。成功したら、∀xφ を T と評価する。失敗したら（φ を F にするような値 x があれば）、 F と評価する。

もちろん、論理式を評価するには、語ろうとしている具体値の集合が定まっていなければならない。このため、述語論理式の真偽値は、実際の値の選択と含まれる述語記号や関数記号の意味によって変わる。

変数が有限種類の値しかとらないなら、合成的に論理式を評価するプログラムを書ける。

根の節が ∧, ∨, →, ￢のどれかなら、 1章で述べたように部分木の真偽値を計算して、対応する論理演算子で φ の真偽値を計算できる。
根が限量子なら、上で述べた方法を使う。
残りは、根が述語記号 P の場合。（命題論理ではアトムであり、計算するまでもなかった。）述語は n 個の引数を要し、引数 t₁, .., t_n は項でなければならない。 P(t₁, .., t_n) の形の論理式の真偽値を計算できる必要がある。

論理式 P(t₁, .., t_n) は、述語論理よりも多くの場合がある。 n=2 のとき、 P の意味は「t₁ によって計算される数は、 t₂ によって計算される数以下である」というものかもしれない。 P の真偽値を適当に決めることはできない。関数記号と述語記号をすべて含むモデルが必要だ。例えば、実数を項とし、実数上の「以下である」関係を P とする。

定義 2.10

F を関数記号の集合、 P を述語記号の集合とする。各記号が要する引数の個数は決まっている。対 (F, P) のモデル M は次のデータ集合から成る。

空でない、具体値全体の集合 A
n 引数の f ∈ F に対して、 Aⁿ （A 上の n 個組み全体の集合）から A への具体関数
f^M: Aⁿ → A
n 引数の P ∈ P に対して、 A 上の n 個組みの部分集合
P^M ⊆ Aⁿ

f と f^M、および P と P^M の違いは非常に重要だ。記号 f と P は単なる記号であり、一方 f^M と P^M はモデル M における具体関数と具体関係である。

例 2.11

F = {+, *, -, s} とし、 P = {=, ≦, ＜, zero} とする。 +, *, - は 2 引数、s は 1 引数を取る。 =, ≦, ＜は 2 引数述語、zero は 1 引数述語である。モデル M を次のように選ぶ。

空でない集合 A は、実数全体の集合
関数 +^M, *^M, -^M は引数として実数を 2 つ取り、それぞれ和、積、差を返す。［関数 s^M は 1 実数［整数］を取って次の数 を返す。］
述語 =^M, ≦^M, ＜^M はそれぞれ等しい、以下である、より小さい関係をモデル化する。述語 zero^M が r について成り立つとは r = 0 であることである。

例 2.12

F = {e, ・} とし、 P = {≦} とする。 e は定数、・は 2 引数関数、 ≦ は 2 引数述語である。・と ≦ は中置記法で書く。

(t₁ ・ t₂) ≦ (t ・ t)

モデル M は集合 A としてビット列全体の集合を考えている。ビット {0, 1} 上の有限長の語全体の集合であり、 ε で表される空列を含む。

e の解釈 e^M は単に空の語 ε を返す。
・の解釈・^M は語の連結である。例えば、0110 ・^M 1110 は 01101110 である。一般に、 a₁..a_k と b₁..b_n があって a_i, b_j ∈ {0, 1} のとき、 a₁..a_k ・^M b₁..b_n は a₁..a_kb₁..b_n である。
≦ の解釈は接頭語順序である。 s₁ が s₂ の接頭語であるとは、 s₁ ・^M s₃ = s₂ であるようなビット列 s₃ があることである。例えば、011 は 011001 や 011 の接頭語だが、010 は違う。つまり、 ≦ は {(s₁, s₂) | s₁ は s₂ の接頭語である} という集合である。

このモデル上で非形式的に検証したい述語論理式をいくつか挙げる。

このモデル上で、論理式
∀x (x ≦ x・e) ∧ (x・e ≦ x)
の意味は、どんな語も自分自身に空語を連結したものの接頭語であり、逆も成り立つことである。明らかに、このモデル上では s ・^M ε は s そのままであり、どんな語も自分自身の接頭語である。
このモデル上で、論理式
∃y ∀x (y ≦ x)
の意味は、どんな語の接頭語でもあるような語 s が存在することである。これは真であり、そのような語 ε が存在する。（この場合、他の選択肢はない。）
このモデル上で、論理式
∀x ∃y (y ≦ x)
の意味は、どんな語にも接頭語があることである。これは明らかに真であり、x によって y は一般に複数の選択肢がある。［ε, x自身, その他］
このモデル上で、論理式
∀x ∀y ∀z ((x ≦ y) → (x・z ≦ y・z))
の意味は、s₁ が s₂ の接頭語ならば、任意の語 s に対して s₁s は s₂s の接頭語であることである。これは明らかに偽である。例えば、s₁ を 01、s₂ を 011、s₃ を 0 とする。［01 ≦ 011 だが、￢ (010 ≦ 0110)］
このモデル上で、論理式
￢∃x ∀y ((x ≦ y) → (y ≦ x))
の意味は、s₁ の接頭語ならば s₁ を接頭語とするような語 s はないことである。これは真であり、そのような s はあり得ない。そのような s が存在するとする。 s は明らかに s0 の接頭語だが、 s0 は s よりビット数が多ければ s の接頭語でない。

引数の個数以外、モデルの概念はほとんど制限がない。

でも、モデルを設計・実装するときはモデル化したいものを十分正確に表し、抽象化によって現実との対応を失わないように。

例えば、家族関係のデータベースを作るなら、 father-of(x, y) の解釈を「x は y の娘である」ことにするのはお馬鹿さんです。血縁関係のデータベースに「より背が高い」述語を入れる必要はない。でも、データベースに機能を追加するなら良いかもしれない。

1 つ残った問題は、 ∀xφ や ∃xφ をモデル上の値 a について検証するとき、これまでの文法では表せないことだ。 φ[a/x] は意味は通じるが、論理式ではない。 a は項ではなくモデルの要素である。

論理式を環境に関連付けて解釈することにする。環境とはすべての変数についての表である。表 l は変数 x をモデル上の値 l(x) に関連付ける。

l: var → A

このような表があれば、すべての論理式の真偽値を計算できるが、計算のために表の更新が必要なこともある。

定義 2.13

l を、具体値全体の集合 A に対する表とする。 a ∈ A とする。 l[x → a] とは、 x を a へ、それ以外の変数 y を l(y) へ写すような表である。

これで、述語論理の意味論を定義できる。

定義 2.14

対 (F, P) に対するモデル M と、環境 l があるとき、 充足関係を φ 上の構造帰納法によって定義する。

M |=_l φ

とは、モデル M 上で環境 l を期待すると φ が T と計算されることを意味する。

P :	φ が P(t₁, .., t_n) という形なら、 l に従ってすべての変数を値に置き換えて、 A 上の項 t₁, .., t_n を具体値 a₁, .., a_n に計算する。 M \|=_l P(t₁, .., t_n) は、 (a₁, .., a_n) ∈ P^M と同値である。
∀x :	M \|=_l ∀xψ は、すべての a ∈ A について M \|=_{l[x → a]} ψ が成り立つこと。
∃x :	M \|=_l ∃xψ は、ある a ∈ A について M \|=_{l[x → a]} ψ が成り立つこと。
￢ :	M \|=_l ￢ψ は、 M \|=_l ψ が成り立たないこと。
∨ :	M \|=_l ψ₁∨ψ₂ は、 M \|=_l ψ₁ または M \|=_l ψ₂ が成り立つこと。
∧ :	M \|=_l ψ₁∧ψ₂ は、 M \|=_l ψ₁ かつ M \|=_l ψ₂ が成り立つこと。
→ :	M \|=_l ψ₁→ψ₂ は、 M \|=_l ψ₁ が成り立てば M \|=_l ψ₂ も成り立つこと。

M |/=_l φ と書いて、 M |=_l φ が成り立たないことを表す。

l と l' が φ の自由変数の集合上で同一なら、 M |=_l φ が成り立つとは M |=_l' φ が成り立つこと。 φ に自由変数が含まれないとき、 φ を文と言う。 M |=_l φ が成り立つか成り立たないかは、 l の選択によらないので、文 φ に対しては

M |= φ

と書く。

例 2.15

F = {alma}, P = {loves} とする。 alma は定数で、loves は 2 引数述語である。モデル M について、 A = {a, b, c}, 関数 alma^M = a とし、述語

loves^M = {(a, a), (b, a), (c, a)}

とする。モデル M が次を充足するか検証しよう。

Almaを好きな人を好きな人は、Almaを好きではない。

まず、これを述語論理の文で表す。

∀x ∀y (loves(x, alma) ∧ loves(y, x) → ￢loves(y, alma))

モデル M はこの論理式を充足するか？充足しない。 x に a を、y に b を選ぶと成り立たない。 [loves(a, a) ∧ loves(b, a) → ￢loves(b, a)]

A と alma^M は M のまま、

loves^M' = {(a, a), (b, a), (c, b)}

としたらどうか？ Almaを好きな人を好きな人は c だけだが、 c は Almaを好きでないので、モデル M' について上の論理式は成り立つ。［Almaを好きな人 = {a, b}, Almaを好きな人を好きな人 = {a, b, c} じゃないのか？］

演習 2.6

論理式
φ = ∀x ∀y Q(g(x, y), g(y, y), z)
を考える。 Q は 3引数述語、g は 2引数関数である。
M |=_l φ であるような M と l、
M' |/=_l' φ であるような M' と l' を見つけよ。
文
φ = ∀x ∃y ∃z (P(x, y) ∧ P(z, y) ∧ (P(x, z) → P(z, x)))
を考える。次のモデルのうち φ を充足するのはどれか？
(a)　自然数全体の集合および P^M = {(m, n) | m < n} から成るモデル M

^M'

^M"

P を 2引数述語とする。
文 ∀x ￢P(x,x) を充足するモデル M を見つけよ。
M' |/= ∀x ￢P(x,x) であるようなモデル M' を見つけよ。
文
∀x (∃y P(x, y) ∧ (∃z P(z, x) → ∀y P(x, y)))
を考える。与えられたモデルの意味は選んだ表 l と無関係だった。適当なモデルを選んでこの文を評価せよ。充足関係の定義に従って部分式を評価するとき、初期の表 l がスタックのように伸び縮みするのに注目。
F = {d, f, g} とする。 d は定数記号、f は 3引数関数記号、g は 2引数関数記号である。 M として自然数全体の集合 {0, 1, 2, ..} を選ぶ。 d^M = 2, f^M(k, n, m) = k*n + m, g^M(k, n) = k + n*n とする。例えば、 f^M(1, 2, 3) = 5, g^M(2, 3) = 11 である。表 l を l(x) = 5, l(y) = 7 として、モデル M における次の項の値を計算せよ。
(a)　f(d, x, d)
(b)　f(g(x, d), y, g(d, d))
(c)　g(f(g(d, y), f(x, g(d, d), x), y), f(y, g(d, d), d))
φ を論理式
∀x ∀y ∃z (R(x, y) → R(y, z))
とする。 R は 2引数述語記号である。
(a)　A = {a, b, c, d}, R^M = {(b, c), (b, b), (b, a)} とする。 M |= φ か？自分の答えを正当化せよ。
(b)　A' = {a, b, c}, R^M' = {(b, c), (a, b), (c, b)} とする。 M' |= φ か？自分の答えを正当化せよ。

2.4.2 論理的帰結

M |=_l φ は分かった。命題論理では φ₁, .., φ_n |= ψ と書いて、 ψ は φ₁, .., φ_n の論理的帰結と言い、 φ₁, .., φ_n がすべて T と計算されれば、 ψ も T と計算されることを表した。

定義 2.16

φ₁, .., φ_n, ψ を述語論理式とする。 φ₁, .., φ_n |= ψ とは、 すべてのモデル M と表 l に対して、 1 ≦ i ≦ n であるような i について M |=_l φ_i ならば、 M |=_l ψ であることである。述語論理において記号 |= は 2つの意味で使われている。

M |= φ であるようなモデル M がある

のように文の充足可能性を表したり、

φ₁, .., φ_n |= ψ

で論理式の論理的帰結を表したりする。

まず、M |= φ を確かめるとき、 M の値全体の集合 A が無限集合だと問題が起きる。例えば、φ が文 ∀x ψ のとき、無限個の a に対して M |=_{[x → a]} ψ を検証する必要がある。

もっと深刻なことに、 φ₁, .., φ_n |= ψ を検証するには、 すべてのあり得るモデルについて検証しなければならない。命題論理では真偽値の計算はできたが、述語論理では難しい。

論理的帰結が恒真だと示せるのは、ごく限られた場合だけ。既出の限量子の等価性は重要。

論理的帰結の例を 2つ。

論理的帰結
∀x (P(x) → Q(x)) |= ∀x P(x) → ∀x Q(x)
を示す。 M は ∀x (P(x) → Q(x)) を充足するモデルとする。 M は ∀x P(x) → ∀x Q(x) を充足することを示せば良い。 M |= ψ₁ → ψ₂ の定義［2.14］から、
- モデルのすべての要素が P を充足しなければ証明は終わりである。
- そうでなければ、すべての要素は P を充足する［M |= ∀x P(x)］。ここで M は ∀x (P(x) → Q(x)) を充足しているので、モデルのすべての要素は Q を充足する。
M のすべての要素が P を充足する場合もしない場合も、 M は ∀x P(x) → ∀x Q(x) を充足することを示した。
今度は逆。
∀x P(x) → ∀x Q(x) |= ∀x (P(x) → Q(x))
は恒真か？否。 M' は ∀x P(x) → ∀x Q(x) を充足するモデルとする。 A' はその下の集合、 P^M', Q^M' は P, Q の解釈とすると、 M' |= ∀x P(x) → ∀x Q(x) の意味は単に、 P^M' = A' ならば Q^M' = A' でなければならないというものだ。 P^M' ≠ A' なら、ならばは真である。反例を作れる。 A' = {a, b}, P^M' = {a}, Q^M' = {b} とすると、 M' |= ∀x P(x) → ∀x Q(x) は成り立つが、 M' |= ∀x (P(x) → Q(x)) は成り立たない。

2.4.3 同一性の意味論

述語論理の意味論の閉じてない性質は分かった。関数記号の集合 F と述語記号の集合 P 上の述語論理があるとき、必要なのは非空集合 A と具体関数 f^M と具体述語 P^M だけだった。もちろん、モデルは関数と述語の自然な解釈を持つものが良いが、 論理的帰結の概念

φ₁, .., φ_n |= ψ

は、無意味に見えようが見えまいが関係なく、あらゆるモデルに依存している。これは必要悪である。無意味か否か、どこで見分けるのか？見分ける方法は、科学たりうるのか？大体そんなことしたら、一般性が失われて、違う問題領域に適用するのが大変だぞ。余計な制約を付けない理由はたくさんある。

しかし、大きな例外が一つある。述語論理で、常に有効な特別の述語 = は、同一性を表す。（2.3.1節参照） 2引数を取り、

t₁ = t₂

項 t₁ と t₂ は同じ値に計算されるという、決まった意味を持つ。自然演繹の証明規則は 2.3.1節で議論した。意味論上は、同一性の特殊な役割は、関数 =^M を集合 A 上で実際に同一であることと解釈するものとする。すなわち、(a, b) が集合 =^M に含まれるとは、 a と b が集合 A の同一の要素であることだ。例えば A = {a, b, c} があるとき、=^M は、

{ (a,a), (b, b), (c, c) }

である。同一性の意味論は単純なので、常にモデル化されているものとする。

演習 2.7

3つの文について考える。
φ₁ = ∀x P(x, x)
φ₂ = ∀x∀y (P(x, y) → P(y, x))
φ₃ = ∀x∀y∀z (P(x, y) ∧ P(y, z) → P(x, z))
2項述語 P が反射律、対称律、推移律を表すのはどれか。どの文も他の文の論理的帰結でないことを、任意の2つの文を満たすモデルが残り1つを満たさないことによって示せ。つまり、3つのうち2つの性質を満たす2項関係を3つ見つけよ。
論理的帰結を示せ。
∀xP(x) ∨ ∀xQ(x) |= ∀x (P(x) ∨ Q(x))
∀x ￢φ |= ￢∃x φ を証明せよ。そのためには、∀x ￢φ を満たすすべてのモデルが￢∃x φ を満たすことを説明しなければならない。 2.4.2節の例を参考にせよ。
φ, ψ, η を文とする。
(a)　φ |= ψ ならば、￢φ |= ψ であってはならないのか？
(b)　φ∧η |= ψ ならば、φ |= ψ かつ η |= ψ か？
(c)　φ |= ψ または η |= ψ ならば、φ∨η |= ψ か？
(d)　φ |= ψ と φ→ψが恒真であるが同値である理由を述べよ。
次を示せ。
∀x (P(x)∨Q(x)) |/= ∀xP(x) ∨ ∀xQ(x)
すなわち、∀x (P(x)∨Q(x)) を満たすが ∀xP(x) ∨ ∀xQ(x) を満たさないモデルを見つけよ。
論理式の集合 φ₁, .., φ_n について、論理式に含まれるすべての述語記号、関数記号のモデルがあって、そのモデル上で論理式がすべて T と評価されるとき、この論理式の集合は無矛盾であると言う。以下の論理式の集合が無矛盾であることを示せ。
(a)　∀x￢S(x, x), ∃xP(x), ∀x∃yS(x, y), ∀x(P(x)→∃yS(y, x))
(b)　∀x￢S(x, x), ∀x∃yS(x, y), ∀x∀y∀z((S(x, y)∧S(y, z))→S(x, z))
(c)　(∀x(P(x)∨Q(x)))→∃yR(y), ∀x(R(x)→Q(x)), ∃y(￢Q(y)∧P(y))
(d)　∃xS(x, x), ∀x∀y(S(x, y)→(x = y))
P, Q を 1引数述語記号とする。以下の論理式が定理であるか検証せよ。定理でなければ、論理式を F と評価させる P, Q のモデルを見つけよ。定理ならば、前提なしの証明を見つけよ。
(a)　∀x ∀y ((P(x)→P(y)) ∧ (P(y)→P(x)))
(b)　(∀x ((P(x)→Q(x)) ∧ (Q(x)→P(x)))) → ((∀xP(x)) → (∀xQ(x)))
(c)　((∀xP(x)) → (∀xQ(x))) → (∀x ((P(x)→Q(x)) ∧ (Q(x)→P(x))))
(d)　(∀x ∃y (P(x)→Q(y))) → (∃y ∀x (P(x)→Q(y)))
以下の述語論理式について、論理式を満たさないモデルを見つけよ。あるいは前提なしに証明せよ。
(a)　(∀x ∀y (S(x, y)→S(y, x))) → (∀x ￢S(x, x))
(b)　∃y ((∀x P(x)) → P(y))
(c)　(∀x (P(x) → ∃yQ(y))) → (∀x ∃y (P(x)→Q(y)))
(d)　(∀x ∃y (P(x)→Q(y))) → (∀x (P(x) → ∃yQ(y)))
(e)　∀x ∀y (S(x, y) → (∃z (S(x, z)∧S(z, y))))
(f)　(∀x ∀y (S(x, y) → (x = y))) → (∀z ￢S(z, z))
(g)　(∀x ∃y (S(x, y) ∧ ((S(x, y)∧S(y, x)) → (x = y)))) → (￢∃z ∀w (S(z, w)))

2.5 述語論理の決定不可能性

述語論理の紹介を否定的な結果で締めくくろう。 命題論理式 φ があるとき、少なくとも原理的には |= φ が成り立つか決定できた。 φ が n 個のアトムを持つとき、 φ の真理値表は 2ⁿ 行あって、 |= φ が成り立つとは、φ の列がすべて T であることだった。

φ が述語論理式であるとき、機械的な手順をすべての φ に対して用いることはできない。形式的な証明を与えることはできず、非形式的な計算の概念を用いる。

述語論理式が恒真であるかを決定する問題は、 決定問題として知られている。決定問題を解くプログラムは、問題の実例を入力に取り、必ず終了して yes か no を正しく出力する。述語論理の決定問題では、入力に任意の述語論理式 φ を取り、論理式が恒真なら yes、恒真でないなら no を出力するのが正しいプログラムである。決定問題を解くプログラムは、良い形式の入力すべてに対して終了しなければならない。

命題論理の恒真性

述語論理式 φ があるとき、 |= φ は成り立つ。 yes か no か？

この問題が解けないことを示す。原理的にはすべての φ について恒真かどうか分かるが、すべての φ について使える機械的な手順はない。

問題簡約という有名な方法で証明する。今の問題を、解決不可能と知られている他の問題に帰着する。これは証明規則 RAA の実例である。

解決不可能と知られていて、面白くて、述語論理に近そうな問題は、 ポスト対応問題である。

ポスト対応問題

対の有限列 (s₁, t₁), .., (s_k, t_k) がある。 s_i, t_i はすべて正の長さをもつビット列である。連結された列 s_i1..s_in = t_i1..t_in であるようなインデクス列 i₁, .., i_n (n≧1) は存在するか？

この問題の解ける実例を挙げる。具体的な対応問題の例 C は 3つの対の列

C = ((1, 101), (10, 00), (011, 11))

この問題の解は (1, 3, 2, 3) で、 s₁s₃s₂s₃ = t₁t₃t₂t₃ = 101110011 である。こんな問題解けるに決まってる？決定問題を解くプログラムは、問題のすべての実例を計算しなければならないことを忘れないように。次の問題は、もう少し難しい。

s₁=001 　s₂=01 　s₃=01 　　s₄=10
t₁=0 　　t₂=011 　t₃=101 　t₄=001

この実例を手で解くか、この実例を解くプログラムを書け。

インデクス列に同じ数が何度現れても良い。つまり、探索空間は無限であり、問題は解けなそうな気がする。この本では形式的な証明は省略。

次の定理の証明は数学者 A. Church による。

定理 2.17

述語論理の恒真性の決定問題は、解決不可能である。任意の φ に対して |= φ が成り立つか決定する手順はない。

証明

述語論理の恒真性は決定可能であり、ポスト対応問題も解決できるものとする。対応問題の実例 C は、

s₁ .. s_k
t₁ .. t_k

有限の空間と時間内に、 |= φ が成り立つことと上の対応問題の実例 C が解を持つことは同値であるような述語論理式 φ を作れる。関数記号 e は定数であり、 f₀, f₁ は 1引数関数記号である。 e は空列、 f₀, f₁ はそれぞれ 0, 1 を連結するものとする。例えば、ビット列 b₁..b_l というビット列は、

f_bl(..(f_b1(e))..)

ビット列を逆順にコーディングしていることに注意。論理式を読みやすくするため、 f_bl(..(f_b1(t))..) を f_b1..bl(t) と略記する。

P は 2引数述語記号である。 P(s, t) は、項 s が s_i1..s_im を表し、項 t が t_i1..t_im を表すようなインデクス列 (i₁, .., i_m) が存在することを意味する。

文 φ の構造は、

φ₁ ∧ φ₂ → φ₃

ここで、

φ₁ = ∧_i=1^k P(f_si(e), f_ti(e))
φ₂ = ∀v ∀w (P(v, w) → ∧_i=1^k P(f_si(v), f_ti(w))
φ₃ = ∃z P(z, z)

論理式 φ がすべてのモデルについて成り立つことと、ポスト対応問題 C が解を持つことは同値であることを主張する。

|= φ が成り立つものとする。作戦は、φ のモデルを見つけ、そのモデルを満たす φ の意味するものを観察して、対応問題 C の解を見つけようというものだ。モデルの具体値空間 A は、空列を含む有限長のビット列全体の集合である。定数 e の解釈 e^M は空列である。 f₀ の解釈 f₀^M は、引数に 0 を連結する。

f₀^M(s) = s0

同様に、

f₁^M(s) = s1

M 上の P の解釈は、

P^M = {(s, t) | s = s_i1..s_im かつ t = t_i1..t_im であるようなインデクス列 (i₁, .., i_m) が存在する }

s, t はビット列、 s_i, t_i は対応問題 C のデータである。

モデル M において φ が成り立つならば、 C が解決可能であることを示す。 M は φ₁ と φ₂ を満たす。例えば、φ₂ が M について言っているのは、対 (s, t) が P^M に含まれるなら、 i = 1, .., k について対 (s s_i, t t_i) も P^M に含まれることである。 (s, t) ∈ P^M ならば、 s = s_i1..s_im, t = t_i1..t_im であるようなインデクス列 (i₁, .., i_m) が存在する。新しいインデクス列 (i₁, .., i_m, i) を選び、 s s_i = s_i1..s_ims_i かつ t t_i = t_i1..t_imt_i であることを観察すれば良い。（M |= φ₁ は、なぜ成り立つのか？）

M |= φ₁∧φ₂→φ₃ かつ M |= φ₁∧φ₂ なので、 M |= φ₃ である。 φ₃ と P^M の定義より、 C の解が見つかる。

逆に、ポスト対応問題 C がインデクス列 (i₁, .., i_n) を解に持つものとする。 M' が任意のモデルであって、定数 e^M'、 1引数関数 f₀^M', f₁^M'、 2引数述語 P^M' を持つとき、 M' が φ を満たすことを示さなければならない。 φ の構文解析木の根が → であることは、 M' |= φ の定義から重要だ。この定義から、 M' |/= φ₁ または M' |/= φ₂ ならば証明は終わる。 M' |= φ₁∧φ₂ の場合、 M' |= φ₃ を検証する必要がある。ここでは、モデル M' の値定義域 A' における有限長ビット列を解釈する。インタプリタでプログラミング言語を他言語にコーディングするのとは違う。解釈は、有限長ビット列のデータ構造上で再帰的に定義された関数 interpret で行う。

interpret(ε) = e^M'
interpret(s0) = f₀^M'(interpret(s))
interpret(s1) = f₁^M'(interpret(s))

interpret(s) は s の長さについて再帰的に定義される。この解釈は逆順である。例えば、ビット列 0100110 は、

f₀^M'( f₁^M'( f₁^M'( f₀^M'( f₀^M'( f₁^M'( f₀^M'(e^M')))))))

ただし、

interpret(b₁..b_l) = f_bl^M'(..(f_b1^M'(e^M'))..)

は、A' の f_s(e) 　(ここで、s = b₁..b_l) を意味する。

この定義と M' |= φ₁ より、 i = 1, .., k について (interpret(s_i), interpret(t_i) ∈ P^M' である。
同様に M' |= φ₂ より、すべての (s, t) ∈ P^M' について (interpret(s s_i), interpret(t t_i) ∈ P^M' である。

この 2つのことから、 (s, t) = (s_i1, t_i1) から始めて繰り返し連結を行うと、

(interpret(s_i1..s_in), interpret(t_i1..t_in) ) ∈ P^M'

s_i1..s_in と t_i1..t_in は共に C の解を成し、等しい。よって、要素 interpret(s_i1..s_in) と interpret(t_i1..t_in) は A' において同一である。つまり、対

(interpret(s_i1..s_in), interpret(t_i1..t_in) ) ∈ P^M'

は M' において ∃zP(z, z) を示し、 M' |= φ₃ である。

あと 2つ否定的な結果が簡単に得られる。 M |= φ であるようなモデル M があれば、論理式 φ は充足可能であると言う。この性質は厄介だ。論理式

∃x (P(x) ∧ ￢P(x))

は明らかに充足不可能である。 φ が充足不可能であるとは、￢φ が恒真、すなわちすべてのモデルで成り立つことである。つまり、M |= ￢φ が恒真であることだ。述語論理の恒真性は決定不可能なので、充足可能性も決定不可能である。

もう1つの決定不可能性は、述語論理の健全性と完全性による。

|= φ iff |- φ　　(2.2)

ここでは証明しない。恒真性が決定不可能なので、 (2.2) より証明可能性も決定不可能である。

×　与えられた論理式に対して、機械的に証明を生成するか論理式が間違っていることを証明する、完璧な定理証明器を実装することはできない。
○　機械には人間の手助けが必要である。機械だけでは創造性が制限される。

演習 2.8

述語論理の証明計算が健全であるとして（3問目を見よ）、 |- の左辺の論理式がすべて T と評価され、右辺の論理式が F と評価されるようなモデルを見つけることによって、以下のシーケントが証明不可能であることを示せ。（これで証明が存在しないことを保証できるのはなぜか。）
(a)　∀x (P(x)∨Q(x)) |- ∀xP(x) ∨ ∀xQ(x)
(b)　∀x (P(x)→R(x)), ∀x (Q(x)→R(x)) |- ∃x (P(x)∧Q(x))
(c)　(∀xP(x))→L |- ∀x (P(x) → L), ここで L は 0引数述語記号
(d)　∀x∃y S(x, y) |- ∃y∀x S(x, y)
(e)　∃xP(x), ∃yQ(y) |- ∃z (P(z)∧Q(z))
P，Q は 1引数述語記号である。以下の論理式が定理かどうか検証せよ。
- 定理でなければ、論理式を F と評価するような P, Q のモデルを見つけよ。
- 定理ならば、前提なしの証明を見つけよ。
(a)　∀x ∀y ((P(x)→P(y)) ∧ (P(y)→P(x)))
(b)　(∀x ((P(x)→Q(x)) ∧ (Q(x)→P(x)))) → ((∀xP(x))→(∀xQ(x)))
(c)　((∀xP(x))→(∀xQ(x))) → (∀x ((P(x)→Q(x)) ∧ (Q(x)→P(x))))
(d)　(∀x ∃y (P(x)→Q(y))) → (∃y ∀x (P(x)→Q(y)))
述語論理の自然演繹規則の健全性を示すには、直感的には証明規則の前提がすべて真であるとき結論も真であることを示せば良い。変数と限量子の存在によって何が難しくなるのか？健全性を証明するのに必要な帰納法を正確に形式化できるか？
述語論理の証明計算が健全であるとして（3問目を見よ）、次の 2つのシーケントが述語論理では証明できないことを示せ。証明計算の健全性より、 |- の左辺の論理式が成り立ち、右辺が成り立たないようなモデルを見つければ良い。
(a)　∃x (￢P(x)∧Q(x)) |- ∀x (P(x)→Q(x)
(b)　∃x (￢P(x)∨￢Q(x)) |- ∀x (P(x)∨Q(x))