Show that two structures are not distinguishable in first order logic. It is about $\mathbb{A}=\langle \mathbb{R}\times \mathbb{Z}, \le\rangle$ and $\mathbb{B}=\langle \mathbb{Q}\times \mathbb{Z}, \le\rangle$. We can use only formula, not set of formulas. $\le$ denotes linear order, which is lexycographic.

Examples of order: $(\frac12, 5) \le (\frac12 6)$
$(\frac13, 100000) \le (\frac12, -10000)$
I don't know how to define it more precisely. $\le$ denotes lexycographic linear order. Comparing first elements of pairs we use standard $\le$ in $\mathbb{Q}$ or $\mathbb{ R}$. At the same for second element of pair: standard $\le $ on $\mathbb{Z}$

It does mean that we should show that for each $n$ these both structures duplicator has always winning strategy in $n$ rounds.

I am going to use fact that $\langle \mathbb{R},\le\rangle $ and $\langle \mathbb{Q},\le\rangle$ are not distinguishable.

Lets give strategy for duplicator:
If spoiler chose $(a, b) $ ten duplicator also chose pair of form $(\_, b)$. Thanks to this, building isomorphism duplicator must worry only about relation in the same chain. In other words, this strategy that relation between elements from different chains will be prevented.

Now, if duplicator has to only win on single chain. Lets suppose that there is no winning strategy for duplicator. However, in this situation there is no strategy for simpler game: $\langle \mathbb{R},\le\rangle $ and $\langle \mathbb{Q},\le\rangle$.
We got contradiction.

Am I ok ?

  • $\begingroup$ What is the order ? It is a linear or partial order ? $\endgroup$ – Rene Schipperus Feb 13 '17 at 15:16
  • $\begingroup$ $\le$ denotes linear $\endgroup$ – user343207 Feb 13 '17 at 15:16
  • 1
    $\begingroup$ Please edit your question to give an explicit definition of the order on these sets. $\endgroup$ – Rene Schipperus Feb 13 '17 at 15:17
  • $\begingroup$ Ok, linear order is sufficient information >? $\endgroup$ – user343207 Feb 13 '17 at 15:18
  • $\begingroup$ Obviously not sufficient information. You didn't specify how to compare two elements from $\mathbb{A}$, for example. $\endgroup$ – user21820 Feb 13 '17 at 15:23

You seem to be using some "spoiler"/"duplicator" framework for your argument that is not common knowledge -- at least I have not heard about it before (but I'm not an expert in model theory either). So I can't say whether your argument works.

I can see a syntactic proof in the form of this general fact:

The first-order theory of total orders where every element has an immediate predecessor and an immediate successor is complete (and decidable).

Since $\mathbb A$ and $\mathbb B$ are both models of this complete theory (as is $(\mathbb Z,{\le})$), they are indistinguishable.

To prove the above fact, formulate the theory with an explicit function letter for the successor function. It then has quantifier elimination.

Namely, to eliminate the quantifier in $(\exists x)\varphi$ where $\varphi$ is quantifier-free, first rewrite $\varphi$ into disjunctive normal form, distribute the quantifier across the disjunctions, and now it is easy to eliminate it from each remaining conjunction of atoms. It is a bit tedious to handle $\neq$ atoms explicitly, but we can avoid that by rewriting $t_1\ne t_2$ to $S(t_1)\le t_2 \lor S(t_2)\le t_1$ during the DNF conversion.

  • 1
    $\begingroup$ The argument is probably related to Ehrenfeucht games? (I haven't read the post, but the terms feel right and the topic is right.) $\endgroup$ – Patrick Stevens Feb 13 '17 at 18:45
  • $\begingroup$ @PatrickStevens yes, EF games. What do you think about it ? $\endgroup$ – user343207 Feb 13 '17 at 19:19
  • $\begingroup$ @Henning, thanks for your answer. We know now that these two classes are not distinguishable, indeed. $\endgroup$ – user343207 Feb 13 '17 at 19:28
  • $\begingroup$ See math.cornell.edu/~mec/Summer2009/Raluca/lesson1.html for a quick introduction to EF games that I found after Haskell Fun told me about them. I also didn't know about it before. It's related to Cantor's back-and-forth method. Note that that website makes a mistake on one page but it can be fixed. $\endgroup$ – user21820 Feb 14 '17 at 13:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy