Zulip Chat Archive

Stream: new members

Topic: Does ¬ (A ↔ ¬ A) require classical?

Patrick Stevens (Dec 14 2021 at 12:03):

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 (Dec 14 2021 at 13:33):

Note there's another thread on this here

David Wärn (Dec 14 2021 at 14:01):

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

Last updated: Dec 20 2023 at 11:08 UTC