2020 年度 数理論理学 講義資料 (1)

2020 年度 数理論理学 講義資料 (1)

青戸 等人

(

知能情報システムプログラ ム

)

目次

-

はじ めに ^{〜論理と は〜}

-

論理学概観 〜論理学の歴史を 振り 返り ながら 〜

はじ めに

証明を 書く こ と が出来ま すか？

なにを 記述すれば， 証明し たこ と になる かわか っ て いま すか？

1/63

はじ めに

証明を 書く こ と が出来ま すか？

なにを 記述すれば， 証明し たこ と になる かわか っ て いま すか？

数理論理学の基本的な知識

(

と 技

)

を学べば， こ れが

(

だい ぶ

?)

わかる よ う になり ま す． 証明の書き 方がわかれば， 証 明の読み方がわかり ま す． 証明の読み方がわかれば， 理論 への扉が開き ま す．

理論がわかれば， 理論と 実験的結果と の差分も 掴める よ う になる でし ょ う ． こ れは情報工学

/

情報科学を 専門にする 人にと っ て はと て も 大き いはずです．

数理論理学と は

数理論理学は「 推論の方法と そ の正し さ 」 について の学 問．

「 真である 論理式と は， 論理的な推論に従っ て 導かれる 論理式のこ と である ．」

ど のよ う に論理的な推論に従っ て 導かれたかを 示すも の を証明と よ ぶ．

(

数理論理学以外も 含めた

)

よ り 幅広い論理学の文脈では，

論理的な推論は演繹的推論と よ ばれる ．

2/63

+---+

| "

_理論

" |

+----+---+----+

|

_数学

|

+---+---+---+

|

_{数理論理学}

|

---+---+---

さ ま ざま な場面で， 理論的な解析を 使う こ と がある が，

そ の道具は数学． 数学のど のよ う な分野を 用いる かはいろ いろ だが

(

ある いは，

“

数学

”

には通常含ま れて ないよ う な 分野かも し れない． オ ート マト ン ， ア ルゴリ ズム， プロ グ ラ ム意味論，

etc.)

， 数学を き ち んと 使いこ なすには， 数学 の基礎と なる 数理論理学

(

論理的な推論の理解と やり 方， 数 学の仕組み・ 証明の仕方

)

を 身につける 必要がある ．

論理的な推論と は

•

推論方法の『 根本』 に焦点

•

絶対確実な推論のみ

•

後に正し く なく なる よ う なこ と がある も のは対象外

4/63

論理的な推論と は

論理的な推論の例：

「 すべて の人は死ぬ．

ソ ク ラ テスは人である ．

従っ て ， ソ ク ラ テスは死ぬ．」

「 すべて の鳥は嘴を も つ．

ペン ギン は鳥である ．

従っ て ， ペン ギン は嘴を も つ．」

“

従っ て

”

と いう

2

つの前提から

1

つの結論を 導いて いる 際に使っ て いる 推論は， 論理的な推論の例．

論理的な推論と は

こ れら の推論はど れも

「 すべて の

X

は

Y

である ．

a

は

X

である ．

従っ て ，

a

は

Y

である ．」

のよ う な一般形を も つ．

論理的な推論は， 個々 の言明の内容ではなく ， 言明の一 般的な形に基づく ．

6/63

初等教育における 論理

数学教育の

2

側面： 計算力と 証明力

計算： 問題に応じ て 正し い計算方法を 適用し て 解を 得る ． 証明： 定義や公理から 出発し ， 論理的に正し い推論を 繰り 返し て 定理を 導く ．

こ の

2

つはと て も 異なる 技． 計算力は早い段階から 学習 が始ま る

(

子供は規則が大好き

(?))

． 証明力はある 程度の年 齢から

(

自分自身に問い掛ける 態度が必要

(?))

．

計算力教育の担い手は主に解析． 証明力教育の担い手は 主に幾何． 論理そ れ自身を 学習する こ と はない．

幾何の問題での論理的な推論の例

日本の初等教育で論理的な推論を 鍛える 代表選手は， 中 学の幾何の問題．

A

B C

D

O

|AB | = |DC |

かつ

