>>153
論理学の一派に直観論理という流儀というか枠があります。
>>150, >>152 は直観論理の枠内に沿って記述しているのです
通常の記号論理では A∨¬A (排中律）を仮定しますが、直観論理の枠の中ではこの仮定を認めません
A∨¬A　 (排中律）の仮定がなければ¬¬A = A (二重否定の除去）も証明できません

ただ、なぜ直観論理主義者がどうして排中律を排除したのか、その理由については、私にもよくわかりません…