Does ¬ (A ↔ ¬ A) require classical?

Stream: new members

[Patrick Stevens]

As a rule of thumb, proving a negation is somehow less likely to require classical than proving a positive statement (e.g. "¬¬p implies p" requires classical, though "¬¬¬p implies ¬p" does not). The "content" of classical is that removing negations is hard.

[Eric Wieser]

Note there's another thread on this here

[David Wärn]

Patrick's remark can be made precise. Whenever you can derive a contradiction using some instance of LEM you can derive one also without it. This is because ¬¬(p ∨ ¬p) holds constructively. Here's an illustration in Lean:

lemma lem_is_not_false (p : Prop) : ¬¬(p ∨ ¬p) :=
λ h, h (or.inr $ λ hp, h (or.inl hp))

lemma eliminate_lem (p q : Prop) (h : (q ∨ ¬q) → ¬p) : ¬p :=
λ hp, lem_is_not_false q $ λ hq, h hq hp