Methods for proving non FO definability - MathOverflow

Methods for proving non FO definability

2012-10-23T10:43:06Z

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?

Answer by maxky for Methods for proving non FO definability

2012-10-23T11:20:11Z

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.

Answer by Emil Jeřábek for Methods for proving non FO definability

2012-10-23T11:29:18Z

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.

Answer by Benjamin Steinberg for Methods for proving non FO definability

2012-10-24T02:42:17Z

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.