First order logic - how to prove a specific part of the completeness theorem?

Question

I am working with the proof system for FOL described in Chang and Keisler. It contains the following axiom schemes:

1. $\alpha \to (\beta \to \alpha)$
2. $[\alpha\to(\beta\to\gamma)]\to[(\alpha\to\beta)\to(\alpha\to\gamma)]$
3. $(\neg\beta\to\neg\alpha)\to(\alpha\to\beta)$
4. $\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$).
5. $\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 [(\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).

Answer 1

I assume you already know that axioms 1, 2, 3 with MP prove every propositional tautology. Also, since $\exists$ is not a formal symbol in your system, presumably $(\exists x)\phi$ abbreviates $\neg(\forall x)\neg\phi$. Then I'd proceed as follows:

Assume that $$T\vdash \neg[(\exists x)\varphi(x)\to\varphi(d)]$$ (by the way "$T\vdash$" is pronounced "$T$ proves", so when you say "some theory $T$ proves sucn-and-such", the "such and such" should not include the "$T\vdash$"). We also have the propositional tautologies $$T\vdash \neg[(\exists x)\varphi(x)\to\varphi(d)] \to (\exists x)\varphi(x)$$ $$T\vdash \neg[(\exists x)\varphi(x)\to\varphi(d)] \to \neg\varphi(d)$$ and then by MP, $$T\vdash \neg(\forall x)\neg \varphi(x) \qquad\text{ and }\qquad T\vdash\neg\varphi(d)$$

When you have some formal proof of $\neg\varphi(d)$ and $d$ is not mentioned by name in any of the axioms, you can take the entire proof and replace every instance of $d$ with $z$, where $z$ is a variable that occurs nowhere in the proof. This isn't a rule of inference; it is based on the meta-observation that every instance of a (logical or proper) axiom is still an axiom when you've substituted $z$ for $d$, and every application of MP or Gen similarly survives the substitution.

This gives you a new proof that concludes $\neg\varphi(z)$. Now generalize $z$ and immediately instantiate it to $x$ (which is allowed or $\varphi(x)$ in the initial assumptions would have been meaningless), giving $ T\vdash \neg\varphi(x) $, which you can generalize to $$ T \vdash (\forall x)\neg\varphi(x) $$ This contradicts $T\vdash \neg(\forall x)\neg\varphi(x)$, which we had from above, so the theory must be inconsistent!