# (First order predicate calculus) Show that the theory of the equality axioms isn’t complete

If I have a theory with the following axioms:

1. $\forall x.(x=x)$

2. $\forall x\forall y.\left(x=y\rightarrow\left(\varphi\left(x,x\right)\rightarrow\varphi\left(x,y\right)\right)\right)$, where $\varphi$ is any atomic formula.

And any model of these axioms is an equivalence relation, how do I prove that this theory isn't complete?

-
What is the signature of your model? if it is just "=" as a binary relation, then φ(x,y) (being atomic) can only be x=y, it seems to me. If you allow φ to be any (also non atomic) formula, then your signature has infinite binary relations. Also: the sentence "And any model of these axioms is an equivalence relation" simply means that the "=" theory also has the axioms of an equivalence theory (for ex. x=y and y=z → x=z). Am I correct? –  magma Dec 19 '11 at 9:21
I would like to edit my previous comment, but i do not see how.So - in my previous comment - please replace the sentence:"if you allow...." with "If you alllow φ to be any other binary relation (that is different from "=") , then your signature has infinite binary relations, so it is in fact a scheme". –  magma Dec 19 '11 at 13:41

## 1 Answer

Let $\phi$ be the sentence $\forall x \forall y (x=y)$. Is $\phi$ a theorem? Is $\lnot\phi$ a theorem?

-
Well...is it or is it not? Can someone please formally prove that it is unprovable? –  magma Dec 19 '11 at 9:23
It is incomplete. The obvious argument is model-theoretic. There is a model with more than $1$ element. So $\phi$ cannot be a theorem. there is a model with $1$ element. So $\lnot\phi$ cannot be a theorem. –  André Nicolas Dec 19 '11 at 10:13
I agree with you. Actually, by the same argument, ∀x∀y φ(x,y) is unprovable. Yet I am a bit puzzled...This question looks like a problem from a textbook and it looks like there is more to it then what is described here. Let's see if the OP comes up with a comment –  magma Dec 19 '11 at 17:09
@magma: Yes, context is not supplied, and it would be nice to know whether there is something more interesting going on. As you pointed out, it would be nice to have a full conventional quick description of the language. –  André Nicolas Dec 19 '11 at 17:45