Instantiation and Negation

Question

Are we allowed to perform universal & existential instantiation when there is a negation in front of the statement? A bit confused since normally I just turn something like $\neg \exists x (...)$ into $\forall \neg (...)$

Answer 1

Do you mean you have a formula of the form $\neg \exists x \phi(x)$ and you want to somehow instantiate that? You cannot.

Existential instantiation means you start with $\exists x \phi(x)$ and conclude $\phi(c)$ for some new constant $c$. This is possible because $\exists x \phi(x)$ is saying that there is some $x$ such that $\phi(x)$, so we may give it a new name $c$ that doesn't conflict with any name we've previously worked with. If you have $\neg \exists x \phi(x)$, it is saying that something doesn't exist. There is nothing to instantiate.

One thing you can do is convert $\neg \exists x \phi(x)$ to $\forall x \neg \phi(x)$, and then conclude $\neg \phi(t)$ for some term $t$ that will help you in the rest of the proof.

Answer 2

In most math courses, most quantifiers are restricted to some set, e.g. $\forall x\in S: P(x)$ or $\exists x\in S: P(x)$.

If assume or have proven that $\neg \exists x\in S: P(x)$, then we can infer that $\forall x\in S: \neg P(x)$ as you suggest. If we also know that $S$ is non-empty, say $x_0\in S$, then we can also infer that $\neg P(x_0)$.