lambda higher order logic

「圏論による論理学　高階論理とトポス」を読んだ。
lambda の = という概念が primitive に入っているがそれが強力すぎるのが気にかかる。
Bool 演算が自然に構築できるとして
T := (\x -> x = \x -> x)
F := (\x -> x = \x -> T)
として話をするのだが。
うーん、なんていうかそれってそんだけ強力な道具立てがあれば、まあ、当然みたいな。

あと、Hom({},{*}) を誤解している。仮想的な元を考えてってところは色々とありえない。
subobject classifier のところもおかしい。

…数学者の書いた文章を読む気になった。

非常に面白かったけれども、数学的には穴があったってところです。
でも、哲学者全体に一般化しないだけの経験(おい)を積んだ気がする。