Are PA and Counting Theory synonymous\bi-interpretable?

Question

The following question is whether $\sf PA$ is synonymous or even bi-interpretable with a theory about counting objects in finite sets.

Counting Theory:

$\textbf{Logic:}$ Bi-sorted first order logic with equality. Lower cases stand for numbers, upper cases for sets of numbers.

$\textbf{Extralogical Primitives: } <, \in, \#$

Syntax: $<$ only occurs between lower cases, $\in$ from lower to upper case. $\#$ a total binary function whose first argument is a lower case and the second argument is an upper case and the value is a lower case, so $\#(x,S)=y $ is to be read as: the count of $x$ in $S$ is equal to $y$.

Define: $x > y \iff y < x$

Define: $x \leq y \iff x < y \lor x=y$

Define: $x \not > y \iff \neg \, x > y$

$ \textbf{Axioms:}$

• $ \textbf{Sorting: } x \neq Y$

• $ \textbf{Order:} \ x < y < z \to x < z \land x \neq y$

• $ \textbf{Finiteness:} \ y \in X \to \exists \, l,u \in X \forall m \in X : l \leq m \leq u $

• $\textbf{Sets: } \forall n \exists! X \forall m (m \in X \leftrightarrow m \not > n \land \phi)$, if $X$ is not free in formula $\phi$

• $\textbf {Counting: } \\ x \in S \to \# (x,S)= \sup^+ \{\# (y,S) \mid y \in S \land y < x \} \\ x \notin S \to \#(x,S)=0$

Where: $\sup^+ X = y \iff \\ \forall z: (\forall m \in X \, (m < z) \land z > 0) \leftrightarrow y \leq z $

• $\textbf{Multiplicity: } \exists x: x=x \land \forall x \exists y: x < y$

Define: $\operatorname {Count}(S)=\{\#(x,S) \mid x \in S \}$

Now we can define the cardinality operator on sets $||$ as:

$|S|= \sup \operatorname {Count}(S)$

Where: $\sup X = y \iff \forall z: \forall m \in X \, (m \leq z) \leftrightarrow y \leq z $

Having cardinality defined we can easily define addition $a + b=c$ as $c$ being the cardinality of the set union of some set of cardinality $a$ and some disjoint set from it of cardinality $b$. Mulitplication $a \times b=c$ is definable also, as the supermum of a set of cardinality $b$ whose first element is $a$ and such that for each element $k$ of it the element of the next higher count in it is $k+a$. The successor function is the $+1$ function, and all rules of $\sf PA$ would follow. For the other direction $\sf PA$ can interpret this theory by having the naturals be the odd numbers, and have the sets of the naturals to be the even numbers that are doubles of numbers that have binary expansions only containing $1$ at odd positions, then we use the Ackermann interpretation to define $\in$. So for example $\{1,3\}=101 \times 10; \{3,5\}= 10100 \times 10$ [to avoid confusion the zero-one numbers are in binary]. We keep equality relation, the $<$ relation is the usual defined $<$ of $\sf PA$ but restricted to the odds, and $\#(x,S)$ is definable recursively in $\sf PA$ of course here restricted to odds and the abovementioned evens standing for sets of them.

Can $\sf PA$ and Counting Theory be synonymous? Or even bi-interpretable?

To the vulgar eye of mine, Counting Theory is no less a natural theory of arithmetic than $\sf PA$, since our basic understanding of the naturals actually arose from counting the order of objects in finite sets. Counting by fingers is a life example of it! So, it would be nice to know if these two natural theories of arithmetic are synonymous.

PS: a definition of the $\in$ relation of $\sf CT$ in $\sf PA$ that ranges over all evens was given in the answer by Lumsdaine as: the number $n \in_G m$ , if and only if, $m$ is even and the $[(n-1)/2 \, +1]^{th}$ digit of the binary representation of $m$ is $1$. Where the $i^{th}$ digit is the coefficient of $2^i$. This way $n$ must be an odd number to be an $\in_G$ element of $m$.

Answer 1

For bi-interpretability, it seems like you’ve mostly answered the question yourself. You’ve described interpretations $\newcommand{\PA}{\mathsf{PA}}\newcommand{\CT}{\mathsf{CT}}\newcommand{\S}{\mathsf{S}}\newcommand{\N}{\mathsf{N}}F : \PA \to \CT$, interpreting the base sort $\N_\PA$ of $\sf PA$ as the “numbers” $\N_\CT$ of $\CT$, and $G : \CT \to \PA$, interpreting $\N_\CT$ as odd numbers of $\PA$ and the “sets” $\S_\CT$ as the even numbers, with binary expansions for membership in the usual way.

(Edit: I slightly misread your description, so my $G$ is actually slightly different from what you gave. An even number represents the set of positions of 1’s in its binary expansion — but do we count positions with the numbers of $\CT$ or of $\PA$? I mean the former; so the membership of $\CT$ is interpreted as the $\PA$-predicate “$n \in_G m$” defined as “$n = 2k+1$, $m$ is even, and the $(k+1)$st binary digit of $m$ is $1$.” Digit positions are indexed from 0, so the $i$th digit is the coefficient of $2^i$.)

The composite $G \circ F : \PA \to \CT \to \PA$ reinterprets $\PA$ in itself as the odd numbers with the standard order; it’s easy to see this is definably isomorphic to the identity interpretation.

So it remains to show $F \circ G : \CT \to \PA \to \CT$ is definably isomorphic to the identity interpretation of $\CT$. $F \circ G$ reinterprets numbers as odd numbers, and sets as even numbers. Assuming $\CT$ proves full induction (which I don’t immediately see how to show, but you seem to claim it in the question), it’s not hard to define the intuitively-clear isomorphism between this and the identity interpretation. Numbers map to corresponding odd numbers by doubling, of course; then we can map sets to their codes $S \mapsto 2 \sum_{i \in S} 2^i$ by induction on cardinality $|S|$, and conversely we map even numbers to the sets they code by comprehension, $2k \mapsto \{ i < k \mid \lfloor k/2^i \!\rfloor\ \text{odd} \}$.

So this gives a conceptually clear bi-interpretation. But it turns out that this can be automatically bumped up to a synonymy, by Corollary 5.3 of Friedman–Visser 2014, When bi-interpretability implies synonymy, since our $G$ is in their terminology “direct” — it interprets the total domain of $\CT$ (i.e. the union $\N_\CT \cup \S_\CT$) precisely as the total domain of $\PA$, $\N_\PA$. And chasing through their proof, it shows us how to define the synonymy concretely: We keep $G$ as is, and modify $F$ to an isomorphic interpretation $F' : \PA \to \CT$, which interprets $\N_\PA$ not just as the numbers $\N_\CT$ but (as required for directness) as the total domain $\N_\CT + \S_\CT$, and then interprets the structure of $\PA$ on that by transporting the arithmetic structure of $\N_\CT$ along the definable isomorphism $(\N_\CT + \S_\CT) \cong \N_\CT$ that we constructed above to show that $F \circ G \cong \mathrm{id}_{\CT}$.