Could relational operators be used to construct formal theory of natural numbers which is "stronger" than Peano Axioms?

Question

This is a beginner's question about foundational construction of (alternative?) number theory. The notion of mathematical equality is closely related to logico-philosophical notion of 'Law of Identity', and Peano axioms start from defining equality (axioms 1-4 according to wiki article) with a certain logical apparatus, which presupposes law of identity, and only then proceed to "Successor function" of additive property.

The basic intuition here is that it could and imho would be more natural to derive mathematical equivalence from more basic "countable" or "ordinal" relations, formally relational operators < and >, than from formal presupposition of Law of Identity which basically gives "=" as given axiom. Deriving equality from "neither less nor more", e.g. if not not equal "<>" then equal "=" seems better connected with universals of counting and ordinality in natural languages of the world (AFAIK at least ordered finite set 'one', 'two', 'three', 'many'/'more' can be found in all languages) than the Peano approach.

Wiki article on relational operators indeed states that "relational operators can be designed to have logical equivalence, such that they can all be defined in terms of one another". If I'm not mistaken, the "cardinal" aspect of natural numbers, which arithmetic functions seemingly requires, could then be derived from relational equivalence in consistent manner. and cardinal numbers as relational identities would be subcategory of more fundamental ordinal relations < and >, and further relational operators derived from those.

I won't attempt to fully formalize this idea here, but leave the task open for any takers. I don't yet know how this idea relates e.g. to Skolem's approach, Löwenheim–Skolem theorem and Skolem's paradox, ie., how dependent those are from the logical apparatus and set theoretical approach used, and do their results extend to mathematics more generally, and welcome all contributions.

Answer 1

Your plan is not crazy, and is actually pretty close to how set theory is often (but not always) formalized, in a logical language where $\in$ is the only primitive predicate, and equality is a defined concept: "$x=y$" is an abbreviation for "$\forall z(z\in x\leftrightarrow z\in y)$".

This approach is not as popular for arithmetic though. I have no doubt something similar could be made to work for arithmetic if one sat down and did the necessary footwork, but I'm less convinced that it would really buy us anything.

One possible reason why it is so is that for first-order Peano arithmetic it is not enough to have $0$ and the successor function; we also need addition and multiplication as primitives -- and as far as I can see, having a primitive ordering would not relieve us of this. And it is pretty important for reasoning about addition and multiplication that they're functions, which means that if their inputs are the same, the output will also be the same. This requires us to have some notion of "the same" before we can state even the most basic properties of our primitive notions here.

(This is not a completely airtight rationale, because we might state that addition and multiplication are both increasing in each argument, and get an axiom that is slightly stronger than simply saying that they are functions -- but on the other hand "stronger axiom" doesn't always translate to "better" in foundational contexts).

If we go to the second-order Peano axioms, we don't need addition and multiplication to be primitive anymore -- but on the other hand I don't see that we can progress in a sane way without explicit axioms that state that all predicates and functions respect the usual equality rules:

$$ \forall P \forall x \forall y \bigl( x<y \lor y<x \lor (P(x)\leftrightarrow P(y)) \bigr) $$ $$ \forall F \forall x \forall y \bigl( F(x)<F(y) \lor F(y)<F(x) \to x<y \lor y < x \bigr)$$ (was well as variants of these for all other arities) -- and these properties do not feel like they really flow naturally from the concept of comparing sizes; they are much easier to justify by appealing to an idea of "being the same".

---

A more philosophical objection: Even if you can construct an argument that "more/less" is a more fundamental property of number than "the same" is, consider that logic comes before number. And our entire tradition of symbolic logic is deeply entrenched with concepts of "the same". In particular, when we use a variable letter in different places in a formula, it is implicit that those two instances will represent the same thing -- except to the extent that we use quantifiers to explicitly modulate that expectation. It would seem arbitrary not to allow the formulas themselves to speak explicitly about "sameness" as a primitive concept, when "sameness" is already so fundamental to how to interpret formulas intuitively.