Comparing cardinalities of sets in Peano? From comments in Pairing in Presburger arithmetic it looks like using Peano Arithmetic we can compare cardinalities of sets. How exactly to do this? 
 A: 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.
