Can equinumerosity by defined in monadic second-order logic? Two properties (or concepts) $F$ and $G$ are said to be equinumerous if they have the same cardinality, i.e. if they can be put in one-to-one correspondence with each other.  This can be very easily defined in polyadic second-order logic: we just need to say that there exists a two-place relation $R$ such that $Rxy$ and $Rxz$ implies $y=z$, $Rxz$ and $Ryz$ implies $x=y$, $Rxy$ implies $Fx$ and $Gy$, $Fx$ implies that $Rxy$ for some $y$, and $Gy$ implies $Rxy$ for some $x$.  (I think that's right.)  My question is can we define equinumerousity in monadic second-order logic, i.e. without the use of relations?
If so, can we prove Frege's theorem in monadic second-order logic?  Also, are there other important notions which can only be defined in polyadic second-order logic?
Any help would be greatly appreciated.
Thank You in Advaance.
 A: Let $T$ be the monadic second-order theory of the successor relation.  Frege showed that the relation of being less than is definable in $T$.  On the other hand, according to Büchi's theorem $T$ is decidable; this implies that it is not the case that both addition and multiplication are definable in $T$.  
However, addition is definable in terms of equinumerosity and the relation of being less than, in particular like this:
$x$ is the sum of $y$ and $z$ if and only if the number of things less than $x$ but not less than $y$ is equal to the number of things less than $z$.
Moreover, in monadic second-order logic multiplication is definable in terms of addition[*].  Thus it cannot be that equinumerosity is definable in $T$.  So equinumerosity is not definable in monadic second-order logic. 
The argument from Buchi's Theorem to the undefinability of addition is due to Avron, 'Transitive closure and the mechanization of mathematics' (2002).  A discussion of the general topic of the question appears in Richard Heck's 'The logic of Frege's theorem'  (2011).

[*] Carl's comment below makes me realize that I'd been wrong to assume that this would be well-known.  Here's Avron's idea.
First, $x$ divides $y$ iff $y$ belongs to the smallest set containing zero which is closed under addition-by-$x$.
Second, $x=y^2$ iff $x+y$ is the least common multiple of $y$ and $y+1$.
Finally, $x=yz$ iff $(y+z)^2=y^2+z^2+2x$.
