清水義夫『圏論による論理学』

昔、森毅が、その存在を指摘していた、Mac Lane が指摘した、論理学の現代版のようだ。
一般に、数学基礎論から、作られる、集合論は、どういう世界か？「はじめに一者あり」である。存在論的な形になっていて、その一者（実は、空）から、すべての存在が生成される。では、この Mac Lane が指摘した、論理学ではどうなるか。「はじめに働きあり」である。なんじゃそりゃ、と思うかもしれない。普通の集合論では、関数は、集合の一種（つまり、グラフ）として定義される。こちらは、逆に、関数から集合を定義しようということなのだ。
実は、この本を買ったんだけど、まだ読んでなくて、そういうことが書いてあるのかはまだよくわからない。あと、最近の、コンピュータ数学でも使われる、型付きの論理学を対象にしているようだ。

圏論による論理学―高階論理とトポス