I have been thinking about how I can prove something like this: $\forall x\neg P(x) ⊢\neg \exists xP(x)$. Unfortunately, I can’t seem to get anywhere...
I have tried assuming $\exists xP(x)$ to get a contradiction, but I only got the contradiction in a sub proof, so I am unsure about how to get $\neg \exists xP(x)$ at the end. How should I proceed? I used curly brackets to show where a sub proof starts and ends, I’m sorry for any confusion.
$∀x¬P(x)$ [premise]
$\qquad\{∃xP(x)$ [assume]
$\qquad\qquad\{P(a)$ [a]
$\qquad\qquad¬P(a)$ [∀ elimination]
$\qquad\qquad ⊥\}$
$\qquad?\}$
$¬∃xP(x)$
You need to use $\exists E$ to justify $\bot$ without the assumption of $Pa$.
From https://proofs.openlogicproject.org/, the natural deduction proof editor and checker: