「技術者／プログラマのためのラムダ計算、論理、圏」セミナー

昨日、行ってきました。

• こういう話（カリー・ハワード対応がどうとか）を聞く機会はあまりないので、とても楽しめました。
• いよいよラムダというところで、時間切れに。→次回も参加します。
• 7 時までに帰る約束だったので、終わった後の食事会に行けず。→次回は参加します。

関係ないですが、檜山さんの記事を読み返していて、辿り着いた記事。
あなたにも（たぶん）わかる「ゲーデルの不完全性定理」 発端＜ほったん＞編

ゲーデルの不完全性定理を、自然言語（日常言語）だけで説明する試みを見かけるのだけど、これは無理スジじゃなかろうか。前もってわかっている人は、「あー、そうだね、確かに」と納得できるだろうが、その自然言語による説明により初めて勉強をする（そして、ちゃんと理解する）ってのはほぼ不可能な気がする。

一見回り道のようでも、記号論理学を一通り勉強して、ゲーデル符号化を（だいたいでも）追いかけないと、納得した気分にはなれないだろう。仮に正確な説明だったとしても（そうじゃない例も見かける）、それが自然言語で記述されると、なんだか騙されたような印象をぬぐいきれない。

そうそう、腑に落ちないんです。
という訳でまぁ、色々（↓）読んだりしてるのですが、こちらの記事「プログラマのための「ゲーデルの不完全性定理」」も再開を希望しま〜す。

形式論理学―その展望と限界