Can the first-order Peano axioms be reformulated without identity and without function symbols? I tried doing this by characterizing one of the following relations axiomatically, but end up with unintended models (see here for the meaning of these terms):
succeeds
- irreflexive
- left-total
- not right-total (zero)
- discrete: $\forall x y (Rxy \to \neg \exists z (Rxz \land Rzy))$
- ...
less-than
- irreflexive
- left-total
- not right-total (zero)
- transitive
- ...
less-than-or-equal-to
- reflexive
- transitive
- strongly connex
- ...
Left- and right- uniqueness cannot be axiomatized as usual due to the lack of identity. (Left-totality + right-uniqueness + left-uniqueness + non-right-totality would suffice for the succeeds relation.)
No. By the upward Lowenheim-Skolem-Tarski theorem, there will always be models of higher cardinality once one can show the existence of an infinite model. So one can't zero in on the intended model $\mathbb{N}$ exactly with a first-order theory. Hence the necessity for a second-order axiom like the induction axiom.
Another problem is that without function symbols, the Herbrand Universe is finite. So there might be problems assuring that the models are all infinite.