excluded middle from dne

Stream: new members

[Manikhanta Teja]

I'm trying to prove A \/ not A using double negation elimination,

open classical
variable A : Prop
theorem dne ( h: not ( not A )) : A :=
by_contradiction
    (assume h1 : not A,
        show false, from h h1)
example : A ∨ ¬ A :=
have h1 : not ( not ( A ∨ not A), from
    assume hA : A,
    have h2 : A ∨ ¬ A, from or.inl hA,
    assume h3 : ¬ (A ∨ ¬ A),
    show false, from h3 h2
show A ∨ ¬ A,from dne (A ∨ not A) h1

I'm getting these errors

em.lean:8:34: error
invalid expression
em.lean:13:0: error
invalid 'have' declaration, ',' expected

I dont knwo whats wrong with this. Is this the right way to do this?

[Patrick Massot]

You should start with ensuring parentheses are balanced

[Manikhanta Teja]

Sorry. Balanced it but no change. i think i didnt prove this
have h1 : not ( not ( A ∨ not A), from

[Kevin Buzzard]

I have been using this software for a while now and I still look at code like this and find it incomprehensible. I know all this have, assume, from stuff is supposed to make it feel closer to English or whatever but for me it turns the code into spaghetti. @Manikhanta Teja have you tried using tactic mode and more structured code with {} in?

[Kevin Buzzard]

What does assume even do? How can I just randomly assume A in the middle of a proof of not ( not ( A ∨ not A))?

[Kevin Buzzard]

Whilst I am not an expert in this horrible mode, I conjecture that if you're trying to prove things, you can't just write random assumptions like assume hA : A in the middle of a proof.

[Manikhanta Teja]

@Kevin Buzzard I'm trying to understand how this working. I'm still a beginner. I'm sorry.

[Kevin Buzzard]

Are you reading TPIL?

[Kevin Buzzard]

They start with this horrible mode

[Kevin Buzzard]

I would probably have given up Lean there and then were it not for the fact that I had read a Coq tutorial that went straight into tactic mode

[Manikhanta Teja]

Yeah i started with TPIL.

[Kevin Buzzard]

I teach a lot of beginners how to use Lean, and for a question like this I would always start with the following template:

example : A ∨ ¬ A :=
begin
  sorry
end

[Kevin Buzzard]

Here is a crazy suggestion: just stop what you're doing, go straight to chapter 5, and read a bit about doing basic logic in tactic mode.

[Kevin Buzzard]

The absolutely massive advantage of tactic mode for beginners is that at all times you can see exactly what you have already proved, and what you are trying to prove.

[Manikhanta Teja]

Starting chapter 5 now. Thanks.

[Andrew Ashworth]

What does assume even do? How can I just randomly assume A in the middle of a proof of not ( not ( A ∨ not A))?

assume is just notation for λ

[Kevin Buzzard]

So that answers the question of why the original code didn't compile -- the assume ha : A looks invalid because it would only work for goals of the form A -> <something>

[Manikhanta Teja]

open classical
variable A : Prop
theorem dne ( h: not ( not A )) : A :=
by_contradiction
    (assume h1 : not A,
        show false, from h h1)
example : A ∨ ¬ A :=
have hN : not ( not ( A ∨ not A), from
    (assume h1 :  ¬ (A ∨ ¬ A),
        have h2 : ¬ A, from
            assume h3 : A,
            have h4 : A ∨ ¬ A, from or.inl h3,
            show false, from h1 h4,
        have h5 : A ∨ ¬ A, from or.inr h2,
        show false, from h1 h5)
show A ∨ ¬ A,from dne(A ∨ not A) hN

em.lean:8:34: error
invalid expression
em.lean:17:0: error
invalid 'have' declaration, ',' expected

This is what i was trying to do. Get ¬¬(A ∨ ¬A) → A ∨ ¬A from dne( A \/ not A) and then apply implication elimination of ¬¬(A ∨ ¬A) → A ∨ ¬A to get A ∨ ¬A.
The proof for ¬¬(A ∨ ¬A) worked

variable A : Prop
theorem cc : ¬ (¬ ( A ∨ ¬ A)) :=
(assume h1 :  ¬ (A ∨ ¬ A),
    have h2 : ¬ A, from
        assume h3 : A,
        have h4 : A ∨ ¬ A, from or.inl h3,
        show false, from h1 h4,
    have h5 : A ∨ ¬ A, from or.inr h2,
    show false, from h1 h5)

Is there anything wrong with this
show A ∨ ¬ A,from dne(A ∨ not A) hN

[Kevin Buzzard]

The error seems to indicate you've got the syntax wrong somewhere.

[Chris Hughes]

There's a missing comma after show false, from h1 h5)

[Manikhanta Teja]

Still have a problem with
em.lean:8:34: error invalid expression

[Manikhanta Teja]

Got it. I'm an idiot. I didn't balance the paranthesis.

[Kevin Buzzard]

If you were to use tactic mode you would have none of these problems and the errors would be far less obscure

[Kevin Buzzard]

Tactic mode forces you to structure your proofs properly

[Don Burgess]

I have worked up some exercises related to the Excluded Middle (EM). Please correct my wording or expand on my thoughts. Let me know if possibly these notes would be useful for a novice or where I could post them.
Thanks for your time.

Is the EM essentially confined to a Boolean-like system?

In the context of a Boolean system are the Excluded Middle(EM) and Double Negative (DNE) Principles logically equivalent?
DNE <-> EM

/- A set of Exercises related to the Excluded Middle (EM)-/
variable (P Q : Prop)

/-If (P OR Q) is False, then both P AND Q must be False: OR TT -/
example : ¬ (P ∨ Q) -> ¬P ∧ ¬Q :=
  fun h =>
    have np := fun p => h (.inl p) /- P -> False -/
    have nq := fun q => h (.inr q) /- Q -> False -/
    ⟨ np, nq ⟩

/- Similarly, the negative of the EM implies that both P and ¬P
   are False : which is contradictory. Therefore the negative
   of the negative of the EM is True. -/

theorem negnegEM :¬ (¬(P ∨ ¬P )) :=
  fun nem =>                          /- nem: ¬(P ∨ ¬P ) -/
    have np := fun p => nem (.inl p)  /- P -> False -/
    have nnp := fun np => nem (.inr np) /- ¬P -> False -/
    absurd np nnp /- ¬P and ¬(¬P) are contradictory => ¬¬ EM  -/

open Classical

/- The Double Negation Theorem requires the EM : (P ∨ ¬ P)-/
theorem DNE : ¬¬P -> P :=
  fun nnp =>
  Or.elim (em P)   /- P must be True or False -/
    (fun p  => p) /- We are done -/
    (fun np => absurd np nnp) /- ¬P and ¬(¬P) are contradictory
                               So P cannot be False -/

/- On the other hand, given DNE we can easily prove the EM -/

theorem EM  : (P ∨ ¬P ) :=
  have nnEM := negnegEM P
  DNE (P ∨¬ P) nnEM /- By DNE the double negation of EM
                       implies EM -/

[Richard Copley]

You proved that EM and DNE are equivalent, in the logic of Lean4. (This is (also) a theorem of intuitionistic logic.) It might be clearer to prove it without axioms. For example (this is your proof again, but overly golfed),

theorem em_iff_dne : (∀ (p : Prop), p ∨ ¬p) ↔ (∀ (p : Prop), ¬¬p → p) := ⟨
    fun hem p hnnp => Or.elim (hem p) id (fun hnp => absurd hnp hnnp),
    fun hdne _ => hdne _ (fun hnem => absurd (hnem ∘ Or.inl) (hnem ∘ Or.inr))⟩

#print axioms em_iff_dne -- 'em_iff_dne' does not depend on any axioms

The proof uses the principle that anything follows from a contradiction, so it doesn't go through in a paraconsistent logic. That might be interesting to think about, but it's hard to reason about it in Lean because that principle is built in.

Another interesting equivalence (in intuitionistic logic) is between Weak Excluded Middle and De Morgan's Law. You can prove all of these without axioms in Lean:

theorem deMorgan1 {p q : Prop} : (¬p ∨ ¬q) → ¬(p ∧ q) := sorry
theorem deMorgan2 {p q : Prop} : (¬p ∧ ¬q) → ¬(p ∨ q) := sorry
theorem deMorgan3 {p q : Prop} : ¬(p ∨ q) → (¬p ∧ ¬q) := sorry

-- Double negation preserves conjunction
theorem not_not_and {p q : Prop} : ¬¬p → ¬¬q → ¬¬(p ∧ q) := sorry

-- De Morgan's Law is equivalent to weak excluded middle
theorem deMorgan_iff_wem :
  (∀ (p q : Prop), ¬(p ∧ q) → (¬p ∨ ¬q)) ↔ (∀ (p : Prop), ¬p ∨ ¬¬p) := sorry

Here are some more exercises that can be proved without axioms.

-- (1) Constructively, ¬(p ↔ q) is equivalent to (¬p → ¬¬q) ∧ (q → ¬p).
-- (2) Constructively, ¬p ↔ q implies ¬(p ↔ q).
-- (3) The classical theorem ¬(p ↔ q) → (¬p ↔ q) is equivalent to dne.
theorem part1 {p q : Prop} : ¬(p ↔ q) ↔ (¬p → ¬¬q) ∧ (q → ¬p) := sorry
theorem part2 {p q : Prop} : (¬p ↔ q) → ¬(p ↔ q) := sorry
theorem part3 : (∀ p q : Prop, ¬(p ↔ q) → (¬p ↔ q)) ↔ (∀ p : Prop, ¬¬p → p) := sorry

I don't know about any systematic study of this sort of thing, but I haven't searched very hard for one!

[Yaël Dillies]

A good reference I like is the first chapter of Borceux volume 3.

[Don Burgess]

Thanks for your feedback.

@Buster

Thank you for your time.

Would you give some explanation to the CIRC operator you use in your proof of "em_iff_dne"?

How do I apply a theorem to a process inside a negation? I would like to apply De Morgan 1 to

¬(¬p ∨ ¬q)

to obtain

¬¬(p ∨ q)

in order to prove "not_not_and".

theorem deMorgan1 {p q : Prop} : (¬p ∨ ¬q) → ¬(p ∧ q) :=
  fun h1 h2 =>
  Or.elim h1
    (fun np => absurd h2.left np)   /- ¬P -> False -/
    (fun nq => absurd h2.right nq)  /- ¬Q -> False -/

/- If (¬p ∨ ¬q) is True then at least one of p,q is False which makes (p ∧ q) False
   and ¬(p ∧ q) True -/

theorem deMorgan2 {p q : Prop} : (¬p ∧ ¬q) → ¬(p ∨ q) :=
  fun hAnd hOr =>
    Or.elim (hOr)
      (fun p => absurd p hAnd.left)
      (fun q => absurd q hAnd.right)
/- If (¬p ∧ ¬q) is True, then both p,q are False
  which makes (p ∨ q) False and ¬(p ∨ q) True. -/

-- Double negation preserves conjunction
theorem not_not_and {p q : Prop} : ¬¬p → ¬¬q → ¬¬(p ∧ q) :=
  fun nnp nnq h =>                                      /- h: ¬(p ∧ q) -/
    have nh1 := deMorgan2 ⟨ nnp,nnq ⟩                 /- nh1: ¬(¬p ∨ ¬q) -/
    /- deMorgan1 applied to nh1 yields ¬¬(p ∨ q) -/

[Richard Copley]

The circle is function composition: hnem ∘ Or.inl is the same function as fun p => (hnem ∘ Or.inl) p, which is the same as fun p => hnem (Or.inl p), which you'll recognise from your own proof.

deMorgan1 goes in the wrong direction for you to apply it there. You have as hypotheses implications of the form nh1: (¬p ∨ ¬q) → A and deMorgan1: (¬p ∨ ¬q) → B ; you can't apply either of them since you don't have ¬p ∧ ¬q [Edit:] Those two implications don't chain together in the way you seem to want, if I understand correctly.

The proof of not_not_and is tricky.

Spoiler 1

From your hypotheses ¬¬q and ¬(p ∧ q), you can prove ¬p.

Spoiler 2

From the hypotheses ¬(p ∧ q) and p, you can prove ¬q.

[Richard Copley]

@Don Burgess, ok? Please ask if not.

[Don Burgess]

Buster said:

Don Burgess, ok? Please ask if not.

Thanks for your hints :)

theorem nnp_nAnd_nq {p q : Prop} :¬¬p -> ¬(p ∧ q) → ¬q  :=
  fun nnp h hq =>
    have np := fun hp => h ⟨ hp,hq ⟩
    absurd np nnp

-- Double negation preserves conjunction
theorem not_not_and {p q : Prop} : ¬¬p → ¬¬q → ¬¬(p ∧ q) :=
  fun nnp nnq h =>                                      /- h: ¬(p ∧ q) -/
    have nq := nnp_nAnd_nq nnp h
    have h1 := Or.intro_right (¬p) nq
    have nh1 := deMorgan2 ⟨ nnp,nnq ⟩                 /- nh1: ¬(¬p ∨ ¬q) -/
    absurd h1 nh1

In principle I think you should be able to prove "not_not_and" using De Morgan 1:

/- ¬(¬p) ∧ ¬(¬q) = ¬ (¬ p ∨ ¬q) by De Morgan 2
  ¬(¬ p ∨ ¬q) = ¬ ¬ (p ∧ q) by De Morgan 1  -/

But I do not know how to apply a theorem inside a NOT.

[Richard Copley]

You cannot deduce ¬q from p → q and ¬p.

example : ¬∀ {p q : Prop}, (p → q) → ¬p → ¬q := fun h => h False.elim not_false trivial

You can deduce ¬q from q → p and ¬p.

example {p q : Prop} : (q → p) → ¬p → ¬q := fun h hnp hq => hnp (h hq)

So it is "deMorgan4" that you would need there, not deMorgan1.

theorem deMorgan4 {p q : Prop} : ¬(p ∧ q) → (¬p ∨ ¬q) := sorry

theorem not_not_and' {p q : Prop} : ¬¬p → ¬¬q → ¬¬(p ∧ q) :=
  fun hnnp hnnq =>
    have h : ¬(¬p ∨ ¬q) := deMorgan2 ⟨hnnp, hnnq⟩
    mt deMorgan4 h

But deMorgan4 is not a theorem of intuitionistic logic. (You can use not_not_and to prove deMorgan_iff_wem.)