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
On Friday, September 17, 2021 at 3:11:15 PM UTC-4 [email protected] wrote:
> 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.
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/f3be3db8-0ae3-431f-8a03-4558daad3ccbn%40googlegroups.com.
