Can we do without equality in first order logic? I looked at some cases in which equality is essential and found that it seems enough to have inequality implicit in the variables. Let $\phi(x,y)$ be a formula not containing equality.
Instead of writing $(\forall x)(\exists y) x \neq y \wedge \phi(x,y)$ one can write $(\forall x)(\exists y) \phi(x,y)$, supposing that different variables denote different objects. Correspondingly:
$(\exists x)(\exists y) \phi(x,y)$ instead of $(\exists x)(\exists y) x \neq y \wedge \phi(x,y)$
$(\forall x)(\forall y) \phi(x,y)$ instead of $(\forall x)(\forall y) x = y \vee \phi(x,y)$
$(\exists x)(\forall y) \phi(x,y)$ instead of $(\exists x)(\forall y) x = y \vee \phi(x,y)$
The other way around, if we want to express that $(\forall x)(\exists y) \phi(x,y)$ allowing the case $x=y$, we have to write $(\forall x)(\exists y) \phi(x,x) \vee \phi(x,y)$, and correspondingly
$(\exists x)(\exists y) \phi(x,x) \vee \phi(x,y)$ instead of $(\exists x)(\exists y) \phi(x,y)$
$(\forall x)(\forall y) \phi(x,x) \wedge \phi(x,y)$ instead of $(\forall x)(\forall y) \phi(x,y)$
$(\exists x)(\forall y) \phi(x,x) \wedge \phi(x,y)$ instead of $(\exists x)(\forall y) \phi(x,y)$
Another case is "there is exactly one object $x$ with $\phi(x)$":
$(\exists x)(\forall y) \phi(x) \wedge \big(\phi(y) \rightarrow y = x\big)$ becomes $(\exists x) \phi(x)
\wedge \neg (\exists x)(\exists y)\phi(x) \wedge \phi(y)$
I wonder if every sentence of first order logic including equality can be equivalently written without equality when interpreting different variables to denote different objects. For the time being I'd like to restrict the question to languages without function symbols and individual constants, i.e. comprising only relation symbols and variables.
Best Answer
The question is this:
The proposal here in fact goes back to Wittgenstein's Tractatus 5.53, where he writes, ‘Identity of the object I express by identity of the sign and not by means of a sign of identity. Difference of the objects by difference of the signs.’ Can this proposal, not really developed out by Wittgenstein, be made to work?
The answer is it that it can, as shown by Hintikka in 1956 ('Identity, Variables, and Impredicative Definitions', Journal of Symbolic Logic). Hintikka distinguishes the usual 'inclusive' reading of the variables (i.e. we are allowed to assign the same object to distinct variables) from the 'exclusive' reading, and then proves the key theorem (summarized on p. 235):
So yes, Hans Striker's conjecture is right. For a more recent revisiting of Hintikka's result, in the context of interpreting the Tractatus see e.g. Kai F. Wehmeier's 'How to Live without Identity - And Why', Australasian Journal of Philosophy 2012, downloadable at http://www.academia.edu/949632/How_to_live_without_identity_--_and_why