## Stream: new members

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

#### elliott smith (Mar 20 2020 at 18:18):

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 (Mar 20 2020 at 18:22):

(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 (Mar 20 2020 at 18:33):

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 (Mar 20 2020 at 18:34):

∀ 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 (Mar 20 2020 at 18:34):

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

#### Reid Barton (Mar 20 2020 at 18:35):

You actually need classical logic to prove this

#### Reid Barton (Mar 20 2020 at 18:39):

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

#### elliott smith (Mar 20 2020 at 18:39):

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

#### Reid Barton (Mar 20 2020 at 18:40):

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 (Mar 20 2020 at 18:49):

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 (Mar 20 2020 at 18:49):

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

#### Mario Carneiro (Mar 20 2020 at 21:39):

@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

#### elliott smith (Mar 20 2020 at 23:04):

@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 (Mar 21 2020 at 00:23):

@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 (Mar 21 2020 at 00:28):

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 (Mar 21 2020 at 00:34):

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),