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

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

青戸 等人

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

目次

-

はじ めに 〜論理と は〜

-

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

はじ めに

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

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

1/63

はじ めに

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

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

数理論理学の基本的な知識(と 技)を学べば， こ れが(だい ぶ?)わかる よ う になり ま す． 証明の書き 方がわかれば， 証 明の読み方がわかり ま す． 証明の読み方がわかれば， 理論 への扉が開き ま す．

理論がわかれば， 理論と 実験的結果と の差分も 掴める よ う になる でし ょ う ． こ れは情報工学/情報科学を 専門にする 人にと っ て はと て も 大き いはずです．

数理論理学と は

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

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

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

(数理論理学以外も 含めた)

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

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

2/63

+---+

| "理論" | +----+---+----+

|

数学  

|

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

|

数理論理学  

|

---+---+---

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

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

(ある いは， “数学”

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

etc.)，

数学を き ち んと 使いこ なすには， 数学 の基礎と なる数理論理学(論理的な推論の理解と やり 方， 数 学の仕組み・ 証明の仕方)を 身につける 必要がある．

3/63

論理的な推論と は

•

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

•

絶対確実な推論のみ

•

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

4/63

論理的な推論と は

論理的な推論の例：

「 すべて の人は死ぬ．

ソ ク ラ テスは人である ． 従っ て ， ソ ク ラ テスは死ぬ．」

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

ペン ギン は鳥である ．

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

“従っ て ”と いう 2つの前提から 1

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

論理的な推論と は

こ れら の推論はど れも

「 すべて の

Xは Yである ． a

は

X

である ．

従っ て ，

a

は

Y

である ．」

のよ う な一般形を も つ．

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

6/63

初等教育における 論理

数学教育の2側面： 計算力と証明力

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

こ の

2

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

(子供は規則が大好き (?))． 証明力はある 程度の年

齢から

(自分自身に問い掛ける 態度が必要(?))．

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

7/63

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

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

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

つの三 角形は合同」

9/63

推論ステッ プを

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つ辿る こ と で示せる ．

11/63

論理は数学のルール

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

•

ど こ で間違えたか，

•

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

•

ど の定義が曖昧か，

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

12/63

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

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

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

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

13/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

目次

-

はじ めに 〜論理と は〜

-

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

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

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

17/63

Venn Diagrams ベン 図

(Venn, 1881)

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

A

18/63

Venn Diagrams ベン 図

B

A と B の積 ( 共通部分 )

A ∩ B

20/63

A と B の和 ( 合併 )

A ∪ B

21/63

A の反転

A

^◦

22/63

B の反転

B

^◦

23/63

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

(A ∪ B)

^◦

= A

^◦

∩ B

^◦

24/63

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

(A ∩ B)

^◦

= A

^◦

∪ B

^◦

25/63

部分集合 (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

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

27/63

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」

も 導入でき る _29/63

真理値表

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

33/63

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

前の推論(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

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

36/63

ジョ ージ・ ブール

(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

38/63

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

40/63

2 つの方法論 1.

真理値にも と づく 方法

真と 偽と いう 命題の

“意味”

を 考える

「 意味論」

2.

等式によ る 導出

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

「 構文論」

まっ たく 異なる

2つの方法だが， こ の 2つの方法は同値に

なる

(「 完全性 」 )

41/63

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

(Emil Leon Post, 1897-1954) (画像はウ ィ キペディ ア よ り 引用)

42/63

数学の厳密化

論理学が

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

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

“定理”が発見さ れて ， 厳密な記述や厳密な

証明が問題になる よ う になっ て く る ．

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

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

る

(ア リ スト テレ ス)

❀

切断によ る 実数の定義

(Dedekind, 1872)

❀

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

(Cantor, 1883)

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

43/63

フ レ ーゲによ る 論理学の刷新 1884年 『 算術の基礎』

1893年 『 算術の基本法則』 第1巻 1903年 『 算術の基本法則』 第2巻

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

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

•

真理値(真と 偽)の導入

•

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

•

論理変数と 量化子の導入

•

証明体系の導入

44/63

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

「 すべて の人は死ぬ．

ソ ク ラ テスは人である ． 従っ て ， ソ ク ラ テスは死ぬ．」

「

∀ 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) (画像はウ ィ キペディ ア よ り 引用)

48/63

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

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

こ のと き ， 普通， 集合そ のも のは， そ れ自体の要素にはなっ て いま せん． つま り ， 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

短縮版の表紙

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

52/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.

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

54/63

第一階述語論理

『 数理論理学の基礎』

(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

の問題提起

•

証明体系の無矛盾問題．

(ど う やっ て 体系から 矛盾が

導かれないと いう こ と が示せる のか？

)

•

証明体系の完全性問題．

(正し い論理式は必ず証明体

系を つかっ て 示せる のだろ う か？

)

56/63

社会現象 自然現象

理論

数学

論理

57/63

理論 数学

論理

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

58/63

意味論

数学

論理

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

59/63

意味論と 構文論

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

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

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

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

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

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

60/63

第一階述語論理の完全性

ゲーデルの完全性定理(Kurt, G¨

odel, 1930)

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

61/63

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

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

I」 (Kurt G¨ odel, 1931)

ゲーデルの

(第一)

不完全性定理

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

不完全である ．

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

62/63

おわり に

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

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

2千年以上も の年月が費さ れてい

ま す．

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

63/63