|AC | = |DB |

と する と き ，

(1) △ABC

と

△DCB

が合同である こ と を 示せ．

(2) △ABO

と

△DCO

が合同である こ と を 示せ．

8/63

三角形の合同条件：

(a) 3

辺の長さ がそ れぞれ等し い．

(b) 2

辺の長さ と そ の間の角がそ れぞれ等し い．

(c) 1

辺の長さ と そ の両端の角がそ れぞれ等し い．

つま り ， 以下のよ う な推論が正し い

「

3

辺の長さ がそ れぞれ等し い

⇒ 2

つの三角形は合同」

「

2

辺の長さ と そ の間の角がそ れぞれ等し い

⇒ 2

つの三角 形は合同」

「

1

辺の長さ と そ の両端の角がそ れぞれ等し い

⇒ 2

つの三 角形は合同」

推論ステッ プを

1

つ

1

つ辿る こ と で示せる ．

(

仮定よ り

) |AB | = |DC |

かつ

|AC | = |DB | (1) (

等号の性質よ り

) |BC | = |BC | (2)

((1),(2)

と 合同条件

(a)

よ り

) △ABC

と

△DCB

が合同

(3) ((3)

と 合同性の性質よ り

) |AB | = |DC | (4)

((3)

と 合同性の性質よ り

) ∠ OAB = ∠ ODC (5) ((3)

と 合同性の性質よ り

) ∠ ABC = ∠ DCB (6) ((3)

と 合同性の性質よ り

) ∠ ACB = ∠ DBC (7) ((6),(7)

と 減算の性質よ り

)

∠ ABO = ∠ ABC − ∠ DBC

= ∠ DCB − ∠ ACB = ∠ DCO (8)

((5),(6),(8)

と 合同条件

(c)

よ り

) △ABO

と

△DCO

が合同

10/63

数学のすべて の命題は， 定義や公理から ， 論理的な推論 によ っ て 得ら れる ．

「 有限個の開集合の共通部分は開集合である 」

「 ラ ムダ計算は合流性を も つ」

「 集合

A

と

B

が可算であればそ の直積も 可算である 」

「 任意の帰納的部分順序集合は極大元を も つ」

こ れら は現代的な数学でき ち んと 意味のある 命題． ほと んど の人には， こ れら の命題のほと んど はおま じ ないのよ う に意味を も たないかも し れない．

さ ま ざま な用語の定義はそ の分野を 勉強し ないと わから ないが， 用いる 論理的な推論はすべて 共通． ど のよ う な命 題も 論理的な推論ステッ プを

1

つ

1

つ辿る こ と で示せる ．

論理は数学のルール

直観は頭の中で考える 上で重要だが， 直観に頼っ た推論 はと て も 間違えやすい． 論理的な推論を き ち ん行う こ と で，

•

ど こ で間違えたか，

•

ど こ で思わぬ仮定が推論に入り 込んだか，

•

ど の定義が曖昧か，

など を 明確にする こ と ができ る ．

12/63

直観に頼っ た推論は誤り やすい

ア キレ スと 亀のパラ ド ッ ク ス

足の速さ で， ア キレ スはギリ シャ で伝説的です． 亀がア キレ スと 競 争し ま す． ただし ， 亀はハン ディ と し て， アキレ スよ り ゴールに近い場 所から スタ ート する こ と にし ま す．

こ のと き ， ア キレ スが亀に追いつく 状況を 考えて みま す． ま ず， ア キ レ スが亀に追いつく には， 亀がスタ ート する と こ ろ に到達し なく て はなり ま せんが， その間に亀は少し 進んでし ま いま す． し かし ， そう す る と ， アキレ スが亀に追いつく には， そのと き 亀がいる と こ ろ に到達し なく てはなり ま せんが， ま たその間にも 亀は少し 進んでし ま いま す． こ う し て ， いつま でたっ て も ア キレ スは亀に追いつけま せん

(

？

)

．

直観に頼っ た推論は誤り やすい

ベリ ーのパラ ド ッ ク ス

英語の文章に使え る 記号

(a,b,

空白

,;,

など

)

は有限個です． 従っ て ，

