In Natural Deduction can I use a negation introduction when I already have (∃x)(Gx∧¬Gx)?

Question

In a Natural Deduction, I want to get ¬(∃x)(Gx). So I assume (∃x)(Gx), and get the following Ga and ¬Ga for some a. What I have got:

Can I use the negation introduction(¬I) below? If not, what should I do?

Answer 1

The details will depend on your particular system of natural deduction. But in many, yes, you can introduce $\bot$ with an absurdity rule and then (since $\bot$ does not involve the variable $a$), discharge the assumption using $\exists$E, and then use RAA i.e. $\neg$I.

So this, for example, is a correct proof:

$\forall x \neg Gx\\ \quad\quad|\quad \exists x Gx\\ \quad\quad|\quad\quad\quad|\quad Ga\\ \quad\quad|\quad\quad\quad|\quad \neg Ga\\ \quad\quad|\quad\quad\quad|\quad \bot\\ \quad\quad|\quad \bot \\ \neg\exists x Gx$

Make sure you understand the justification for each step!