Lecture 3 (4.11.96)

Previous lecture: Lecture 2 , Overview , Course home page ,

How to Prove Non-definability ?

We want to develop tools to prove non-definability for various logics. The main tool will be the Back and Forth Games or Ehrenfeucht-Fraisse Games in many variations.

The method was invented by Roland Fraisse, a French Mathematician, in 1954, and was popularized in its game theoretic form and extended by Andrzei Ehrenfeucht, a Polish Mathematician, in 1961. This method is the most powerful method known so far to prove both definability and non-definability results.

In this lecture we introduce the game theoretic form of the method for First Order Logic.

Introduction of the game $E_n^{\tau}({\cal A}_0, {\cal A}_1)$

Fix a vocabulary $\tau$, without function symbols.
Fix a natural number $n$.
Fix two $\tau$-structures ${\cal A}_0$ and ${\cal A}_1$.
There are two players: I (the spoiler) and II (the duplicator).
The game consists of $n$ moves.
In the $k$-th move
I chooses $i \in \{0,1\}$ and an element $a_k^i \in A_i$;
II chooses an element $a_k^{1-i} \in A_{1-i}$.
After $n$ moves we have $n$ pairs $(a_k^0, a_k^1), k \leq n$.
II wins, if the mapping $a_k^0 \rightarrow a_k^1, k \leq n$ is an isomorphism.

We looked at several examples to understand the game.

Winning strategies

Player I (II) has a Winning strategy for $E_n^{\tau}({\cal A}_0, {\cal A}_1)$ if he/she can win against all the choices of player II (I).

We say that ${\cal A}_0$ and {\cal A}_1)$ are n-equivalent, and write ${\cal A}_0 =_n {\cal A}_1)$ if II has a winning strategy for $E_n^{\tau}({\cal A}_0, {\cal A}_1)$.

Exercise: Show that this is an equivalence relation on the class of $\tau$-structures.

Quantifier rank

We define the quantifier rank $qr(\phi)$ of a first order formula $\phi$ inductively:

Atomic formulas have quantifier rank 0.
$qr(\exist v \phi)= qr(\forall v \phi) = qr(\phi)+1$.
$qr(\phi \and \psi) = qr(\phi \or \psi)= max( qr(\phi), qr(\psi)).
$qr(\not\phi)= qr(\phi)$.

THEOREM Let $\phi$ be a $\tau$-formula with quantifier rank at most $n$. If ${\cal A}_0$ and {\cal A}_1)$ are n-equivalent then ${\cal A}_0 \models \phi$ iff ${\cal A}_1 \models \phi$.

The proof was given in detail.

We use this theorem to show that several concepts of graphs and strings are not first order definable.

THEOREM Connectivity is not first order definable.

Next lecture: Lecture 4