Lecture 5 (18.11.96)

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

How to Prove Non-definability ? (Continuation)

Back and Forth Games or Ehrenfeucht-Fraisse Games for Monadic Second Order Logic (MSOL) and Second Order Logic (SOL). Two $\tau$-structures $\cal A$ and $\cal B$ are MSOL-n-equivalent if player II has a winning strategy in the MSOL game of n moves on $\cal A$ and $\cal B$.

We looked at more examples to understand the game.
Examples: We analized the cases of the

empty vocabulary;
vocabularies with a finite number of unary predicates;
finite linear orders.

for MSOL.

Proposition Connectivity is MSOL definable on graphs.

THEOREM Evenness is not MSOL definable on ordered graphs, but is SOL definable, also over the empty vocabulary.

Remark: Over the empty vocabulary, it is SOL expressible that the cardinality of a structure is a prime number.

THEOREM Over words in $\{a,b\}^*$ the language $a^nb^n$ is not MSOL definable.

We actually prove an analogue of the pumping lemma for MSOL: Lemma: given for words u, v_1, v_2 and w such that v_1 and v_2 (as structures) are MSOL-n-equivalent, then the concatenated words uv_1w and uv_2w are MSOL-n-equivalent as structures.

Exercise: Derive the pumping lemma for v_1, v_2 words over the one-letter alphabet for MSOL-definable languages.

THEOREM The class of ordered graphs < V, E, R_< > with hamiltonian paths HAMP (cycles HAMC) is not MSOL definable.
Proof: First we observe that a bipartite graph has a hamiltonian cycle (HAMC) iff both sides have the same cardinality.
Next we observe that, if HAMC were definable over ordered graphs, then the language $a^nb^n$ would be MSOL definable too. This is a first example of a logical reduction .
Last we observe that HAMC is MSOL definable iff HAMP is MSOL definable.

Remark: HAMP is SOL definable, even on unordered graphs. HAMP is MSOL definable on graphs < A, P_V, P_E, R(v_1,e,v_2) > where the universe consists of vertices and edges.

Exercise: Is planarity MSOL definable on unordered (ordered) graphs ?

We introduce the cartesian product of two $\tau$ structures $\cal A \times \cal B$. We also introduce the disjoint union of a $\tau_1$ structure $cal A$ and $\tau_2$ structure $cal B$, denoted by $\cal A \sqcup \cal B$.

THEOREM Let both ${\cal A}_0$ and ${\cal A}_1$ and ${\cal B}_0$ and ${\cal B}_1$ be FOL-n-equivalent.
Then ${\cal A}_0 \times {\cal B}_0$ and ${\cal A}_1 \times {\cal B}_1$ are FOL-n-equivalent and ${\cal A}_0 \sqcup {\cal B}_0$ and ${\cal A}_1 \sqcup {\cal B}_1$ are FOL-n-equivalent.

THEOREM Let both ${\cal A}_0$ and ${\cal A}_1$ and ${\cal B}_0$ and ${\cal B}_1$ be MSOL-n-equivalent. Then ${\cal A}_0 \sqcup {\cal B}_0$ and ${\cal A}_1 \sqcup {\cal B}_1$ are MSOL-n-equivalent.
For the cartesian product MSOL-n-equivalence is not preserved.

Next lecture: Lecture 6