This theory is a theory of arithmetic having a last natural number that is not reachable from below by syntactical recursive iteration of the successor function. So it doesn't prove all rules of arithmetic, but it can do it for every writable natural in terms of recursive iterative succession starting from zero.
From what appears to me, the theory is consistent, since axioms 1 to 17 clearly has a model with its domain being $N^{<n} \cup P(N^{<n}) \cup N^{<n} \times N^{<n} \cup P(N^{<n} \times N^{<n})$, where $N^{<n}$ is the set of all naturals up to and including $n$. Now clearly any finite set of instances of the axiom schema 18 is consistent with 1-17. So by compactness of first order logic this theory is consistent.
This theory cannot prove all rules of arithmetic, it cannot prove Robinson's arithmetic $\sf Q$. So can it be complete?
Question 2: is this theory complete?
Question 3: what's the consistency strength of this theory?
EXPOSITION
Language: first order logic with identity
Extra-logical primitives: $0, k, \mathcal, S, \in, =, Nat, \langle, \rangle$
Where $0,k$ are constants representing the first and last natural numbers respectively.
$S$ stands for the partial one place function successor
$Nat$ stands for the predicate "Natural number"
$\langle, \rangle$ stands for the partial two place function "ordered pair"
$\in,=$ stand for set membership and equality relations respectively.
Axioms:
$\forall x \forall y \ [S(x)=y \to Nat(x) \land Nat(y)]$
$ Nat(0)$
$\not \exists n (S(n)=0)$
$\not \exists n (S(k)=n)$
$\forall n \neq k [Nat(n) \to \exists m (S(n)=m)]$
$\forall n \neq 0 [Nat(n) \to \exists m (S(m)=n)]$
$\forall a,b,c (S(a)=c \land S(b)=c \to a=b)$
Define: $ set(x) \iff \neg Nat(x) \land \not \exists a,b (x=\langle a,b \rangle)$
- if $\phi$ is a formula in which $x$ is not free, then:
$Ay (\phi \to Nat(y)) \to \exists \ set \ x \forall y (y \in x \leftrightarrow \phi)$
$\forall a,b,c,d (\langle a,b \rangle = \langle c,d \rangle \to a=c \land b=d)$
$\forall \ Nat \ x,y \exists z (z=\langle x,y \rangle \land \neg Nat(z))$
$\forall x,y,z [z=\langle x,y \rangle \to Nat(x) \land Nat(y)]$
EXTENSIONALITY: $\forall x,y (set(x) \land set(y) \to [\forall z( z \in x \leftrightarrow z \in y ) \to x=y])$
$\forall x [\neg set(x) \to \not \exists m (m \in x)]$
$\forall x,y [\forall m (m \in x \lor m \in y \to Nat(m)) \to \exists z (z= x \times y)]$
Where $x \times y$ is the Cartesian product of $x$ and $y$ defined as the $set$ of all ordered pairs $\langle a,b \rangle$ where $a \in x, b \in y$.
$\forall x [\forall y \in x (Nat(y)) \lor \forall z \in x \exists \ Nat \ a,b (z=\langle a,b \rangle)]$
SEPARATION: if $\phi$ is a formula in which $x$ doesn't occur free, then all closures of: $$\forall A \exists \ set \ x \forall y (y \in x \leftrightarrow y \in A \land \phi)$$; are axioms.
Define: $x=|a| \iff set(a) \land [(a=\emptyset \land x=0) \lor \exists y \ (y=\{1,..,x\} \land y \text { equinumerous } a)]$
Define: $x + y = z \iff \exists a,b,c: x=|a| \land y=|b| \land c= a \cup b \land a \cap b = \emptyset \land z=|c|$.
Define: $x * y = z \iff \exists a,b,c: x=|a| \land y=|b| \land c= a \times b \land z=|c|$
- INDUCTION: If $\phi$ is a formula, then:
$\phi(0) \land \forall \ Nat \ x < k \ (\phi(x) \to \phi(S(x))) \to \forall \ Nat \ y (\phi(y))$
Define recursively: For $n=0,1,2,..$
$S_0(0) = 0$
$S_{i+1}(0)=S[S_i(0)]$
- FURTHEST: For $i=0,1,2,3,....$
$k \neq S_i(0)$