＞「第二不完全性定理」（その公理系の中に矛盾があっても、その公理系の中では「矛盾がある」ということが証明できない）
ちょっと違うのでは？
「その公理系の中に矛盾ないとき、『その公理系の中では矛盾がない』ということを、その公理系では証明できない」
＞「二重否定の除去」は、直観論理では認められていないんですよ。すなわち、「¬¬A ≡ A」は成立しないんです。
厳密ではないですね
二重否定の除去は、「排中律」＋「矛盾の公理：矛盾から任意の命題を導くことができる」のダブルパンチの威力があります
直観主義論理は、「排中律」を公理として含みませんが、「矛盾の公理」は含んでいます
