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<n\wedge \varphi(i; a_1,...,a_k).$$

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.

  • $\begingroup$ 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. $\endgroup$ Sep 20 '19 at 16:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.