Elementary existence proof in first order logic

142 Views Asked by At

Please forgive my dullness but I just don't know how to - formally - show that

$$\lbrace \forall x\ \phi(x), \exists x\ x = x \rbrace \vdash \exists x\ \phi(x)$$

for an arbitrary formula $\phi(x)$.

It seems easy when there are individual constants:

$$\forall x\ \phi(x)\vdash \phi(a) $$

$$\phi(a) \vdash \exists x\ \phi(x)$$

But when the language doesn't contain individual constants, and $\exists x\ x = x$ is all that I know?

1

There are 1 best solutions below

5
On BEST ANSWER

Let $y$ be a variable not occuring at all in $\phi(x)$. Then we have $$\forall x\;\phi(x)\vdash\phi(y)$$ per Universal Instantiation and then $$\phi(y)\vdash\exists x\;\phi(x)$$ (because $x$ does not occur in $\phi(y)$) per Existential Generalization.

How come we don't even need $\exists x\;x=x$? Well, the rules of inference already incorporate that our universe of discourse is nonempty (variables are not of type "pink unicorn").