# Zulip Chat Archive

## Stream: general

### Topic: Negation of ∃ elimination

#### Dominic Farolino (Feb 13 2019 at 00:16):

Existential quantifier elimination is illustrated here: https://leanprover.github.io/logic_and_proof/natural_deduction_for_first_order_logic.html. It says we can prove `B`

from `∃xA(x) B`

, if be can be proved from a hypothesis `A(y)`

. I'm wondering, if I have `¬∃xA(x) B)`

, can I prove `B`

from a hypothesis `¬A(y)`

? Is it valid to make the assumption `¬A(y)`

here, from `¬∃xA(x)`

?

#### Mario Carneiro (Feb 13 2019 at 01:27):

What you want is actually: If we have `∃x ¬A(x)`

, and `B`

assuming `¬A(y)`

, then we can deduce `B`

. This is just the regular exists intro rule. If we use de Morgan on the first assumption, it says that if `¬∀x A(x)`

, and `¬A(y)`

implies `B`

, then we can deduce `B`

. To derive this, in classical logic, we can case on whether `∃x ¬A(x)`

or not. If it's true, we use the first argument to conclude. If it's false then `¬ ∃x ¬A(x)`

, so it suffices to derive `∀x A(x)`

to get a contradiction with the assumption `¬∀x A(x)`

. For any `x`

, if `A(x)`

is not true (proof by contradiction) then `¬A(x)`

, so `∃x ¬A(x)`

which contradicts the assumption. Thus `∀x A(x)`

and `¬∀x A(x)`

, so `B`

holds by reductio ad absurdum.

#### Dominic Farolino (Feb 13 2019 at 02:44):

If we have

`∃x ¬A(x)`

, and`B`

assuming`¬A(y)`

, then we can deduce`B`

. This is just the regular exists intro rule.

Ah, yeah I did know this, just wasn't sure exactly what I could do with the negation outside. Ultimately what I was actually trying to prove is `¬∃xA(x) -> ∀x ¬A(x)`

, and I bungled it and got stuck. I re-worked it, to get the image attached to this message. If it isn't to much trouble, would you migth checking it for correctness? (Haven't read chapter 9 of Logic and Proof yet, where first order logic is used in lean) IMG-1411.JPG

Last updated: May 17 2021 at 21:12 UTC