Do I need classical logic for this proof?

Stream: general

[Dominic Farolino]

Hello. There exists a section in 4.4, from the "Theorem Proving in Lean" book that contains a bunch of common identities, involving the existential quantifier. I'm working through solving all of them, and I've solved example: (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) := using classical logic (by_contradiction specifically). I'm wondering if it is possible to get away with a proof that does not require classical logic here? My proof is as follows:

example: (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) :=
  iff.intro
    (assume h: (∀ x, p x),
      show ¬ (∃ x, ¬ p x), from
      assume hpos: (∃ x, ¬ p x),
      show false, from
      exists.elim hpos
        (assume y: α,
          assume hinner: ¬ p y,
          show false, from hinner (h y)
        )
    )
    (assume h: ¬ (∃ x, ¬ p x),
      show (∀ x, p x), from
      assume x: α,
      show p x, from
      by_contradiction
        (assume h1: ¬ p x,
          have hpos: ∃ x, ¬ p x, from exists.intro x h1,
          show false, from h hpos
        )
    )

[Chris Hughes]

It's not possible without classical logic.

example : (∀ {α : Type} {p : α → Prop}, (∀ x, p x) ↔ ¬ ∃ x, ¬ p x) → ∀ (P : Prop), P ∨ ¬ P :=
λ h P, (@h unit (λ _, P ∨ ¬ P)).2 (λ ⟨_, h⟩, h (or.inr (h ∘ or.inl))) ()

[Chris Hughes]

More or less, the reason is that the right hand direction is a proof of double negation. ¬¬p - > p

[Dominic Farolino]

@Christopher Hughes Ok that makes sense, thank you very much!

[Kevin Buzzard]

I don't know of any example of a question of the form "show that this statement which is true in classical logic cannot be shown in constructive logic" which cannot be answered by showing that the law of the excluded middle is implied by the statement. Is this a general principle or are there classically true statements which are unprovable in constructive logic and yet do not constructively imply LEM?

[Mario Carneiro]

there are intermediate statements

[Mario Carneiro]

an example is not not p \/ not p

[Mario Carneiro]

wikipedia has a whole zoo of them: https://en.wikipedia.org/wiki/Intermediate_logic

[matt rice]

I have trouble thinking classically, but there is this constructive derivation of one of the demorgan's, which isn't constructively derivable without additional assumptions, but which can then be derived using excluded middle, or A ∨ B
giving a weird half classical/half constructive proof... :shrug:

def something {A B : Prop} (h : ¬(A ∧ B)) : (A -> ¬ B) ∧ (B -> ¬ A) :=
    and.intro (λ a, (λ b, h (and.intro a b))) (λ b, (λ a, h (and.intro a b)))

def demorgans {A B : Prop} (lem : A ∨ ¬A) (nab : ¬(A ∧ B)) : ¬A ∨ ¬B :=
  or.elim lem
    (λ a, or.inr (λ b, (nab ⟨a, b⟩)))
    (λ na, or.inl (λ a, na a))

def weird_demorgans {A B : Prop} (a_or_b : A ∨ B) (nab : ¬(A ∧ B)) : ¬A ∨ ¬B :=
   or.elim a_or_b
    (λ a, or.inr ((something nab).left a))
    (λ b, or.inl ((something nab).right b))

def foo {A B : Prop} : ((A ∨ B) ∨ (A ∨ ¬A)) → ¬(A ∧ B) → ¬A ∨ ¬B
:= (λ foo, or.elim foo (λ ab, weird_demorgans ab) (λ lem, demorgans lem))