Comparing cardinalities of sets in Peano?

Question

From comments in Pairing in Presburger arithmetic it looks like using Peano Arithmetic we can compare cardinalities of sets. How exactly to do this?

Answer 1

There are a couple steps to this.

---

I'll first make things simpler by shifting attention from PA to PA$_{exp}$ - this is just like PA, but our language is expanded to include the binary function symbol "$exp$," our induction scheme is expanded to apply to all formulas in this larger language, and we add axioms saying that $exp$ behaves like it should (specifically: for all $a,b$ we have $exp(a,0)=1$ and $exp(a, b+1)=a\cdot exp(b)$). Once you understand how this version of the problem works, just observe that Godel's $\beta$ function lets us get away with only $+$ and $\times$.

---

Next, we need to decide how exactly we're going to represent finite sets in $\mathcal{N}=(\mathbb{N};+,\times,exp)$. There are many ways to do this; one way is to identify a number $a$ with the set $$set(a):=\{i: \mbox{ for some prime $p$, we have }p^i\vert a\mbox{ but }p^{i+1}\not\vert a\}.$$

Now the relation "$set(a)\subseteq set(b)$" is definable as

For each prime $p\vert a$ there is some prime $q\vert b$ such that for all $i$ we have $$p^i\vert a\iff q^i\vert b.$$

From this in turn we can define the relation "$set(a)=set(b)$," and finally define the canonical representative for a number $a$, $can(a)$, as the smallest $b$ such that $set(b)=set(a)$. It's now easy to check that

$\vert set(a)\vert=\vert set(a')\vert$ iff the primes dividing $can(a)$ are exactly those dividing $can(a')$

(the point being that when we pass from $x$ to $can(x)$, we use as few primes as possible and as small primes as possible). And all of this is definable in $\mathcal{N}$.

EDIT: To be super-explicit, here's how it all gets put together. We express "The set coded by $x$ is of strictly smaller cardinality than the set coded by $y$" as

For every $x'$ and $y'$, if $can(x,x')$ and $can(y,y')$ then every prime dividing $x'$ also divides $y'$ but there is a prime dividing $y'$ which does not divide $x'$,

where "$can(u,v)$" is the relation (intuitively meaning "$v=can(u)$") defined by

$subset(u,v)$ and $subset(v,u)$ and for all $w<v$ either $\neg subset(w,u)$ or $\neg subset(u,w)$,

where "$subset(m,n)$" is the relation (intuitively meaning "the set coded by $m$ is a subset of the set coded by $n$") defined by

for every prime $p$ dividing $m$ there is a prime $q$ dividing $n$ such that for all $i$ we have $p^i\vert m$ iff $q^i\vert n$.

All of this nests together to give a single, very long, first-order formula.

---

More generally, using $exp$ we can reason satisfactorily about finite sequences, by representing a finite sequence $$\langle a_1,..., a_n\rangle$$ by the number $$\prod_{0\le i\le n}p_i^{a_i+1},$$ where $p_i$ denotes the $i$th prime. (The "$+1$" is required to avoid ambiguity - think about what would happen if $a_n=0$.) The key step behind this is the prime counting relation, $$C(p,i)\equiv p\mbox{ is the $i$th prime};$$ this relation is definable in $\mathcal{N}$ as

There is some $n$ such that $(1)$ the power of $2$ in $n$ is $1$, $(2)$ the power of $p$ in $n$ is $i+1$, and $(3)$ for each prime $q<p$.

This winds up being incredibly useful, so while it's not needed here I think it's still worth mentioning.

---

Finally, note that rather than talk about provability in the theory PA$_{exp}$ I've really just talked about definability in $\mathcal{N}$ - in a particular application/analysis, we need to check that all the "relevant properties" of the coding we're using are actually provable in PA$_{exp}$. But this theory is so strong that this generally is basically immediate.