Proving $\vdash \exists x (x=c)$ for each term $c$.

Question

I wish to prove that $\vdash \exists x (x=c)$ for each term $c$. It seems quite obvious that this would be the case, for $c$ is such an $x$, but creating a formal proof of this is escaping me.

$(c=c)$ is an axiom and by generalization we have $\forall x (c=c)$. From this point I can't see how to justify replacing the first $c$ with an $x$ nor to add appropriate negations to make this into $\neg \forall x \neg (x=c)$.

The context is that I'm trying to prove the Completeness Theorem using the Henkin-style proof, so for that reason using the Completeness Theorem is not an option, though it would admittedly make it a no-brainer.

The specific formal system I'm working with is

1. $(\alpha\rightarrow \alpha)$
2. $(\beta\rightarrow (\alpha\rightarrow \beta))$
3. $((\alpha\rightarrow \beta)\rightarrow ((\alpha\rightarrow (\beta\rightarrow \gamma))\rightarrow (\alpha\rightarrow \gamma)))$
4. $((\alpha\rightarrow \bot) \rightarrow (\alpha\rightarrow \beta))$
5. $(((\alpha\rightarrow \bot)\rightarrow \bot)\rightarrow \alpha)$
6. $(\forall x (\varphi\rightarrow \psi) \rightarrow (\varphi\rightarrow \forall x \psi))$ whenever $\varphi$ and $\psi$ are wffs, $x$ is a variable, and $x$ is not free in $\varphi$
7. $\forall x \varphi(x)\rightarrow \varphi(y)$ whenever $\varphi(x)$ is a wff with free variable $x$, $y$ is a variable or constant, and no free occurence of $x$ in $\varphi(x)$ is within the scope of a $\forall y$
8. $(t=t)$ whenever $t$ is a term
9. $((x=y)\rightarrow (\varphi \rightarrow \psi))$ whenever $x$ and $y$ are variables or constants, $\varphi$ and $\psi$ are wffs, and $\psi$ is obtained by substituting $y$ for some free occurrences of $x$ in $\varphi$.

Our rules of inference include Modus Ponens: $\{\alpha\rightarrow \beta,\alpha\}\vdash \beta$, and Generalization: $\{\varphi\}\vdash \forall x \varphi$.

Answer 1

Because of rule 7, it is sufficient to derive $(\forall z)(\exists x)[x = z]$.

Because of generalization, it is thus enough to derive $(\exists x)[x = z]$ with $z$ being free.

In your system, $(\exists x)[x = z]$ is an abbreviation for $(\forall x) [ x \not = z] \to \bot$. The general outline of a derivation of the latter is as follows:

1. $(\forall x)[x \not = z]$ (assumption)
2. $z = z$ (rule 8)
3. $z \not = z$ (rule 7 applied to 1). Remember this is $(z = z) \to \bot$.
4. $\bot$ (modus ponens applied to 2,3)
5. $(\forall x)[x \not = z] \to \bot$ (deduction theorem)

The difficulty with formalizing this sketch in your proof system is that the sketch uses the deduction theorem, which can be removed using the algorithm in the proof of the deduction theorem for your system.

---

Here is a hands-on derivation of $(\forall x)(x \not = z) \to \bot$, not using the deduction theorem. You can see that the trick is to use rule 3.

1. $(z \not = z) \to (z = z) \to \bot$ (rule 1)
2. $ z = z$ (rule 8)
3. $(z = z) \to (z \not = z) \to z = z$ (rule 2)
4. $(z \not = z) \to (z=z)$ (modus ponens on 2,3)
5. $((z \not = z) \to (z =z)) \to ( (z \not = z) \to (z = z) \to \bot) \to ((z \not = z) \to \bot)$ (rule 3)
6. $(z \not = z) \to \bot$ (modus ponens twice)
7. $((z \not = z) \to \bot) \to (\forall x)(x \not = z) \to (z \not = z) \to \bot$ (rule 2)
8. $ (\forall x)(x \not= z) \to (z \not = z) \to \bot$ (modus ponens on 6,7)
9. $(\forall x)(x \not = z) \to (z \not = z)$ (rule 7)
10. Rule 3: $$((\forall x)(x \not = z) \to (z \not = z)) \to ((\forall x)(x \not = z) \to (z \not = z) \to \bot) \to ((\forall x)(x \not = z) \to \bot)$$
11. $(\forall x)(x \not = z) \to \bot$ (modus ponens twice)

Answer 2

If your form of Existential Generalization requires you to replace all occurences of a single constant with your chosen variable, you can instead use proof by contradiction:

• $\neg\exists x(x=c)$
• $\forall x\neg(x=c)$
• $\neg(c=c)$
• $\bot$
• $\neg\neg\exists x(x=c)$
• $\exists x(x=c)$