Can WS1S encode any power of $2$?

Question

I was wondering if I can write in weak monadic second order theory of one successor can encode the number $2^x$ for a variable $x$.

Answer 1

I'm interpreting your question to be "is there a formula $\phi(x,y)$ in the language of WS1S that holds iff $y = 2^x$"? If so, the answer is "no". Let me know if I haven't interpreted this correctly.

Given a tuple of finite subsets of the natural numbers $X_1,\ldots,X_n$, we can encode it as word $w$ on the alphabet of subsets of $\{1,\ldots,m\}$ to feed into a finite automaton. Specifically the $i$th character of the word $w$ is the set of all $k$ such that $i \in X_k$. First order elements should be converted to their singletons, then encoded.

For every formula $\varphi(X_1,\ldots,X_m)$ in the language of WS1S, there is a corresponding automaton on the alphabet of subsets of $\{1,\ldots,m\}$ that accepts the encoding of $X_1,\ldots,X_m$ iff $\varphi$ holds of $X_1,\ldots,X_m$.

As such, if $\varphi$ encodes a function from $X_1,\ldots,X_{m-1}$ to $X_m$ (i.e. for every $X_1,\ldots,X_{m-1}$ there is a unique $X_m$ such that $\varphi(X_1,\ldots,X_m)$), then there is a constant $k$ (the number of states of this automaton) such that for any $X_1,\ldots,X_{m-1}$, the maximum element of $X_m$ is at most $k$ more than the maximum element of the $X_1,\ldots,X_{m-1}$. This follows from the pumping lemma applied to the region between the maximum element of the inputs and the maximum element of the output.

A similar argument applies to show there is no formula $\varphi$ representing the function $x \mapsto 2^x$.