Dtyjlui

Informal account: the following theory copies one of the most basic understanding of "natural number", that of it being an indicator of how many members are there in a finite set, all sets are fully extensional, separation rule applies as usual, and the numbering rules are the equality and the inequality rule, the first one states that if one can send elements of one set to another in one-to-one manner in both directions, using first order formulas, then both sets are assigned the same number, on the other hand the second rule states that the number assigned to a proper subset of a set is not equal to the number assigned to the set. These rules here are meant to enforce restricting our discourse to finite sets only and thus the naturals are the numbers that indicate how many elements are in finite sets. Now as a set formation rule this theory can construct sets of all numbers that are smaller than or equal to any given number. A number $n$ is to be labelled as "strict natural" if $n$ is a number that is assigned to the set $mathcal N^{<n}$ of all numbers strictly smaller than $n$, provided that $mathcal N^{<n}$ is well founded by the $leq$ relation (see below), and such that every non zero element of $mathcal N^{<n}$ has a predecessor, and $n>0$ itself has a predecessor. This method proves the existence of infinitely many strict naturals, and proves the absence of a set of all of them. Also it proves that all numbers are strict naturals! So it does prove induction over all numbers! Also it easily proves summation and multiplication rules, so it can interpret $PA$, however it also defines finite sets of naturals, so it is a subsystem of second order arithmetic. But I generally think it is just a conservative extension over $PA$. Yet I'm not sure of that, hence the question?

Formal Exposition:

Language: mono-sorted first order predicate logic with extra-logical primitives of
$``=,in,N"$ standing for equality, set membership and the number of elements of,
respectively, where the last is a one place total function.

Axioms: those of identity theory +

1. Extensionality: $forall x (x in A leftrightarrow x in B) to A=B$

2. Separation: if $varphi(y)$ is a formula in which $y$ is free, and $X$ not free, then all closures of:
$$forall S exists X forall y (y in X leftrightarrow y in S wedge varphi(y))$$ are axioms.

Define: $phi text { is 1-1 from } X to Y iff \forall x in X [exists! y in Y phi(x,y) wedge not exists z in X (z neq x wedge exists u in Y (phi(z,u) wedge phi(x,u)))] $

3. Number equality: if $phi, varphi $ are formulae, then all closures of: $$(phi text { is 1-1 from } X to Y) wedge (varphi text { is 1-1 from } Y to X) to N(X)=N(Y)$$, are axioms.

4. Number inequality: if $phi$ is formula , then all closures of:$$Y^* subsetneq Y wedge (phi text { is 1-1 from } X to Y^*) to N(X) neq N(Y)$$, are axioms.

Define: $a leq b iff exists A,B (a=N(A) wedge b=N(B) wedge A subseteq B)$

5. Set formation: $forall X exists Y forall n (n leq N(X) to n in Y)$

Question: this theory copies the very basic notion of a natural number being an index of how many elements are there in a finite set. So, is it equi-interpretable with Peano arithmetic?