Does ¬ (A ↔ ¬ A) require classical?

Stream: general

[Martin C. Martin]

This is the last exercise in the propositional logic chapter in "Logic and Proof". It seems like it kind of assumes the law of the excluded middle, but I'm not entirely sure.

[Anne Baanen]

You don't need excluded middle here. Hint: first show that (A → ¬ A) implies ¬ A.

[Martin C. Martin]

Thanks! Somehow, I didn't think of proving a lemma. But it makes sense now.

[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.