12/02/04 20:53:10.81
>>492
Elementary topos は、確かにモデルに関して記述される場合が多いけれど、
object と morphism の２つの sort を持つ一階述語論理
（お好みなら identity を使って morphism だけの方法でもいいが）を考え、
identity と composition を関数記号として入れれば、
elementary topos であることを一階述語論理で記述できる。
元々 "elementary" という言葉は、
elementary extension, elementary submodel 等々、
一階述語論理の観点という意味合いを持つ。
トポスの重要な性質をすべて
（上述の言語による）一階述語論理で記述できた、
というのが elementary topos の意義。
公理系に関する研究がないじゃないか、というかも知れないが：
完全性があるのだから、
そうやって記述された elementary topos の公理系で何が証明できるか調べることと、
elementary topos に共通する("elementary" な)性質を調べることは同値。