Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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),
_

view this post on Zulip 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 _ _

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Mar 20 2020 at 18:35):

You actually need classical logic to prove this

view this post on Zulip 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.

view this post on Zulip elliott smith (Mar 20 2020 at 18:39):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip elliott smith (Mar 20 2020 at 18:49):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 22:07):

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

view this post on Zulip 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.

view this post on Zulip 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:

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

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

view this post on Zulip 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 PP holds for some fixed value aa but that doesn't mean that it holds everywhere.

view this post on Zulip 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