In my current frame of mind I feel the worst thing about first-order predicate calculus is its many names. Wilkipedia suggests several others and I suppose I will go with ‘predicate logic’ here for its brevity. There is a cluster of concepts here with little correlation between name and concept. Several of the concepts I am familiar with are equivalent as can be seen with fairly simple proofs. Second-order logic is a definite extension and the article relates how set theory, along with first-order logic, is considered by many to be an adequate alternative to Second-order logic.
When I learned Henkin’s completeness proof for predicate logic from Benson Mates (Berkeley 1954) he pointed out that axioms for the equality predicate could be added to those of predicate logic and the completeness proof extended so as to prove the existence of proofs for all generally true predicate logic statements with equality given the standard semantics for equality. The additional axioms were ⊢ x = x and ⊢ x=y → (φ → ψ) when x occurs freely in φ wherever y occurs freely in ψ. It seemed clear that this was the only predicate for which this was possible. I found this comforting and welcomed equality into my inner sanctum of fundamental concepts. Still there was a great deal of logic that seemed productive without equality.
Sometimes we need equivalence rather than equality but that may not address the fundamental problems with equality.
In quantum mechanics one learns not to ask of two electrons, which election is which— do not ask “Is this the electron that was over there one second ago?”. Find a way of talking and thinking so that that question can not be phrased. The multi particle interpretation of Schrödingers equation achieves this. John Baez writes in Categorifying Fundamental Physics about avoiding equality in mathematical physics by hewing to category theory. Evils of =
Yet philosophers remark on the realization that ‘the morning star’ is the same as ‘the evening star’. Benefits accrue from that realization. We want those benefits; can they be had without equality? Projective geometry seems to demand inequality in a general way; see “equality” in this note.
There is some anxiety over equality in programing languages. Perhaps of special note is the question of how to aggregate the rumors of integrity of some purported agent that you must decide whether to trust. Is the Joe known by Jim the same as the Joe known by Jane, and how do I get in touch with Joe? I have seen specific instances of solving such problems without equality but I have not understood a general pattern. I have seen no vague patterns for how to transform away uses of equality.