直観主義論理というのは実無限、選択公理に対する疑念がその起源だったはず。
排中律が実無限に拠っているということでその論理式であるp∨¬pをそれより弱い主張の(p→q)∧(p→¬q)→¬pに替えて使うのがハイティンクの直観主義的命題算。
その命題算はこれと残りの古典論理から導かれる。
¬¬p→pというのはヒルベルト＝ベルナイスが示した公理系にある恒真式の一つ。