I think I understand how this begins now. The key definition is that:
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)$
or for these purposes
an $\omega$-model for the language $(R,S)$ is a model $M$ such that $(|M|,R)$ is isomorphic to $(\omega, x +1=y)$
This is hidden inside the definition of a particular set, in the middle of theorem 7.10, at the top of page 415; furthermore, the language is not specified in the paper. But once I figured that out, I could make sense of the rest of the argument.
Consider the sentence $\theta$: $$\exists m,n\, (2m=2n+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 Sabc \rightarrow Sade) \\ &\wedge\,(Sabc \wedge Sabd \rightarrow c=d)\\ \wedge\, \exists m,n,u,v\, &(Smmu \wedge Snnv \wedge Ruv) \end{align}
The paper does not specify this use of these clauses, but in an $\omega$-model they are enough to determine the addition relation completely. In particular, in an $\omega$-model, the first two clauses are enough to determine that any two elements can be added.
We transform $\theta$ further into $G_1(\theta)$: $$\forall a,b,c,d,e\, \exists m,n,u,v\,$$ $$\Big((Sa0a \wedge Smmu \wedge Snnv \wedge Ruv \wedge \neg Sabc)$$ $$\vee\ (Sa0a \wedge Smmu \wedge Snnv \wedge Ruv \wedge \neg Rbc \wedge \neg Sabd)$$ $$\vee\ (Sa0a \wedge Smmu \wedge Snnv \wedge Ruv \wedge \neg Rde \wedge \neg Sabd)$$ $$\vee\ (Sa0a \wedge Smmu \wedge Snnv \wedge Ruv \wedge Sade \wedge \neg Sabd)$$ $$\vee\ (Sa0a \wedge Smmu \wedge Snnv \wedge Ruv \wedge \neg Rbc \wedge c=d)$$ $$\vee\ (Sa0a \wedge Smmu \wedge Snnv \wedge Ruv \wedge \neg Rde \wedge c=d)$$ $$\vee\ (Sa0a \wedge Smmu \wedge Snnv \wedge Ruv \wedge Sade \wedge c=d)\Big)$$
Now 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.
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.
As warnings for the rest of the procedure:
- Step (1) seems to have a typo, where $l<0$ should be replaced by $l>0$
- Steps (1), (3), (4) refer to $\psi$, which is defined on p. 413 using the definition of $\theta$ on p. 411.
- Step (4) seems to be defining $\psi$ as $\alpha \wedge \beta \wedge \gamma \wedge \delta \wedge \epsilon$, even though the clauses of the conjunction are interrupted by another definition.