Internal Language の続き

いや、論文書きとかいろいろやってたはずなんだけど? そんなにがんばってないんだが、

　　Topos から集合が入ってる直観主義論理(Internal Language)を構築する

ってなお題で、まぁ、そこそこできた。なのだが、

　　(p ⊢ q) → (q ⊢ p) → p ≈ q

と書いてある。論理的にはあんまり使わない式ですね。

4/27くらいからはまったんですが、どうも、できそうにない。Lambek には

　　p ⊢ q は p ⊆ q のことだから、kernel (ker h) が等しい
　　なので char (ker h) ≈ h から出る

とか書いてあって、ちっとも圏論でやってない。Sets でやると瞬殺ででる。だからさ〜

　　集合論作ってる最中だから、ここで集合的なイメージを使うのはだめだろ?

結果的には、Topos の char の uniqueness を拡張してできたんですが、
ちょっと強力すぎる気もする。でも、こうすると、char の cong とかもできるので便りであるな。

ま、良いということにしよう。残りを片付けるかどうかは気分次第かな。他にもいろいろ中途半端に停めてるし。

いや、この手のものには終わりはないんだよ。