How tricky is it to define predicate calculus without equality?

[Gustavo Gonçalves]

It seems like if one wants to define equality instead of "axiomizing" it, it would be as

|- ( x = y <-> A. w ( w e. x <-> w e. y ) )

So I started doing a little digging to how much things would change if we used that instead.

ax-7 |- ( x = y -> ( x = z -> y = z ) )

I think we can derive ax-7 by using the following theorems

by definition |- ( x = y <-> A. w ( w e. x <-> w e. y ) )

using albiim, syl, some other biconditional theorems

|- ( A. w ( w e. x <-> w e. y ) -> A. w ( w e. x -> w e. y ) )

|- ( A. w ( w e. x <-> w e. y ) -> A. w ( w e. y -> w e. x ) )

the same can be applied to x = z

with that and a few other theorems (such as alsyl) I'm pretty sure you can reach

|- ( ( A. w ( w e. x <-> w e. y ) /\ A. w ( w e. x <-> w e. z ) ) -> A. w ( w e. y <-> w e. z ) )

and applying ex we can prove ax-7

The description in the axiom of extensionality already states that if we define equality instead axiomizing it, we can basically rewrite it as ax-8. So that's covered

Unfortunately, we can't prove ax-9 with this definition without ax-12

But using ax-12, we can pretty much apply sp to the definition, along with biimp and syl and that proves ax-9

So us there another reason to why it's preferable to use equality as a primitive wff?

There's a chance I'm forgetting problems that could arise, or maybe it's just really inconvenient in the long run.

[Norman Megill]

You may want to look at the [Tarski] reference at http://us.metamath.org/mpeuni/mmset.html#bib showing how to formulate predicate calculus without equality on p. 78:

Tarski, Alfred, "A Simplified Formalization of Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:61-79 (1965)

which I think would work. The system needs an arbitrary binary predicate pi, which can be our e., and "equality" (I'll call it ~~) would be defined as

x ~~ y <-> (A. w ( x e. w <-> y e. w ) /\ A. w ( w e. x <-> w e. y )),  with w distinct from x and y

Our axioms ax-6,7,8,9 would be replaced by the ones he shows as A8', A9', A9'', and A9'''. His A9' would become our ax-8 and ax-9 with ~~ instead of =.

The brackets on Tarski's schemes indicate the Quine closures of the axioms, but I think they can be removed. As far as I can tell, the closures eliminate the need for ax-gen (compare the inference rules for system S_1' on p. 75 with those for system S_2 - equivalent to our ax-1 through ax-9 - on p. 77). But unless I am missing something, the unwieldiness of closures seems like a high price to pay for this, and I've never understood their appeal. (If someone understands the advantage of Quine closures, let me know.)

I think our axioms ax-12 and ax-13 will remain valid with ~~ instead of =. However, they aren't needed for logical completeness, only for scheme completeness ("metalogical completeness"). An open question is whether scheme completeness would continue to hold and, if not, whether it can be repaired with different or additional axioms.

As for why we have equality as primitive, it is partly a matter of taste.  The axioms would become very long and unwieldy when defined symbols are eliminated.  I have tried to find the simplest axioms possible when expressed in primitive form.  In addition, there is tradition:  predicate calculus with equality is almost always presented in the literature with = as primitive.

Perhaps a somewhat analogous situation is why we have both -. and -> as propositional calculus primitives, when a single primitive, the Sheffer stroke (nand), would suffice.

Norm