200

文字未満の文章の種類も 有限個し かあり ま せん． する と ，

200

文字 未満の文章で表わせる 正整数の種類も 有限個し かないこ と になり ま す．

する と ，

200

文字未満の文章で表わせる 正整数のう ち， 最大の数がある はずです． そ こ で， そ の数を

k

と おき ま し ょ う ．

正整数を 表わす文章の例：「

999

の

999

乗の

· · ·

の

999

乗 」

14/63

直観に頼っ た推論は誤り やすい

ベリ ーのパラ ド ッ ク ス

英語の文章に使え る 記号

(a,b,

空白

,;,

など

)

は有限個です． 従っ て ，

200

文字未満の文章の種類も 有限個し かあり ま せん． する と ，

200

文字 未満の文章で表わせる 正整数の種類も 有限個し かないこ と になり ま す．

する と ，

200

文字未満の文章で表わせる 正整数のう ち， 最大の数がある はずです． そ こ で， そ の数を

k

と おき ま し ょ う ．

正整数を 表わす文章の例：「

999

の

999

乗の

· · ·

の

999

乗 」 と こ ろ が，

the least positive integer that is not denoted by an English expression containing fewer than 200 occurrences of symbols

(

長さ

200

文字以下の英語文では表現でき ない最小の正整数

)

と いう 文章は

200

文字未満の文章なのに，

k + 1

を 表わし て し ま う

(

？

)

．

目次

-

はじ めに ^{〜論理と は〜}

-

論理学概観 〜論理学の歴史を 振り 返り ながら 〜

(お断り)以下で紹介する 歴史の話は， 講義内容を 俯瞰する ための参考に紹介する も のであり ， 史実の確かさ について 保証する も のではあり ま せん．

14/63

ア リ スト テレ ス論理学

論理学の始ま り と いわれて いる のはギリ シャ のア リ スト テレ ス

(Aristotle, B.C.384–322)

．

「 すべて の人は死ぬ．

ソ ク ラ テスは人である ．

従っ て ， ソ ク ラ テスは死ぬ．」

アリ スト テレ ス論理学はその後

17

世紀ま で論理学の基礎 であっ た．

ア リ スト テレ ス論理学

ア リ スト テレ スは， 以下の

4

つのタ イ プの言明について ，

syllogism

と よ ばれる 推論がど のよ う な場合に正し いか議 論し た．

All X is Y No X is Y Some X is Y

Some X is not Y

16/63

ア リ スト テレ ス論理学

以下は正し い論理的な推論か？

(1) All X is Y

Therefore, All non-Y is non-X (2) All X is Y

No Z is Y

Therefore, No Z is X (3) All X is Y

Some Z is Y

Therefore, Some Z is non-X

Venn Diagrams ベン 図

(Venn, 1881)

論理的な推論はベン 図を 使う と 考え やす い．

A

18/63

Venn Diagrams ベン 図

B

A と B の積 ( 共通部分 )

A ∩ B

20/63

A と B の和 ( 合併 )

A ∪ B

A の反転

A

^◦

22/63

B の反転

B

^◦

ド ・ モルガン の法則 (1)

(A ∪ B )

^◦

= A

^◦

∩ B

^◦

24/63

ド ・ モルガン の法則 (2)

(A ∩ B )

^◦

= A

^◦

∪ B

^◦

部分集合 (A ⊆ B )

A

B

A ⊆ B ⇔ A ∩ B = A ⇔ A ∪ B = B

⇔ A ∩ B

^◦

= 0 ⇔ A

^◦

∪ B = 1

(

こ こ で，

0

は空集合，

1

は全体集合を 表す．

)

26/63

ア リ スト テレ ス論理学 ( 再 )

前の推論

(2)

を ベン 図を 使っ て 考えて みる と ？

All X is Y No Y is Z

Therefore, No X is Z

X ⊆ Y

Y ∩ Z = 0

Therefore, X ∩ Z = 0

こ の推論にはど んな法則が使われて いる だろ う か？

X ⊆ Y

Y ∩ Z = 0

Therefore, X ∩ Z = 0

X

Y

Z

•

