先ほどの記事、12-03という日付になっているが、一応日付が変わってから公開している。 これははてなダイアリーの仕様*1なので、私に言われても困る。 *1:もちろん設定で変更可能、今はデフォルトの午前6時日付変更になっている。

これは、Theorem Proving Advent Calendarの四日目の記事である。 ぱっと見ではあまりTheorem Provingらしくないかと思われるかもしれないが、たまにはこういう話もよいだろう、ということで。 お題 今回使う道具は、Curry-Howard同型対応、直観主義で失われ…