Proving that ∀xG(x,a)⊢∃xG(a,x)

Question

Can I prove ∀xG(x,a)⊢∃xG(a,x) this way:

∀xG(x,a)   premise
G(a,a)     ∀xe
∃xG(a,x)   ∃xi

Answer 1

Yeah, you can prove it that way.

Here is another way. The tableau $$ \forall x G(x, a) \\ \lnot \exists x G(a, x) \\ G(a, a) \\ \lnot G(a, a) $$ is closed, so the result holds. (It's a proof by contradiction.)

Answer 2

Your proof is correct. I think you are doubting yourself because in going from $G(a,a)$, is it ok to not replace all $a$'s with $x$'s? This is a common concern.

But yes, this is indeed ok!

In general:

When you eliminate a quantifier, then you do need to replace all variables that were quantified by that quantifier using a constant.

But when you introduce a quantifier, you do not have to replace all constants that you quantify by the variable you use for that quantifier.