# Is this theory of recursive counting equi-interpretable with PA?

To the theory presented in this link, add a two place function symbol $$\#$$ denoting a counting function on numbers in sets, to the list of primitives of that language, and add the axiom:

$$\#^K (x) = n \leftrightarrow [x=min(K) \land n=1] \lor [x \in K \land min(K) < x \land n= S[\#^K(P^K(x))]$$

Define $$P^K(x) = y \iff x \in K \land y \in K \land y < x \land \not \exists z \in K (y < z < x)]$$

Define Successor as: $$x=S(y) \iff y < x \land \not \exists z (y < z < x)$$

Define: $$x = min(K) \iff x \in K \land \forall y \in K (x \leq y)$$

Would the resulting theory be equi-interpretable with Peano arithemtic "PA"? And thus conservatively extends PA.

At a glance, the answer is yes.

As an upper bound on strength, the argument you give in your previous question works once we include $$\#$$.

The lower bound is then provided as follows: if $$M$$ is a model of PA, then $$M$$ equipped with its internally-finite sets "is" a model of your theory (we have to massage the language a bit of course). Here an internally-finite set is a set of the form $$\{x: n>x\wedge M\models\varphi(x)\}$$ for some formula with parameters $$\varphi$$ and some $$n\in M$$.

There is a subtlety with this lower bound: to prove comprehension, we need to show that something definable by quantifying over internally-finite sets is definable in the original sense. This follows from the following: for each formula $$\varphi(x; y_1,...,y_k)$$, PA proves the following:

For all $$a_1,...,a_k, n$$, there is a $$c$$ such that for all $$i$$ we have $$p_i\vert c\iff i

That is, in any model of PA, all the internally-finite sets are in fact quantifier-freely definable, and we can quantify over formulas of bounded quantifier complexity.

• Incidentally, the comprehension subtlety is something I failed to address in my answer to the OP's previous question. While I think all the claims there are indeed true, the argument is incomplete. Sep 20 '19 at 16:27