# 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.

• My intuition says no -- but note that it is not being monadic alone that is the problem: in monadic third order logic we can speak of sets of (unordered) pairs which is enough to define equinumerosity ... – Henning Makholm Dec 26 '13 at 22:00
• @HenningMakholm Yes, I think monadic $n+1$-st order logic can always interpret polyadic $n$-th order logic. – Keshav Srinivasan Dec 26 '13 at 22:06

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$.

• Thanks. Do you know of other notions which are only definable in polyadic second-order logic? – Keshav Srinivasan Dec 29 '13 at 1:57
• Perhaps "there are infinitely many"? Not sure though. – mmw Dec 29 '13 at 22:52
• Frege's definition of finite doesn't require polyadic second-order logic. – Keshav Srinivasan Dec 29 '13 at 23:13
• Hmmm. You mean the def in grundlagen? I.e., an object's bearing to zero the ancestral of the successor relation (or a concept's being such that the number of objects falling under it stands likewise to zero)? – mmw Dec 30 '13 at 0:29
• Yes, the ancestral is what I'm talking about. – Keshav Srinivasan Dec 30 '13 at 1:35