What corresponds to $\forall m\forall n(2m \neq 2n+1)$ or $\forall p\forall q(p^2 \neq 2q^2)$ in the monadic theory of the real line?


[Shelah (1975)](https://www.jstor.org/stable/1971037?seq=1#page_scan_tab_contents) proved that arithmetic can be reduced the monadic theory of the real line. The paper gives a procedure to input a sentence of first-order arithmetic, and then output a sentence with the same truth value in the structure $\{\mathcal{P}(\mathbf{R}), \subset, <\}$, where $<$ is a version of the order that applies to singleton sets. But the procedure does not do this via an interpretation of one theory in the other.


What does this procedure give for simple sentences?


The procedure is on pp. 415-416 of Shelah's paper, but I can't make sense of it. Gurevich (1985), as linked to [here](https://mathoverflow.net/questions/332867/monadic-second-order-theories-of-the-reals), gave a similar procedure interpreting arithmetic in the monadic second-order theory of the Cantor set, but I can't make sense of that either. What do these procedures do with addition and multiplication? I'm hoping that someone with more experience or skill reading Shelah can clarify.


*To clarify:* The algorithm (or perhaps, partially-described algorithm) would begin with these statements in the equivalent relational forms $$\forall m,n,u,v (\neg Smmu \vee \neg Snnv \vee \neg S1uv)$$ $$\forall p,q,u,v (\neg Pppu \vee \neg Pqqv \vee \neg P2uv)$$ where $S$ and $P$ are symbols for the relations of sum and product. It remains unclear what the algorithm does with $S$ and $P$, or indeed how the algorithm treats these two sentences differently at all.



Translating basic number theory to the monadic theory of the real line
Consider the sentence $\theta$:
$$\exists m,n\, (2n=2m+1)$$
This is the negation of the first sentence in the above question. In relational form this is
$$\exists m,n,u,v\, (Smmu \wedge Snnv \wedge Ruv)$$
where $Sabc$ is the relation for $a+b=c$ and $Ruv$ is the relation for $u+1=v$.


**To find out whether $\theta$ is true arithmetically,** we can incorporate clauses for the Peano definition of addition and the uniqueness of addition, and then ask whether there is an $\omega$-model for the sentence:


\begin{align}
\forall a,b,c,d,e &(Sa0a\\
&\wedge\, (Rbc \wedge Rde \wedge Sabd \rightarrow Sace)
\\
&\wedge\,(Sabc \wedge Sabd \rightarrow c=d))\\
\wedge\, \exists m,n,u,v\, &(Smmu \wedge Snnv \wedge Ruv)
\end{align}


**The key definition** of an $\omega$-model is "an $\omega$-model for the language $(R\_1, \ldots R\_n)$ is a model $M$
such that $(|M|,R\_1)$ is isomorphic to $(\omega, x +1=y)$". In this case we take $R\_1$ to be the above $R$, and $R\_2$ to be the above $S$, though this is not specified in the paper, and the whole definition is hidden inside the definition of a particular set, in the middle of theorem 7.10, at the top of page 415.


The advantage of using an $\omega$-model is that in an $\omega$-model the clauses above are enough to determine the addition relation completely, and to determine that any two elements can be added. Again, this is the only way I see to make sense of the argument, even though the paper does not specify this use of those clauses.


**So the difference in the treatment of the two original sentences** is that the procedure for the first only needs to incorporate the Peano definition of addition, and the procedure for the second needs to incorporate the Peano definitions of both addition and multiplication.


To continue with the procedure for $\theta$, we transform it further into prenex form for $G\_1(\theta)$. (The paper also says to put the quantifier-free portion into $\bigvee\_i \bigwedge\_j$ form, but that does not seem necessary.) Then we can presumably apply the rest of the procedure to calculate $G\_2(\theta)$, $G\_3(\theta)$, and finally the desired $G(\theta)$ in the language of the monadic theory of order. I haven't done so yet.


I also see a few noteworthy items in the rest of the procedure:


* Step (1) seems to have a typo, where $l<0$ should read $l>0$.
* Steps (1), (3), (4) refer to $\psi$, which is defined on p. 413 using the definition of $\theta$ on p. 411.
* Step (3) seems to have a typo, where $\bigwedge\_i \bigvee\_j$ should read $\bigvee\_i \bigwedge\_j$ as in the definition of $G\_1$.
* Step (4) seems to define $\chi^\*$ as $\alpha \wedge \beta \wedge \gamma \wedge \delta \wedge \epsilon$, even though the clauses of the conjunction are interrupted by a sentence with another definition.
* Step (5) refers to quantifying over $X\_0, \ldots, Q\_l^i, \ldots$, which does not mean quantifying over $X\_0, X\_1, X\_2, \ldots$; it means quantifying over $X\_0, Q\_1^1, \ldots, Q\_l^i, \ldots, Q\_{n(2)}^{m(n(2))}$.


The density of confusing exposition in this section is remarkable.


