本日の授業で

最小命題論理（直観主義論理から矛盾律を除去した体系）で、¬¬¬ A⇒¬ AとA⇒¬¬ Aは証明できるが、¬¬A⇒ Aは証明できない、と言う話をしたんですよ*1。授業終了後、一人の学生がやってきて、「証明できない理由の説明が曖昧だったんですが、最小論理にはタブローとかないんですか」って聞いてきたんです。話を聞くと、春休みに「論理学をつくる」を100ページ勉強したんだそうで。今年の授業は、熱心な学生さんが多いです。

*1:最小論理は、証明できる論理式を証明するのは簡単だけれど、ある論理式が証明できないことを示すのは難しい