I am really struggling to get to grips with Enderton's Existential Instatiation. I asked a question yesterday and had to delete it shortly after because it was wrong... Hopefully, today I'll be better at narrowing down what bothers me.
Basically, trying to use a notation that is self-explanatory, Enderton is saying that $\Sigma, \varphi(c) \vdash \psi$ implies that $\Sigma, \exists x \varphi(x) \vdash \psi$. The restriction is that $c$ is a new symbol that basically doesn't appear anywhere...
Now, my problem with this is the proof. He uses a theorem that he proves in the previous page and he calls it "Generalization on constants". He proves that if $\Gamma \vdash \varphi(c)$, then there exists a variable $y$ such that $\Gamma \vdash \forall y \varphi(y)$.
In the first step of his proof, he takes a deduction of $\Gamma \vdash \varphi(c)$, replaces $c$ with $y$ in every formula, and proves that the resulting sequence is a deduction of $\Gamma \vdash \varphi(y)$. In order to do that, he takes every formula and says it must either be a logical axiom, a member of $\Gamma$ or an application of modus ponens.
Specifically, if it is a logical axiom, then it stays a logical axiom if you replace $c$ with $y$. And I agree with that, but what happens when we get out of the pure logical theory and add some non-logical axioms? I don't think there is a rule that restricts how you can write axioms, so if this theorem is all we have, each time a new theory is defined, we need to prove that all of its axioms have this property before we can use existential instantiation?
For example, I could add an axiom to the Peano system to add a new constant to define the number $1$. It would look like this: $1=S(0)$. It looks like a pretty harmless thing to do. Let me simulate a silly dialogue between me and Enderton:
Me: I claim that $\Sigma, \varphi(1) \vdash \psi$ implies $\Sigma, \exists x \varphi(x) \vdash \psi$.
Enderton: No! That's clearly wrong. $1$ is not a generic constant, so you can't do that. You must ensure that your constant does not appear in your non-logical axioms.
Me: OK, then my $c$ cannot appear in my non-logical axioms, but surely $c+0=c$ is an axiom for any $c$ I can come up with, so I would never be able to use any $c$.
Does anybody have a view on this? Is there a flaw in my reasoning? Do you think there is a way to enunciate existential instantiation without having to run through the axioms of every new theory we can come up with? Because I don't think there is anything you could write in the non-logical axioms that would harm your right to use existential instantiation.
Thank you.