Negation of ∃ elimination

Stream: general

[Dominic Farolino]

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]

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]

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