複雑な命題になる と ， ベン 図ではう ま く 表わせない．

28/63

真理値と 命題結合子

真理値

命題が正し い

/

正し く ないと 考える かわり に， 命題それぞれ が， 真

(

正し い場合

)

や偽

(

正し く ない場合

)

と いう 値を も っ て いる と 考える

「

Y ∩ Z = 0

」

⇐⇒

命題「

x ∈ Y ∩ Z

」 の値は偽

⇐⇒

命題「

(x ∈ Y )

かつ

(x ∈ Z )

」 の値は偽

「 かつ」 は， 単純な命題「

x ∈ Y

」 と「

x ∈ Z

」 から ， よ り 複 雑な命題を 構成する ． こ のよ う なも のを命題結合子と よ ぶ．

Y ∪ Z

に対応する 命題結合子「 ま たは」

Y

^◦に対応する 命題結合子「

not

」 も 導入でき る

真理値表

A ¬A T F F T

A B A ∧ B T T T T F F F T F F F F

A B A ∨ B T T T T F T F T T F F F

30/63

A → B の真理値

X ⊆ Y ⇔ a ∈ X implies a ∈ Y X ⊆ Y ⇔ X ∩ Y

^◦

= 0

⇔ a / ∈ X ∩ Y

^◦

⇔ a ∈ (X ∩ Y

^◦

)

^◦

⇔ a ∈ X

^◦

∪ (Y

^◦

)

^◦

⇔ a ∈ X

^◦

∪ Y

⇔ a ∈ X

^◦

or a ∈ Y

⇔ (not a ∈ X ) or a ∈ Y

つま り ，

A → B

と

¬A ∨ B

の論理的な意味は同じ ．

真理値表

命題

A, B

の真

(T)

偽

(F)

が決ま っ たと き の， 命題

¬A, A ∧ B , A ∨ B , A → B

，

A ↔ B

の真偽を 表にし たも の

A ¬A T F

F T

A B A ∧ B T T T T F F F T F F F F

A B A ∨ B T T T T F T F T T F F F

A B A → B T T T T F F F T T F F T

32/63

真理値の計算

含ま れて いる 単純な命題の真理値によ っ て ， 複雑な命題の 真理値は決ま る ．

P Q R Q → R P → (Q → R)

T T T T T

T T F F F

T F T T T

T F F T T

F T T T T

F T F F T

F F T T T

F F F T T

ア リ スト テレ ス論理学 ( 再 )

前の推論

(2)

を 命題計算を 使っ て 考えて みる と ？

All X is Y No Y is Z

Therefore, No X is Z

x ∈ X → x ∈ Y

x ∈ Y → ¬ (x ∈ Z )

Therefore, x ∈ X → ¬ (x ∈ Z )

34/63

「

x ∈ X → x ∈ Y

」 は，

T

「

x ∈ Y → ¬ x ∈ Z

」 は，

T

そ のと き ， 「

x ∈ X → ¬ x ∈ Z

」 は，

T

実際に， 真理値表で確認し て みる と ．．．

x ∈ X x ∈ Y x ∈ Z x ∈ X ¬(x ∈ Z) x ∈ Y x ∈ X

→ x ∈ Y → ¬(x ∈ Z) → ¬(x ∈ Z)

T T T T F F F

T T F T T T T

T F T F F T F

T F F F T T T

F T T T F F T

F T F T T T T

F F T T F T T

F F F T T T T

Algebra ’al-jabr’

Algebra(

代数

)

と いう と 現在では抽象代数を 指すが， 語 源はア ラ ビア 語の

’al-jabr’

：

式の変形によ っ て 等式の解を 得る 方法

1 + x = 3 − x

⇒ 2x = 3 − 1

⇒ 2x = 2

⇒ x = 1

36/63

Algebra ’al-jabr’

Algebra(

代数

)

と いう と 現在では抽象代数を 指すが， 語 源はア ラ ビア 語の

’al-jabr’

：

式の変形によ っ て 等式の解を 得る 方法

1 + x = 3 − x

⇒ 2x = 3 − 1

⇒ 2x = 3 − 1

⇒ x = 1

