Methods for proving non FO definability

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

I'm having difficulties to prove that the subset of even numbers is not first-order definable in $(\mathbb{N},<)$. Any hint is welcomed!

More generally, what are usual techniques in order to prove that a subset is not FO-definable. I know one using isomorphism.

What are other methods?

-

3 Answers

One method is to use quantifier elimination. Note that 0 and $S(x)=x+1$ are definable in $M=(\mathbb N,<)$. The expanded structure $M'=(\mathbb N,<,0,S)$ is a model of the theory $T$ of a discrete linear order with zero and successor. You can show that every formula is in $T$ equivalent to an open formula (it suffices to prove it for formulas consisting of a single existential quantifier followed by a conjunction of atomic formulas and their negations), and this implies that every definable subset of $M$ is finite or cofinite. (And as a bonus, it shows that $T$ is complete.)

Another method is to use compactness. In this simple example, you can just take any elementary extension $M^*\succ M$ and an element $a\in M^*$ satisfying the alleged formula $\phi$ defining parity. The function $f$ which leaves $\mathbb N$ fixed and maps everyone else to its successor is an automorphism of $M^*$, but $\phi$ cannot be satisfied by two successive elements. In more complicated situations, one may need to take $M^*$ e.g. recursively saturated (or saturated in some larger cardinality) to define an automorphism by some sort of a zig-zag construction.

Yet another method is to use Ehrenfeucht–Fraïssé games (these are quite useful for showing undefinability of classes of finite structures, but often come handy in other situations as well). By induction on $k$, show that Duplicator has a winning strategy in $EF_k((M,a_1,\dots,a_n),(M,b_1,\dots,b_n))$ whenever the sequences $\vec a$, $\vec b$ are ordered in the same way, and for each $i,j$, the distances $a_i-a_j$ and $b_i-b_j$ are the same, or they are both large (bigger than $2^k$ or something like that). This implies that a fixed formula $\phi(x)$ cannot distinguish two large enough elements.

-

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.

Another proof is to use the theorem of McNaughton-Schutzenberger that a regular language can be defined in $FO(<)$ if and only if its syntactic monoid is aperiodic (satisfies $x^n=x^{n+1}$ from some $n$). $FO(\mathbb N,<)$ is the special case of a unary alphabet. The syntactic monoid of the even numbers is the cyclic group of order 2, which is not aperiodic. More generally, it follows from the McNaughton-Schutzenberger theorem that the only sets definable are finite or cofinite. See the book of Straubing on Automata, logic and circuit complexity for these kinds of things.

-

General methods

• Ehrenfeucht-Fraisse games
• The theorems of Hanf and Gaifman

You can prove, that the even numbers are not first order definable by gaifmans theorem: Suppose they were. By gaifmans theorem the definition is a boolean combination of basic local sentences. Choose an even and an odd number far away from 0 in terms of the locality of these sentences. Then they cannot distinguish these two numbers. Contradiction.

-

1
Locality theorems can be used to prove undefinability (they work basically as ready-made applications of Ehrenfeucht–Fraïssé arguments), but in this case, isn’t the Gaifman graph of $(\mathbb N,<)$ one huge clique? – Emil Jeřábek Oct 23 at 12:59
Oops. I confounded $(\mathbb N,&lt;)$ with $(\mathbb N,S)$ where $S$ is a successor relation. Sorry. – maxky Oct 24 at 8:25
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 33, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": false, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9320555925369263, "perplexity_flag": "head"}