Conditions on Existential Generalization in an axiomatic proof system In the axiomatic proof system that I am using, I have Existential Generalization (EG).
So an instance of EG is the following.
$(Fx \land Gx) \rightarrow \exists z (Fz \land Gz)$
But is the following a valid instance of EG?
$(Fx \land Gx) \rightarrow \exists z (Fx \land Gz)$
Now, usually Existential Generalization is given where the consequent quantifies and replaces every instance of a variable (or term). So would my second instance of EG be an incorrect instance since I only replaced and quantified one of the $x$'s in the consequent?
If my second instance is not a valid use of (EG), is there any quick way to prove the second instance using (EG) and perhaps some other intermediary steps?
 A: Based on your presentation of existential generalization, you're right that the candidate example you give is not a valid instance. It would, however, be fine to expand the rule to allow it since it is derivable.
Basically:

*

*From $Fx\wedge Gx$ infer $Fx$ and $Gx$ separately via the conjunction elimination rules.


*Apply existential generalization to $Gx$ to get $\exists z(Gz)$, and then existential instantiation to that to get $Gc$ for a fresh symbol $c$.


*Using conjunction introduction, get $Fx\wedge Gc$.


*Now apply existential generalization, replacing $c$ this time, to that to get $\exists z(Fx\wedge Gz)$.

Alternatively, and in my opinion more transparently, we could argue semantically and then apply the completeness theorem: since any structure-and-variable-assignment pair making $Fx\wedge Gx$ true also makes $\exists z(Fx\wedge Gz)$ true, by the completeness theorem the corresponding inference must be deducible from the rules you already have.
A: 
usually Existential Generalization (aka: Existential Introduction) is given where the consequent quantifies and replaces every instance of a variable (or term).

Correct. How to get the result describey by @Noah's answer above with Natural Deduction?
We consider $\varphi(x,x)$ meaning that the formula has (at least) two distinct free occurrences of variable $x$.

*

*$\varphi(x,x)$


*$\lnot \exists y \varphi (x,y)$ --- assumed [a]


*$\varphi (x,y)$ --- assumed [b]


*$\exists y \varphi (x,y)$


*$\lnot \varphi (x,y)$ --- using the contradiction 2)-4) and discharging assumption [b]


*$\forall y \lnot \varphi (x,y)$ --- by UG: correct, because $y$ is not free in assumptions above


*$\lnot \varphi(x,x)$ --- by UI



*$\exists y \varphi (x,y)$ --- using the contradiction 1)-7) by Double Negation, discharging assumption [b].


A: 
From any statement $\varphi(x,x)$ where term $z$ does not occur, you may infer $\exists z~\varphi(z,x)$. $$\varphi(x,x)\vdash \exists x~\varphi(z,x)$$

That is :   You do not have to replace all free instances of $x$.   You can generalise on as many of these instances as you need (including zero).

Now $x$ is often a witness variable (a fresh variable obtained through existential instantiation) and you do not want any occurrences of such to remain in the conclusion.   If you ensure that it does not, then there is no issue.