論理推論を 式変形のよ う に簡単にでき ないか．

ジョ ージ・ ブール

(George Boole, 1815-1864)

(

画像はウ ィ キペディ ア よ り 引用

)

37/63

ブール代数

式変形にも と づく 論理推論，

“

論理の代数

”

A. De Morgan (Formal Logic, 1874), George Boole (Calculus of Thought, 1854), C.S. Pierce, Ernst Schr¨ oder (The Algebra of Logic, 1890), W.S.Jevons (Pure Logic, 1864; Elementary Lessons in Logic, 1870).

1. X ∪ X = X 2. X ∩ X = X

3. X ∪ Y = Y ∪ X 4. X ∩ Y = Y ∩ X

5. X ∪ (Y ∪ Z ) = (X ∪ Y ) ∪ X

6. X ∩ (Y ∩ Z ) = (X ∩ Y ) ∩ X

7. X ∩ (X ∪ Y ) = X 8. X ∪ (X ∩ Y ) = X

9. X ∩ (Y ∪ Z ) = (X ∩ Y ) ∪ (X ∩ Z ) 10. X ∪ (Y ∩ Z ) = (X ∪ Y ) ∩ (X ∪ Z ) 11. X ∪ X

^◦

= 1

12. X ∩ X

^◦

= 0 13. (X

^◦

)

^◦

= X 14. X ∪ 1 = 1 15. X ∩ 1 = X 16. X ∪ 0 = X 17. X ∩ 0 = 0

18. (X ∪ Y )

^◦

= X

^◦

∩ Y

^◦

19. (X ∩ Y )

^◦

= X

^◦

∪ Y

^◦

39/63

ア リ スト テレ ス論理学 ( 再 )

X ⊆ Y (1)

Y ∩ Z = 0 (2) Therefore, X ∩ Z = 0

By (1) X ∩ Y

^◦

= 0 (3)

By (3) X ∩ Y

^◦

∩ Z = 0 (4)

By (2) X ∩ Y ∩ Z = 0 (5)

By (4),(5) (X ∩ Y ∩ Z ) ∪ (X ∩ Y

^◦

∩ Z ) = 0 (6) By (6) (X ∩ Z ) ∩ (Y ∪ Y

^◦

) = 0 (7)

By (7) (X ∩ Z ) ∩ 1 = 0 (8)

By (8) X ∩ Z = 0

2 つの方法論

1.

真理値にも と づく 方法

真と 偽と いう 命題の

“

意味

”

を 考える

「 意味論 」

2.

等式によ る 導出

規則によ っ て ， 機械的に導出ができ る かを 考える ．

「 構文論 」

まっ たく 異なる

2

つの方法だが， こ の

2

つの方法は同値に なる

(

「 完全性 」

)

41/63

エミ ール・ レ オン ・ ポスト

(Emil Leon Post, 1897-1954)

(

画像はウ ィ キペディ ア よ り 引用

)

数学の厳密化

論理学が

18

世紀ま でほと んど 発展がなかっ た一方で，

18

世紀ま でに数学の世界はおおき な発展を 遂げて いた． さ ま ざま な驚く べき

“

定理

”

が発見さ れて ， 厳密な記述や厳密な 証明が問題になる よ う になっ て く る ．

直線上の点は「 互いに触れ合う

2

片の境界」 によ り 確定さ れ る

(

ア リ スト テレ ス

)

❀

切断によ る 実数の定義

(Dedekind, 1872)

❀

有理数のコ ーシー列によ る 実数の定義

(Cantor, 1883)

一方で， ア リ スト テレ ス流の論理学は， 数学で用いら れ る 高度な推論を 行う には不十分．

43/63

フ レ ーゲによ る 論理学の刷新

1884

年 『 算術の基礎』

1893

年 『 算術の基本法則』 第

1

巻

1903

年 『 算術の基本法則』 第

2

巻

「 論理に基づいてど こ ま で数学が展開でき る のだろ う か」

多く の革新的なア イ デア で現代の論理学の基礎を 構築

•

真理値

(

真と 偽

)

の導入

•

関数と 引数に分解し た命題の導入

•

