3
$\begingroup$

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$.

$\endgroup$
  • 2
    $\begingroup$ Don't you have a rule that allows you to deduce $\exists x.\Phi(x)$ from $\Phi(c)$? $\endgroup$ – MJD Aug 18 '14 at 4:51
  • $\begingroup$ What is the formal proof system you are working with? $\endgroup$ – Carl Mummert Aug 18 '14 at 10:08
  • $\begingroup$ @MJD I wish my formal system had that as a rule; I've thought of just adding it as a rule and moving on, but wondered how to make a formal proof with the system at hand. $\endgroup$ – Hayden Aug 18 '14 at 10:24
  • $\begingroup$ @CarlMummert I added the specific formal system. $\endgroup$ – Hayden Aug 18 '14 at 10:24
  • $\begingroup$ @MJD Thinking on it further, I guess my Axiom (7) likely captures that rule, so I'll try and deduce it from that. $\endgroup$ – Hayden Aug 18 '14 at 10:45
3
$\begingroup$

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)
$\endgroup$
  • $\begingroup$ Thanks for all the help. I also ended up being able to make a formal proof of Existential Generalization using Rule 7 and first proving $\{(\alpha\rightarrow \beta)\}\vdash ((\beta\rightarrow \bot)\rightarrow (\alpha\rightarrow \bot))$. So many possible proofs! $\endgroup$ – Hayden Aug 18 '14 at 11:35
3
$\begingroup$

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)$
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.