How to prove (¬ (∀ x, P x)) → (∃ y, ¬ (P y)) in Lean

Stream: new members

[elliott smith]

here is the natural deduction

        P a
  ------------- ∀ I
    (∀ x, P x)       ¬ (∀ x, P x)
----------------------------------- ¬ E
                ⊥
            --------- ¬ I
              ¬ P a
       ------------------ ∃ I
         (∃ y, ¬ (P y))
----------------------------------- → I
  (¬ (∀ x, P x)) → (∃ y, ¬ (P y))

but I have a problem when write the proof in lean:

variable U : Type
variable P: U → Prop
example : (¬ (∀ x, P x)) → (∃ y, ¬ (P y)) :=
assume h: ¬ (∀ x, P x),
_

[Reid Barton]

(Isn't the last rule →-introduction?)
You can write the term from the outside in, corresponding to reading your proof tree from the bottom up. assume corresponds to the last deduction. The one above that is ∃ introduction, so next you can replace _ by Exists.intro _ _

[elliott smith]

Reid Barton said:

(Isn't the last rule →-introduction?)
You can write the term from the outside in, corresponding to reading your proof tree from the bottom up. assume corresponds to the last deduction. The one above that is ∃ introduction, so next you can replace _ by Exists.intro _ _

after exists.intro should be a U type, but there is no in the context, how I can introduce a?

[Reid Barton]

∀ and → both correspond to (dependent) functions in the DTT approach to logic, so the introduction and elimination rules correspond to lambda/assume and function application respectively. The remaining connectives correspond to inductive types and you'll use the constructors/eliminators of those types.

[Reid Barton]

Oh, I didn't look at your proof that closely. What is a in the original proof?

[Reid Barton]

You actually need classical logic to prove this

[Reid Barton]

I don't think the original proof is correct, but then I never understood how traditional logic deals with quantifiers.

[elliott smith]

from the proof tree, we want prove ¬ P a, so we assumen P a and deduce ⊥

[Reid Barton]

You can't get a U from what you have, as you noted. But you can use classical.by_contradiction now (after the assume).

[Reid Barton]

Maybe try writing your proof in the form described at https://en.wikipedia.org/wiki/Natural_deduction#Proofs_and_type_theory
It's also much closer to what is happening in Lean.

[elliott smith]

I am not familiar with the classical in lean, I will take a look

[Mario Carneiro]

@elliott smith Your natural deduction proof is not correct. When you deduce ∀ x, P x from P a, you are obligated to ensure that a is not free in any open assumptions, but P a is an open assumption at the point of that deduction, so this violates the side condition of ∀ I

[Kevin Buzzard]

I'm so glad I never had to learn natural deduction proofs

[elliott smith]

@Mario Carneiro , thanks for pointing that out. Could you suggest any references about nature reduction? I am not very clearly understand what you mean.

[Mario Carneiro]

@elliott smith I googled around a bit to find a decent source, here's one. (Unfortunately the wikipedia page is a bit vague on the point I want to make here.) That page says:

$(\forall I)$ If $\Gamma\vdash[a/x]\varphi$, then $\Gamma\vdash\forall x\;\varphi$
... In the case of $\forall I$, a parameter $a$ is required to be "fresh" in the sense of having no other occurrences in $\Gamma,\varphi$. Such a fresh $a$ is sometimes called an 'eigenvariable' or a 'proper variable'.

In your case, you attempted to apply $\forall I$ to deduce from $P\,a\vdash P\,a$ to $P\,a\vdash \forall x\;P\,x$, and the eigenvariable condition is violated because $\Gamma=\{P\,a\}$ contains a free occurrence of the eigenvariable $a$.

[Mario Carneiro]

Thinking about what the theorem is trying to say, it should be obvious why this can't be true. You assume that $P$ holds for some fixed value $a$ but that doesn't mean that it holds everywhere.

[Mario Carneiro]

This might be too much of a hint, but here's how you can use by_contradiction in this case:

variable U : Type
variable P: U → Prop
example : (¬ (∀ x, P x)) → (∃ y, ¬ (P y)) :=
assume h: ¬ (∀ x, P x),
classical.by_contradiction $
assume h2: ¬ (∃ y, ¬ (P y)),
suffices ∀ x, P x, from h this,
assume x,
_ -- P x