論理変数と 量化子の導入

•

証明体系の導入

ア リ スト テレ ス論理学を 一般化

「 すべて の人は死ぬ．

ソ ク ラ テスは人である ．

従っ て ， ソ ク ラ テスは死ぬ．」

「

∀x (P x → Q x) ⇒ P a ⇒ Q a

」

当時の数学を 展開でき る 論理の体系を 与えたよ う に見え たが， そ の体系には矛盾がある こ と が判明

(

ラッ セルのパラ ド ッ ク ス

)

．

ア イ デア も 記法も 非常に難解であっ たため， そ の仕事は なかなか知ら れる こ と がなかっ た．

45/63

ゴッ ト ロープ・ フ レ ーゲ

(Gottlob Frege, 1848

−

1925)

(

画像はウ ィ キペディ ア よ り 引用

)

ラ ッ セルのパラ ド ッ ク ス

”Hardly anything more unfortunate can befall a scientific writer than to have one of the foundations of his edifice shaken after the work is finished. This was the position I was placed in by a letter of Mr. Bertrand Russell, just when the printing of this volume was nearing its completion.”

「 学問的著作に携わる も のにと っ て ．．．， 自ら の仕事を 完 遂し た後に， そ れが土台から 揺る がさ れる 事態に逢着する こ と ほど 望ま ら し から ぬこ と はない． こ の巻の印刷が終わ ろ う と し て いたそ のと き に， バート ラ ン ド ・ ラ ッ セル氏か ら 送ら れて き た手紙によ っ て 私が立たさ れる こ と になっ た のが， ま さ にそう し た状況であっ た．」

(

フ レ ーゲ，『 算術の基 本法則』 第

2

巻， あと がき

)

47/63

バート ラ ン ド ・ ラ ッ セル

(Bertrand Russel, 1872-1970)

(

画像はウ ィ キペディ ア よ り 引用

)

ラ ッ セルのパラ ド ッ ク ス ( 集合論バージョ ン )

集合は対象の集ま り ですが， 対象と し て集合そのも のを 考えてよ い．

こ のと き ， 普通， 集合そ のも のは， そ れ自体の要素にはなっ て いま せん． つま り ，

X ∈ X

は成立し て いま せん． けれど も ， 集合全部の集 合， など を 考える と ， 集合全部の集合は集合ですから ， それ自身の要素 になっ て いま す．

今，

A

と し て 自分自身を 含ま ない集合を 全部集めた集合を と り ま す．

つま り ，

A

と いう のは，

X / ∈ X

が成立し て いる よ う な

X

を 集めた集合 です． こ のと き ，

A ∈ A

か考えて みま す．

A ∈ A

と する と ， 集合

A

の定 義から ，

A / ∈ A

と なっ て いる はずで， こ れは矛盾ですから ，

A ∈ A

は 成立し て いま せん． 一方，

A / ∈ A

と する と ， 集合

A

の定義から ，

A

は集 合

A

に含ま れる はずです． つま り ，

A ∈ A

と なっ て し ま い， やはり 矛盾 なので，

A / ∈ A

も 成立し て いま せん． 従っ て ，

A ∈ A

でも

A / ∈ A

でも ないこ と になっ て し ま いま す

(

？

)

．

49/63

パラ ド ッ ク スの回避

自己言及的な構成を 許すこ と が問題 型の理論

(theory of types)

(Bertrand Russel, 1903)

個体を タ イ プ

0

と する ．

タ イ プ

0

の個体に対する 述語を タ イ プ

1

と する ． タ イ プ

1

の述語に対する 述語を タ イ プ

2

と する ．

...

プリ ン キピア ・ マテマティ カ

(Alfred North Whitehead and Bertrand Russell, 1910, 1912, and 1913)

「 数学で発展さ せら れた全て のア イ デア と 推論ステッ プ を 論理に基づいて 厳密に再現し よ う ． 」

フ レ ーゲのアイ デアと 仕事がこ れで知ら れる よ う になり ， 数学に大き なイ ン パク ト を 与える こ と になっ た．

51/63

短縮版の表紙

(

画像はウ ィ キペディ ア よ り 引用

)

