排中律やPeirce's lawの挙動 - chiguriの生態（嘘や誇張アリ）これは、Theorem Proving Advent Calendarの四日目の記事である。 ぱっと見ではあまりTheorem Provingらしくないかと思われるかもしれないが、たまにはこういう話もよいだろう、ということで。 お題 今回使う道具は、Curry-Howard同型対応、直観主義で失われる二重否定除去、そして栄光のcall/cc*1である。 ただ、これらの背景を説明すると滅茶苦茶に長くなるので、あとで解説用のスライドを作成しようと思う。 今回はこれらがわかっている前提で話を進める。 着眼点1：二重否定除去以外の規則群 直観主義論理と二重否定除去の組み合わせは古典論理と同じ計算能力を有する。 つまり、二重否定除去をつけると「直観主義論理で証明できなかったもの（のうち古典論理で正しいもの）が証明できる」こととなる。 また、同時にこれは逆が言える場合もあり、その規則を直観主義論理に付
