Translating basic number theory to the monadic theory of the real line

Question

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) 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, 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.

Answer 1

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.

Answer 2

Disclaimer: I last seriously tackled any papers of Shelah over 20 years ago. There are conventions which puzzle me (and are probably important), but I am not reading the whole paper. Someone who has read it can probably explain the conventions and the reason for them.

Convention one. There are some pairs of symbols like I and I* and D and D* which may be related. One might stand for a subset of another perhaps,, or that there is a containment relationship. For now I pretend they are separate variables standing for subsets of the reals with I variables for intervals.

Convention two: in the key part of the construction, an equation is given for translating an atomic formula with relation symbol R_l, and another for the negation of an atomic formula with relation symbol R_l. However, I read it as saying use the first only if the subscript l is less than 0, and the other only if the subscript l is greater than or equal to zero. Perhaps it is important (since one is dealing with Skolemnization prior to this) to represent a relation in two ways, with a negative and with a positive index. I am unsure.

If I ignore these two conventions, I read the machine as a rather tedious and complex but straightforward transcription. Here is my take on it.

Back a couple pages (Definitions 7.1 and 7.2 for those of you following at home), Shelah defines a couple of families of formulae indexed by a parameter n, in the nomadic theory. Formula n for one family says there are n+1 disjoint sets Y_i which have magical properties in relation to the other sets in the formula. and formula n for the other family includes the formula n for the first family, plus a negation of that same formula but applied to a certain class of supersets. (I am mangling for simplicity; if you know the monadic theory, go read the actual definitions for yourself.)

In doing the construction, Shelah only seems to use members of either family with indices 0,1, and 2. I don't know why. However, much of the time, these members seem stand alone and do not have much to do with the relation symbols present on the relational number theory.

So now we come to the machine. The goal (for the theorem) is to take a sentence of relational number theory and do a Skolem normal form of it so it looks like AE matrix of atomic formulae and their negations with only relation symbols including equality (such as Matt F has provided), and then transform this into a sentence in the monadic theory so that the input is true in a certain model of relational number theory iff the output holds in something, probably a standard model of the monadic theory.

Let me handle the key parts of the machine backwards (and in doing so, attempt an answer to the question asked). Step (3) says write the Skolem form AE matrix as AE newmatrix, where newmatrix is a pattern that follows the pattern of matrix, but using and-or instead of or-and, and for each atomic/negatomic formula in the matrix, using a transformed portion of that piece. There is also a preamble in the formula that suggests to me a C-include file for stdio. (But I digress.)

Step (2) handles the transform negatomic formulae which is the negation of the transform for the atomic formulae. The surprise here is that this is for index l at least zero, where l is the index on the relation symbol.

Step (1) is the key to understand (which I don't) and handles the transform of an atomic formula, but this for relation symbols with negative index l. However, ignoring that, one creates a preamble, and uses psi_2 (from Definition 7.2), and other things which I am shaky on, and set variables that I will type as Qli, which is indexed using both l (for the lth relation) and i (for the ith variable in a relation with arity m(l)).

So I can answer the recent question: how are the transforms different? For the two sentences given above, syntactically because they use different sets of Qli: one uses a set for the S relation, and a different one for the P relation.

Step (0) is a monadic version of equality to stand in for the atomic formula x=y.

There is a lot more to the machine, and seems to depend on a certain precondition, but now I have enough to take a stab at what is going on.

Shelah is replacing relation symbols in the input formula by tuples of specialized variables, and these variables sit in the Q place in the two infinite families. The set Q in earlier lemmata and definitions suggest that there is a perfect set P which avoids Q (or has small intersection with Q) and P stands in a nice relation with other parameters in the formula. I'm thinking that Shelah replaces a relation in rational number theory (which is a subset or sub universe of a power of omega), with a nicely condition subset of (some power, perhaps of) the reals. To get his theorem (relational number theory is recursive in the .indicate theory of order), he chooses the Q to satisfy the preamble and to bear some resemblance to the relations on the number theory model to make the transform true iff the input sentence is true.

While I hope my take is helpful, a serious student of the paper should resolve the two conventions first and take their own stab at Theorem 7.10 and the machinery behind it.

Gerhard "Wants To Keep His Comments" Paseman, 2019.07.07.

(To Matt F : even if they seem disjointed. We can have moderators arbitrate if this is a big issue for you.)