プリ ン キピア の証明体系 ( 命題論理断片 )

公理：

(1) (P ∨ P ) → P (2) Q → (P ∨ Q)

(3) (P ∨ Q) → (Q ∨ P )

(4) (P ∨ (Q ∨ R)) → (Q ∨ (P ∨ R)) (5) (Q → R) → ((P ∨ Q) → (P ∨ R))

推論規則：

A → B A

B A

Aθ θ :

命題変数の具体化

“

公理から 推論規則を 繰り 返し 使っ て 得ら え る も のだけ が正し い命題

”

53/63

ヒ ルベルト の計画

フ レ ーゲ〜プリ ン キピア・ マテマティ カへの批判： 型の 理論に基づく ため， 従来行われて いたよ う な数学の証明が し づら い．

1904:

「 論理学と 算術の基礎」

(

国際数学者会議での講演

)

集合論や自然数論を 形式化し ， そ の無矛盾性を 証明すべ き ．

1.

プリ ン キピア の公理から 本当に矛盾が導かれないか？

2.

数学のど んな定理の証明にも 十分な証明体系は？

第一階述語論理

『 数理論理学の基礎』

(Hilbert and Ackermann, 1928)

第一階述語論理， 第二階述語論理，

...

と いう 形で， 述語論 理を 見通し よ く 整理．

公理：

(1) A → (B → A)

(2) (A → B ) → ((A → (B → C )) → (A → C )) (3) A → (B → (A ∧ B ))

(4) A ∧ B → A (4’) A ∧ B → B (5) A → A ∨ B (5’) B → A ∨ B

(6) (A → C ) → ((B → C ) → (A ∨ B → C ))

55/63

(7) (A → B ) → ((A → ¬B ) → ¬A) (8) ¬¬A → A

(9) A(t) → ∃xA(x) (10) ∀xA(x) → A(t)

推論規則：

A → B A B

A(a) → C

∃xA(x) → C

C → A(a) C → ∀xA(x)

ただし ，

a

は

C

に出現し ない．

Hilbert

の問題提起

•

証明体系の無矛盾問題．

(

ど う やっ て 体系から 矛盾が 導かれないと いう こ と が示せる のか？

)

•

証明体系の完全性問題．

(

正し い論理式は必ず証明体 系を つかっ て 示せる のだろ う か？

)

社会現象 自然現象 理論

数学

論理

57/63

理論 数学

論理

数学の理論は， 論理を 対象と する こ と も でき る ．

意味論 数学

論理

数学の理論は， 論理を 対象と する こ と も でき る ．

59/63

意味論と 構文論

意味論： 真理値表のア イ デア を 数学の概念を 使っ て 一般化．

「 真な論理式と は， すべての数学的なモデル上で成り 立 つ論理式のこ と である ．」

構文論： いろ いろ な推論形式が発明．

「 真な論理式と は， 論理的な推論に従っ て 導かれる 論理 式のこ と である ．」

意味論と 構文論における 真の概念は等価なのか？

「 意味論と 構文論は論理学の両輪」

第一階述語論理の完全性

ゲーデルの完全性定理

(Kurt, G¨ odel, 1930)

第一階述語論理の証明体系と 意味論が対応する ． 従っ て ， 第一階述語論理の証明体系は無矛盾．

61/63

ヒ ルベルト の計画のそ の後

「『 プリ ン キピア・ マテマティ カ』 やそ の関連体系での形 式的に決定不可能な命題について ，

I

」

(Kurt G¨ odel, 1931)

ゲーデルの

(

第一

)

不完全性定理

ペア ノ 算術を 含む再帰的な公理系は， 無矛盾なら ば，

不完全である ．

自然数の算術を 含むよ う な十分に強い体系では， 体系の 無矛盾性は示せない．

おわり に

歴史的には， 論理学は， 数学よ り ずっ と 遅れて 発明さ れ，

数学の言葉であり ， ルールである 論理を ， き ち んと 人類が 理解する よ う になる ま で，

2

千年以上も の年月が費さ れてい ま す．

こ の講義ではそ のエッ セン スを 紹介し ま す．

63/63