日々の流転

λ. 数学基礎論講演会 「ゲーデルの不完全性定理」

講師

田中 一之 （東北大学大学院理学研究科数学専攻教授）

題目

ゲーデルの不完全性定理

内容

ゲーデルの定理はどこまで自己言及的か？ 本質的決定不能性と証明の加速性，新しい独立証明など，ゲーデル以降の発展のポイントを概観すると共に，この定理の誤用例など負の部分にも触れる．

6月にあった田中一之先生の講演「数学基礎論の考え方・学び方」の盛況を受けて第二弾が企画されていたので、参加してきた。 ゲーデルの不完全性定理なんて、いまさらなテーマのように思えたけど、後半のΣ無矛盾性やゴールドバッハ予想に関する話は「おおっ、そうなのか」と思った。

ゴールドバッハ予想はΠ₁文なので、無矛盾な体系でゴールドバッハ予想が証明できればそれは(標準モデルで)真。一方で、ゴールドバッハ予想の否定の証明から(標準モデルで)偽であることを導くには、Σ健全性が必要。 さらに、双子素数予想はΠ₂文なので、証明されたときにそれが真であることを主張するには、公理系にさらに強い要請が必要となる。

本質的決定不能性や加速定理についても、考えたことがなかった話なので、非常に新鮮だった。ヘンキン文とLöbの定理については、この日記でも以前に ヘンキン文 - ヒビルテ(2007-09-16) で少し取り上げたけど、Löbの定理の系として第二不完全性定理を導出できるというのも、気づいておらず「おおー」と思った。

主な参考文献として以下の3つが挙げられていた。

Feferman他編 Kurt Gödel Collected Works, Vol.1, Oxford University Press, 1986

<URL:http://books.google.co.jp/books?id=5ya4A0w62skC>

田中一之編 『ゲーデルと20世紀の論理学』 全4巻 東大出版会, 2006-7.

Torkel Franzén 著 (邦訳書来年出版) Gödel's Theorem: An Incomplete Guide to Its Use and Abuse, A K Peters, 2005.

<URL:http://books.google.co.jp/books?id=71pK8Zz9Dd8C>

なお、次回は2010年5月ごろに「不完全性定理　その後」というテーマで予定しているとのこと。「ランダムネスと不完全性定理」「クリプキの別証明」「パリス・ハーリントンの独立命題」ということで、また面白そうだ。

終了後に、かがみさんの紹介で igarisさんにお会いしたのだけど、僕はすぐに Real World Haskell 読書会の方に移動してしまったので、あまりお話できずに残念だった。 あと、下の写真は帰りにキャンパス内で見かけたもの。

関連

• 数学基礎論講演会〜ゲーデルの不完全性定理 (かがみさん)
• 数学基礎論講演会 - IgaBlogue - イガブロギュ

λ. Real World Haskell読書会 2009-10

前回の読書会が8月で、9月はお休みだったので2ヶ月ぶり。 前回、7章「入出力」の7.2「ファイルおよびハンドルを使う」まで読んでいたので、今日は多分7.3「規模の大きい例：関数的入出力と一時ファイル」から7章の残りと、8章「効率的なファイル処理、正規表現、ファイル名マッチング」。

• Chapter 7. Input and output (原著オンライン版)
• Chapter 8. Efficient file processing, regular expressions, and file name matching (原著オンライン版)

といっても、上記の講演会が終わってから移動したので、付いたときには既に8章の半ばまで進んでいて、最後の方しか参加できなかったのだけど(苦笑。

それから、Real World Haskell がついに出版ということで、オライリーの動物カレンダーつきで献本して頂いてしまった。 読書会には参加していたもののあまりフィードバック出来ていなかったので、ちょっと申し訳なくもあるのだけど、ありがとうございました。

以下いろいろ

末尾再帰的でない (++) :: [a] -> [a] -> [a] の定義が「なぜ問題ないのか?」「なぜ固定空間で評価できるのか?」について、個人的には違和感をまったく感じなくなってしまっていたのだけど、他の参加者にとってはそうでもなかったみたいだった。 それと、「このような形の関数に何か名前がなかったっけ?」という話があったが分からず。個人的に思い浮かぶのは「余帰納法(coinduction)」、「余再帰(corecursion)」、「anamorphism」とかだけど、これらは多分違うよなぁ……

System.FilePath が (</>) :: FilePath -> FilePath -> FilePath という演算子を提供していて、パスの連結を "foo" </> "bar" のように書けることに感心した。 これは記号の使い方がうまい。

それから、The Typeclassopedia 日本語訳 の話で盛り上がるなどしたが、私は未読なのでちょっと疎外感を感じるなどする(笑。それに関係してかどうかは分からないけど、Real World Haskell の16章「Parsecを使う」でなぜApplicativeを使うのかという話があった。 Real World Haskell って既存の便利な関数はできる限り使う主義みたい(たとえば、前回もArrowをちゃんと紹介せずにsecondだけ使ってみたりしてたし)なので、単に便利な関数として使っているだけではないかという気がする。

ただ、モナドはパーサーの記述には提供されている演算が強力すぎるので、パーサコンビネータの実装側としては、より制限された演算しか持たないApplicativeを抽象化として用いるのは、あり得る選択肢と思う。 John Hughes が Generalising Monads to Arrows でArrowを導入した際にも、モナドベースのパーサライブラリでは Swierstra and Duponcheel のテクニックが利用できないがArrowベースなら利用できるという例が挙げられていたので。

それから、Traversableについては The Essense of the Iterator Pattern がまとまった資料だと思う。