演習問題 (PDF)

論理学
第 13 回不完全性定理と直観主義論理
萩野達也
慶應義塾大学
環境情報学部
LOGIC13 (1/17)
健全性と完全性
健全性
正しいことしか証明されない
証明できたことはすべて正しいことである
論理学および公理的理論において重要
完全性
正しいことは必ず証明される
一階述語論理は健全かつ完全である
すべての閉じた論理式は真か偽かを証明できる
公理的理論は必ずしも完全である必要はない
群の公理的理論
1. ∀x∀y∀z((x · y) · z = x · (y · z))
2. ∀x(e · x = x ∧ x · e = x)
3. ∀x(x · x−1 = e ∧ x−1 · x = e)
∀x∀y(x · y = y · x) の真偽は証明できない
LOGIC13 (2/17)
ペアノの自然数論の不
完全性
ペアノの自然数論 PA
自然数の構造 N = hN, Ii を公理化したもの
自然数を扱う数学の定理などにおいて必要なものを公理化したはず
完全であることが望ましい
ゲーデルの第一不完全性定理 (Gödel First Incompleteness Theorem)
PA が無矛盾 (矛盾を証明することはない) であれば不完全である．
PA が不完全であるとは?
PA の公理から証明することができない自然数に関する真実がある．
PA が不完全なら，もっと公理を追加すれば良いのでは?
PA にいくら公理を追加したとしても，公理集合が決定可能 (論理式が公理かど
うか判定する手段がある) である限り不完全である．
ゲーデルの第二不完全性定理 (Gödel Second Incompleteness Theorem)
「PA が無矛盾である」は，PA では証明できない．
LOGIC13 (3/17)
ゲーデル文
PA の不完全性定理は，次のようなゲーデル文を作成することで示す．
G は「G は証明できない」という命題とする．
完全だとすると G あるいは G の否定が証明可能であるが，
G が証明可能であれば，G は証明できないはずで
G が証明できないのであれば，G の否定が証明できるはずであるが，そでは G
が証明できることになる．
どちらにしても矛盾する．すなわち「PA が完全であるとすると PA は矛盾する」
対偶をとると，
「PA が無矛盾であれば PA は完全ではない」
集合論におけるラッセルのパラドックスに似ている (?)
集合 R を {x | x 6∈ x} とする．
R ∈ R とすると R 6∈ R となり，
R 6∈ R とすると R ∈ R となり，どちらにしても矛盾する．
LOGIC13 (4/17)
ゲーデル数
ゲーデル文 G =「G は証明できない」は自己言及の文
ペアノの自然数論は数字を扱う公理的理論である
論理式を数字で符合化する
ゲーデル数 (Gödel number)
論理式を構成する記号に一意的な数字を割り当てる
論理式 P は記号の列なので，それぞれを表す数字の列 x1 , x2 , . . . , xn が対応
する
論理式 P のゲーデル数
n
♯G = 2x1 × 3x2 × · · · × px
n
pn は n 番目の素数
ゲーデル数が与えられると，素因数分解することで，もとの記号の列が分かる．
LOGIC13 (5/17)
ゲーデル文の構成
PA を公理とモーダス・ポネンスなどの推論規則からなる自然数の公理的理論とする
次のような論理式を作ることができる
A(x) =「x は公理のゲーデル数である」
M (x, y, z) = 「z をゲーデル数とする論理式は，
x をゲーデル数とする論理式と，
y をゲーデル数とする論理式から
モーダス・ポネンスを使って導くことができる」
P (x, y) =「ゲーデル数 x の論理式の証明は論理式の列 y で与えられる」
T (x) = ∃yP (x, y) =「ゲーデル数 x の論理式は証明可能である」
a(y, z) = 「ゲーデル数 y の論理式の変数 x に
自然数 z を代入した論理式のゲーデル数」
ゲーデル文
g を論理式 ¬T (a(x, x)) のゲーデル数とする
ゲーデル文 G = ¬T (a(g, g))
LOGIC13 (6/17)
不完全性定理の証明
第一不完全性定理の証明
G が証明可能であれば，a(g, g) は証明できない論理式のゲーデル数であるが，
それは G のゲーデル数であり矛盾する．
逆に ¬G が証明可能であれば，a(g, g) は証明可能な論理式のゲーデル数を意味
し，それは G なので，やはり矛盾する．
すなわち，G も ¬G も証明できない．
第二不完全性定理の証明
矛盾を表す論理式のゲーデル数を b とすると
¬T (b) = PA が無矛盾である
第一不完全性定理の G が証明可能であれば，矛盾するので，G ⊃ T (b)
対偶をとれば，¬T (b) ⊃ ¬G
同じように，¬G が証明可能であっても矛盾するので，¬G ⊃ T (b)
対偶をとれば，¬T (b) ⊃ G となり，先ほどと矛盾する
すなわち，PA が無矛盾であるとすると，矛盾する．
LOGIC13 (7/17)
不完全性定理とコン
ピュータの発明
PA の不完全性定理はどうして成り立つのか?
論理式を数で符合化することで自己言及の論理式を作った
PA を仮定すれば，数字で符合化できる
フォンノイマン
PA は完全であることを証明しようとしていた
ゲーデルの不完全性定理にショックをうける
ゲーデル数のアイデアをもらい，ノイマン型コンピュータを発明
デジタル計算機では，すべてを数値として扱う
プログラム自身も数値としてメモリに置いておく (ストアドプログラム)
プログラム自身もデータ
LOGIC13 (8/17)
直観主義論理
20 世紀の数学
カントールの集合論「数学的思考はその自由性にある」
数学的対象はその存在が矛盾をひき起こすものでない限り実際に存在するものと
考える．
19 世紀までの数学では，幾何学，整数，有理数，実数など，具体的なものを対
象とした．
20 世紀の数学では，群や体，位相空間，圏など抽象的な対象を扱う．
矛盾の克服
カントールの集合論にはラッセルのパラドックスのように矛盾を含んでいる．
形式主義的な立場からは，公理に制限を入れることで克服しようとした．
これまでの数学の成果を失うことなく形式的に進めることが可能になった．
直観主義 (insuitionism)
数学的対象は人間が作り出すものであり，その存在は構成的な手続きで示さなく
てはならない．
これまでの数学の一部の成果を失うことになるかも知れない．LOGIC13 (9/17)
対象が存在することの
意味
古典論理では背理法を用いて存在を示していた．
性質 P を持つ対象が存在しないと仮定すると矛盾する，だから P を持つ対象が
存在しなければならない．
直観主義では背理法的な存在証明を認めない．
P をみたす対象の存在を示すには，その対象を見出すための有限の手続きを具体
的に与えなくてはならない．
例「xy = z となる実数 x, y, z で，x と y が無理数で z が有理数であるものが存在す
る」の証明
√ √2
2
を考える．
√
√ 2
√
2
が有理数であれば，x と y を 2 とすれば良い．
√ √2
√
√ √2
2
が無理数であれば，x を 2
とし，y を 2 とすれば，z は 2 となり
有理数である．
この証明では x, y, z に何をとったら良いか具体的に示していないので，直観主義的
には認められない．
LOGIC13 (10/17)
古典論理との違い
古典論理では ∃x∀y(P (y) ⊃ P (x)) は恒真である．
ある a0 について P (a0 ) が成り立てば，どんな b についても P (b) ⊃ P (a0 ) が
成り立つので，∀y(P (b) ⊃ P (a0 )) が成り立つ．
どの c について P (c) が成り立たないとすると，任意に選んだ d に対して，
P (c) ⊃ P (d) が成り立つので，∀y(P (y) ⊃ P (d)) が成り立つ．
どちらにしても ∃x∀y(P (y) ⊃ P (x)) が成り立つ．
直観主義的には ∀y(P (y) ⊃ P (x)) を真とする x として具体的に何をとれば良い
のか分からないので，上記の証明は認められない
二重否定は肯定?
¬¬A ⊃ A は古典論理では恒真
A を ∃xP (x) とすると，¬¬∃xP (x) ⊃ ∃xP (x)
¬¬∃xP (x) は，
「P (x) となる x が存在しないとすると矛盾する」を意味する
∃xP (x) は，直観主義では「P (x) となる x が存在し，具体的に見つける方法が
ある」ことを意味する
¬¬∃xP (x) ⊃ ∃xP (x) は直観主義的には正しくない
LOGIC13 (11/17)
排中律
A∨B
直観主義では A が正しいと具体的にいえるか，B が正しいと具体的にいえる時
に真と考える
排中律
A ∨ ¬A
古典論理では恒真
直観主義では一般には正しくない
ゴールドバッハ予想
「任意の 4 以上の偶数は 2 つの素数の和として表される」
非常に大きな偶数までこの予想が正しいことが認められているが，まだ証明され
ていない
P (n) =「2(n + 2) は 2 つの素数の和として表すことができない」
∃xP (x) ∨ ¬∃xP (x)
LOGIC13 (12/17)
構成的数学とプログ
ラム
構成的数学 (constructive mathematics)
直観主義に基づく数学の再構成
背理法を用いない
構成的な概念と構成的な証明の基づいた数学の再構成
プログラム
問題の解に対して具体的な計算方法を示す
プログラムがその問題に関する証明
例
「任意の 2 つの自然数 m, n に対して，最大公約数が存在する」
ユークリッドの互除法は最大公約数が存在することの証明
プログラム=証明
論理式の構成的証明からプログラムを抽出することができる
LOGIC13 (13/17)
直観主義論理の体系
直観主義論理体系 LJ
古典論理体系 LK と同じ始式および規則
LJ における式は，A1 , . . . , Am → B に限る (m は 0 でも構わなく，B はなく
ても良い)
構造に関する推論規則
(weakening 左)
Γ→B
A, Γ → B
(contraction 左)
A, A, Γ → B
A, Γ → B
(cut)
(weakening 右)
(exchange 左)
Γ→
Γ→A
Γ, A, A′ , Π → B
Γ, A′ , A, Π → B
Γ → A A, Π → B
Γ, Π → B
(B は空またはただ一つの論理式)
LOGIC13 (14/17)
直観主義論理の推論
規則
論理結合子に関する推論規則
(∧ 左 1)
(∧ 右)
(∨ 右 1)
(⊃ 左)
(¬ 左)
(∀ 左)
(∃ 左)
A, Γ → C
A ∧ B, Γ → C
Γ→A Γ→B
Γ→A∧B
Γ→A
Γ→A∨B
Γ → A B, Π → C
A ⊃ B, Γ, Π → C
Γ→A
¬A, Γ →
A[t/x], Γ → B
∀xA, Γ → B
A[z/x], Γ → B
∃xA, Γ → B
(∧ 左 2)
(∨ 左)
(∨ 右 2)
(⊃ 右)
(¬ 右)
(∀ 右)
(∃ 右)
B, Γ → C
A ∧ B, Γ → C
A, Γ → C B, Γ → C
A ∨ B, Γ → C
Γ→B
Γ→A∨B
A, Γ → B
Γ→A⊃B
A, Γ →
Γ → ¬A
Γ → A[z/x]
Γ → ∀xA
Γ → A[t/x]
Γ → ∃xA
LOGIC13 (15/17)
直観主義論理に関する
定理
cut 除去定理
式 Γ → A が LJ で証明可能であれば，Γ → A に至る LJ の証明図で cut を一度
も用いないものが存在する．
直観主義命題論理の決定性
与えられた式が命題論理の形式体系 LJ で証明可能か否かを判定する有限の手続
きが存在する．
直観主義述語論理の決定不能性
与えられた式が述語論理の形式体系 LJ で証明可能か否かを有限の手続きで判定
する方法は存在しない．
直観主義述語論理の disjunction property
形式体系 LJ で論理式 A ∨ B が証明可能ならば，A か B のいずれかが LJ で証
明可能である．
直観主義述語論理の exisitence property
形式体系 LJ で論理式 ∃xA が証明可能ならば，ある項 t が存在して A[t/x] が
LOGIC13 (16/17)
LJ で証明可能である．
まとめ
ゲーデルの不完全性定理
PA が無矛盾であれば不完全である．
「PA が無矛盾である」は，PA では証明できない．
直観主義
背理法の使用を認めない
排中律が成り立たない
構成的方法で証明する
直観主義論理体系 LJ
式を A1 , . . . , Am → B に限定
LOGIC13 (17/17)

Download Report