# Zulip Chat Archive

## 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`

#### Kevin Buzzard (Mar 20 2020 at 22:07):

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

#### 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), classical.by_contradiction $ assume h2: ¬ (∃ y, ¬ (P y)), suffices ∀ x, P x, from h this, assume x, _ -- P x

Last updated: May 10 2021 at 00:31 UTC