Can you prove the Categoricity of Second-Order PA with monadic SOL?

Question

If I have understood things correct, you can express the axiomatisation of Second-Order Peano Arithmetic in Monadic Second-Order Logic: the axiom of induction quantifies over unary predicates only. So I am now wondering: can you also prove the categoricity of second-order PA in monadic SOL?

Answer 1

As Alex Kruckman comments, it's not clear exactly what you're asking. However, there is a general fact that is likely to resolve whatever question is being asked here:

In the context of $\mathfrak{N}=(\mathbb{N}; +,\cdot)$, monadic second-order logic is as powerful as full second-order logic.

The reason for this is that $\mathfrak{N}$ has a (first-order) definable tupling function - for example, $(x_1,...,x_n)\mapsto \prod_{1\le i\le n}p_i^{x_i+1}$ where $p_i$ denotes the $i$th prime does the job.

• The "$+1$" in the exponent is to handle the situation where $x_n=0$; otherwise, we'd have trouble distinguishing $(x_1,...,x_n)$ from $(x_1,...,x_{n-1})$. Moreover, recall that the above is first-order expressible over $\mathfrak{N}$; if you're not familiar with this argument, you may want to look at Godel's $\beta$ function/lemma instead.

This lets us can convert finite-arity relations to sets as follows: for $R\subseteq\mathbb{N}^n$ we let $$Set(R)=\{\prod_{1\le i\le n}p_i^{x_i+1}: (x_1,...,x_n)\in R\}.$$ And we can use this translation in turn to assign to each second-order formula $\alpha$ a monadic second-order formula $\hat{\alpha}$ which is logically equivalent to $\alpha$ over $\mathfrak{N}$.

For example - and using capital letters for relation variables, with superscripts indicating arity - given $$\alpha\equiv \forall X^2\forall y_1,y_2(X^2(y_1,y_2)\rightarrow Y^3(y_1,y_2,z))$$ the associated monadic formula would be $$\hat{\alpha}\equiv \forall X^1\forall y_1,y_2(X^1(2^{y_1+1}3^{y_2+1})\rightarrow Y^1(2^{y_1+1}3^{y_2+1}5^{z+1})))$$ (actually that's just an abbreviation for it, but it's not hard to fully unwind this).

So basically anyting full second-order logic can do with $\mathfrak{N}$, monadic second-order logic can do as well.

---

There are a couple subtleties to note here:

• First, the translation above also has a negative aspect: while sometimes monadic second-order logic is substantially "tamer" than full second-order logic, the translation above shows that this is not the case with respect to $\mathfrak{N}$. In particular, there's no good proof system for monadic second-order logic over $\mathfrak{N}$.

• Second, note that the above really only used the existence of a definable tupling function. Moreover, all we really needed was a definable pairing function (since such can be iterated to give definable tupling functions). So the above translation works over any structure with such an operation. On the other hand, since pairing functions are binary functions - or, thought of as relations, ternary relations - we can't "directly introduce" one via a monadic second-order quantifier in general. So