>>62
古典論理では認められてるんですが、「二重否定の除去」は、
直観論理では認められていないんですよ。すなわち、
「¬¬A ≡ A」は成立しないんです。
このあたりは、クルト・ゲーデルというひとが、
「完全性定理」（無矛盾な公理系があって、
その中では「正しいことは、すべてその体系の中で
証明できる」）とか「第一不完全性定理」（その公理系の
中で記述された命題のうち、「正しいんだけど証明できない
命題」があっても矛盾しない）とか「第二不完全性定理」
（その公理系の中に矛盾があっても、その公理系の中では
「矛盾がある」ということが証明できない）とかいうことを、
「ゲーデル数」という概念を使って証明しちゃったんで、
このあたりの話は、けっこう活発に議論されているテーマ
なんです。
「数学基礎論」とか「連続体仮説」とか「選択公理」とかについて
勉強してみると、けっこう面白いですよ？