I am working with the proof system for FOL described in Chang and Keisler. It contains the following axiom schemes:
- $\alpha \to (\beta \to \alpha)$
- $\forall x\varphi(x) \to \varphi(t)$ where $t$ is a term which is free for substitution for x in $\varphi$ (i.e. $t$ contains no variable that will fall under a quantifier in $\varphi$).
- $\forall x(\varphi \to \psi)\to (\varphi \to \forall x\psi)$ where $x$ does not occur freely in $\varphi$.
The rules of inference are MP (from $\alpha$ and $\alpha\to \beta$ infer $\beta$) and Gen (from $\alpha$ infer $\forall x \alpha$).
In the proof of the completeness theorem (page 62 in C&K) we arrive at a stage where some theory $T$ proves the following sentence:
$$T\vdash \neg[(\exists x)\varphi(x)\to\varphi(d)]$$
Where $d$ is a constant symbol not present in the theory. Now C&K claim that $$T\vdash [(\exists x)\varphi(x)\wedge \neg\varphi(d)]$$
This presents some trouble for me, as in my proof system $\wedge$ is not a formal symbol (in C&K it is, and $\to$ is only a shorthand). However, this is still ok for me.
Now C&K claim that
$$T\vdash \forall x[(\exists x)\varphi(x)\wedge \neg\varphi(x)]$$
And this is the first real problem I have. I can understand the idea behind this claim - repeat the proof of the previous sentence replacing each occurence of $d$ by $x$. However, I am not sure if this can be carried out in the system I outlined above.
The main problem I have is with the next claim:
$$T\vdash x[(\exists x)\varphi(x)\wedge \neg(\exists x)\varphi(x)]$$
It is quite obvious that this sentence and the previous one were semantically equivalent; however, I fail to see how one can progress from the first to the second in the proof system I outlined. There doesn't seem to be any relevant rule, and my attempts to "play" with the rules have came out with nothing.
My question is how to formalize, in the concrete proof system I gave (and preferably without using $\wedge$ at all) C&K's argument.
(A valid response is "use another proof system" as virtually any book has his own flavor for a proof system; however, I prefer to work with "my" proof system).