If we have a theory of numbers, pairs of numbers, and sets of those, and axiomatize that the relation $<$ on numbers is both extensional and well founded, then this theory would prove all PA axioms over numbers.
What happens if we drop the requirement of $<$ being extensional?
Formally speaking, let's work in four-sorted first order logic, first sort written in Greek, stands for natural numbers; second sort written as pairs of Greeks standing for pairs of naturals; the third written in lower case, stands for elements of sets; the fourth sort written in upper case, standing for Sets.
Primitives: $S$, $=$, $\in$.
The first standing for "successor" a unary function from first sort to first sort, the second standing for "equality" with the axioms of ID theory, the third standing for set membership from first three sorts to the fourth sort.
Logical axioms about sorts:
I: Separateness: $X \neq x \land \alpha \neq \beta \lambda $.
II: Elements: $\forall x\, \exists \alpha \, ( x=\alpha \lor \exists \beta: x=\alpha\beta)$.
Extra-logical axioms:
- Comprehension: $\exists! X \, \forall y \ (y \in X \iff \phi)$; where "$X$" doesn't occur in $\phi$.
Define: $\mathbb N = \{\alpha: \alpha = \alpha\}$.
Well-Foundedness: $X \subseteq \mathbb N \land X \neq \emptyset \to \exists \alpha \in X \, \forall \beta \in X \, (\alpha \neq S(\beta))$.
Start: $\exists! \alpha : \neg \exists \beta \, (\alpha = S(\beta))$.
Pairs: $\alpha \beta = \gamma \lambda \to \alpha=\gamma \land \beta = \lambda $.
Now this theory would prove that the relation $<$ "strict lower than" on numbers would be an extensional well founded relation, and so would prove induction and all axioms of PA over numbers; and with the sets of numbers it would I think be equivalent to second order arithmetic.
So the question stated formally is about what happens if we just remove uniquness $!$ from axiom 4. By then we can have multiple starting numbers, and so violate $<$ being extensional. This would let numbers be able to have many predecessor numbers. This way induction cannot be proved! However, instances of induction would be proved if all starting numbers qualify for the predicate in the instance.
So what would be the strength of such a weakened theory? Would it still continue to prove all instances of PA over numbers?
