2008-04-01 [長年日記]
λ. 『圏論による論理学—高階論理とトポス』 清水 義夫
貸してもらったので、ざっと読んだ。 トポスに関しては元々あまり知らなかったこともあり勉強になったが、哲学的な話は正直よくわからなかった。
第一章 関数型高階論理
関数型高階論理 λ-h.o.l. の 定義は、プリミティブを少なくするために工夫している部分以外は普通。 λ-h.o.l は、型の一つとして真理値の型 t を持ち、命題はこの型を持つような項(≠型)であるような論理。 この論理だと命題それ自体は型にならないので、型理論からカリーハワード同型対応で得られる高階論理とは流儀が違う感じ(?)。 そういえば、「言語の意味論」の授業でモンタギュー文法とPTQをやったときに使った内包論理ILもこんな感じの高階論理だった(c.f. 言語の意味論(2006))。
と思ったら、簡易モンタギュー文法の話が出てきた。モンタギュー文法についてもう少し詳しい話を知りたい人は前述の「言語の意味論」の講義資料と、中村さんのノート「UG とPTQ の概要」とを読むと良いと思う。
第二章 トポス
圏論の諸概念とトポスを定義して λ-h.o.l. をトポスで解釈する。
トポスで解釈するといっても任意のトポスではなく、集合圏のトポスでの解釈。 なんだ、一般のトポスで解釈するんじゃないのね。 まあ、第一章で λ-h.o.l. は古典論理として定義されているので、任意のトポスで解釈することは出来ないのは当然だけど……λ-h.o.l.はなんでわざわざ古典論理にしたのかな。
ラムダ式に対する解釈の定義は、あまりフォーマルな定義にはなっていないが言いたいことは分かる。 ただ、論理記号 T, F, ¬, ∧ は略記法として導入していたので、それに対して明示的に定義を与えているのは変。 まあ、略記法に基づいて解釈しても同じものになるはずだけど。
それから、第一章で導入していた λ-h.o.l. の拡張には、確定記述(definite description)と自然数があったが、自然数しかトポスで解釈していないのは何故だろう。 (追記: 確定記述(definite description) - ヒビルテ (2008-04-03)で少し書いたが、確定記述の解釈にはコンテキストないしは継続のような概念が必要になるが、トポスにはそれらに直接対応する概念はないので、直接の翻訳は出来なくて当たり前。)
あと、λh.o.l. の集合圏のトポスでの解釈の健全性を証明していながら、完全性については全く触れていないのはちょっと拍子抜け。 トポスが「われわれの知性にとって普遍性かつ基底的な事態に根ざす言語」であることから、λ-h.o.l.が「われわれの知性にとって普遍性かつ基底的な事態」に係わっていることを主張するためには、単に解釈可能というだけでなく、完全性などのより強い性質を示さなくて良いのだろうか。 トポスはリッチな構造を持っている分、λ-h.o.l. に限らずいろんなものを解釈可能なわけで……
それから、トポスの定義で「始対象」「直和」「プッシュアウト」の存在条件が不要であることについては、証明はややこしいとかではぶかれていたが、どうやるんだろう。 トポスはよく知らないので、すぐにはわからなかった。 後でやってみる。
第三章 トポスの基本定理
著者がトポスの基本定理と呼ぶ以下の定理の証明。
E をトポスとし， B を E の任意の対象とする．このとき， E↓B もトポスである。
また A も E の任意の対象とし、f : A→B を E の矢とするとき、 E↓A と E↓B の間には， f* : E↓B → E↓A および ∑f : E↓A → E↓B, ∏f : E↓A → E↓B なる関手 f*, ∑f, ∏f が存在し，∑f ⊣ f* ⊣ ∏f が成立する。
この本では Locally Cartesian Closed Category (LCCC) については言及されていないが、これは E↓B に subobject classifier が存在することと、E が LCCC であることとを示すことと同じ。
第四章 プルバック関手f*の右-随伴関手∏f
前章で一般的に証明していなかった部分のきちんとした証明。 結構面倒くさい。以前にrpfさんから elementary topos は LCCC になっていると聞いていたけど、そのときはこんなに面倒くさいとは思わなかったよ。
partial arrow classifier と singleton の概念をはじめて知った。 面白い。
この章が一番勉強になった。
第五章 リミット、空間性トポス、限量記号
.
結び
「多少比喩的にいえば」と断ってはあったものの、対象でトポスをスライスすることが何故「視座」を設定することになるのか分からなかった。 というか、ここで言っている「視座」が何なのか分からなかった。 LCCCによる型理論の解釈(c.f. On the Interpretation of Type Theory in Locally Cartesian Closed Categories)の場合だと、コンテキストに対応するので理解できないこともないのだけど。
他にも、哲学的なことに関しては、「示された」と書かれていることで、何故言えるのか論理を追うことが出来なかった部分が多い。
関連
- はてなダイアリー - 「圏論による論理学—高階論理とトポス」を含む日記
- lambda high order logic - 白のカピバラの逆極限 S144-3
- nucさんによると結構酷い間違いもあったみたいだけど、すごい勢いで斜め読みしてたので気づかなかった……
