Here's the other half of the answer: an interpretation of PA in this theory.

If $a < b$ and $b < a$, then $a < a$, which by Connective implies $a \neq a$, which is a contradiction. So $<$ is asymmetric.

Consider an arbitrary number $n$. By the axiom of sets, the set of numbers that are less than or equal to $n$ exists (using a formula like $m = m$ as $\phi$), and by well-foundedness this has a minimum element $0$. For any number $k$, if $k < 0$, then $k < n$, so $k$ is in the set of numbers $\leq n$, and therefore $0 \leq k$ (by minimality of $0$ in the set), which is a contradiction. So $0 \leq k$ for all $k$.

Suppose that $n$ is the largest number. Then because $m \leq n$ for all $m$, we can, by Sets, construct the set of all numbers that are not elements of themselves. This is an element of itself iff it is not, which is a contradiction. So there is no largest number.

Since for any $n$ there is some $m > n$ (because $n$ cannot be the largest number), we can take the set of all numbers that are $\leq m$ and $> n$. This set is not empty, because $m$ is in it, so it has a minimum element $S(n)$. There is no number between $n$ and $S(n)$, because if there was it would be $< m$ and therefore in the set so $S(n)$ wouldn't be minimal. So every number has a successor.

For any two numbers $n,m$, the set $\{n,m\}$ exists. Suppose (wlog) that $n \leq m$. Then the set of numbers $\leq m$ that are either equal to n or equal to m contains both $n$ and $m$, since those are both less than $m$, and clearly doesn't contain anything else.

For two numbers $n,m$, define the pair $(n,m)$ to be $\{\{n\},\{n,m\}\}$, which exists by repeated applications of the above argument (constructing $\{n\}$ as $\{n,n\}$). If $(a,b) = (c,d)$, then either they both have only one element, in which case $a = b$, $c = d$, and $\{\{a\}\} = \{\{c\}\}$, which implies $a = c$ and therefore $b = d$; or they both have two elements (which implies $a \neq b$ and $c \neq d$), in which case $\{a\} = \{c\}$ (which implies $a = c$) and $\{a,b\}=\{c,d\}$ (which implies $b = d$); so either way, $a = c$ and $b = d$, so this is a pairing function.

Any number $n \neq 0$ is the successor of some other number. Take the set of numbers $\leq n$ that are less than n. This set is not empty because it contains $0$, so by finiteness, this set has a maximum element $m$. If $n < S(m)$, then $n$ is between $m$ and $S(m)$ which is impossible. If $S(m) < n$, then $S(m) < m$ by maximality of $m$ in the set of numbers less than $n$, which is impossible. So $n = S(m)$.

For any formula $\phi(n)$, if $\phi(0)$, and $\phi(n)$ implies $\phi(S(n))$ for all $n$, then $\phi(n)$ for all n. Suppose there is some number $k$ such that $\neg\phi(k)$. The set of numbers $\leq k$ for which $\phi$ is false is not empty (it contains $k$), so it has a minimum $x$. $x$ is not 0, because $\phi(0)$ and $\neg\phi(x)$, so it is the successor of some number $y$. If $\phi(y)$, then $\phi(S(y))$, but we know that isn't true. If $\neg\phi(y)$, then $x$ wasn't the minimum, because $y < x$. This is a contradiction.

Given number $n$ and $m$, the union of $n$ and $m$ exists: it is the set of numbers less than or equal to the maximum of the maximum element of $n$ and the maximum element of $m$, that are elements of either $n$ or $m$.

For a function $f$ (encoded as a formula $\phi(x,y)$ that represents $f(x) = y$), and numbers $n$ and $x$, there is a set $F_n$ with the properties that:

- $(0,x) \in F_n$
- For $k < n$, if $(k,y) \in F_n$, then $(S(k),f(y)) \in F_n$.
- For all $k \leq n$, there is a unique number $F_n(k)$ such that $(k,F_n(k)) \in F_n$.
- For all $k > n$ and all $y$, $(k,y) \notin F_n$.

For $n = 0$, $F_0 = \{(0,x)\}$. For $n = S(m)$, $F_n = F_m \cup \{(n,f(F_m(m)))\}$.

For any two sets $F_n$ and $F_m'$ satisfying these properties, $F_n(k) = F_m'(k)$ for all $k$, by induction: for $k = 0$, $F_n(0) = F_n'(0) = x$, and for $k = S(m)$, $F_n(k) = f(F_n(m)) = f(F_m'(m)) = F_m'(k)$.

Define $f^n(x)$ to be $F_n(x)$ for any $F_n$ (we know they all give the same answer). By property 1, $f^0(x) = x$, and by property 2, $f^{n+1}(x) = f(f^n(x))$.

Now we can define $n + m$ as $S^m(n)$, and $n \cdot m$ as $f^m(0)$ where $f(x) = x + n$. The axioms for the recursive definitions of $+$ and $\cdot$ follow immediately from the paragraph above.

Suppose that $S(n) = S(m)$, but $n \neq m$; wlog assume $n < m$. Then $S(n) \leq m$, but since $m < S(m)$, $S(n) < S(m)$, which is a contradiction. So $S$ is injective.

If $S(n) = 0$, then $n < 0$, which is a contradiction. So $0$ is not a successor.

I already proved that $0$ and successor exist, and induction, so that's all the axioms of PA.