継続の圏 続き

前回の日記のあと、さかいさんから個人的に指摘もらいました。「この圏はCCCじゃないんじゃないか」と。

CCCに対応するのは直観主義論理なのですが、一方で継続 ~X が Xの双対なら、~~X が X と同型になりそうなのです。つまり、~X を「Xの否定」とみなすと、排中律が成り立っちゃうかもしれないと。

ありゃー、一から考え直さないといかんかなー。