Summary of Lectures: 236331-2018

Projects

Lectures 1 and 2

• Outline of the Course
• SOL and its fragments
• Definability
• Many examples

Lectures 3 and 4

• Non-definiability
• Pebble games and Hintikka formulas

Lectures 5 and 6 and 7

• Disjoint unions and concatenation
• Finite Automata
• Regular languages
• Buechi-Elgot-Trakhtenbrot Theorem
• Weighted automata

Lecture 8 and 9 and 10

• The complexity of model checking for fragments of SOL (upper bounds)
• Translation schemes and the Feferman-Vaught Theorem
• Without slides (on the white board):
  How to define SAT in MSOL.
  Introducing translation schemes via interpreting the complex numbers in the reals, and the natural numbers in the reals with the trigonometric function sin.

Lecture 11 and 12 and 13

• To be posted

Challenge

• For FOL it should be doable.
• For MSOL seems a good research project.
• For SOL this would separate the polynomial hierarchy PH from PSpace and would be a major break through.

Additional proofs not (yet) on the slides

1. SOL does not satisfy FV for rich disjoint unions
2. Prove pumping lemma using Hintikka formulas
3. In Libkin, Elements of Finite Model Theory, Chapter 7, Proposition 7.12 it is shown that two sets of size bigger than $2^k$ cannot be distinguished by MSOL formulas of quantifier rank less than $k$. Hence there is exactly one Hintikka formula of MSOL with quantifier rank $k$ which has infinitely many models over the empty vocabulary. The proof use the Pebble Games and describes the winning strategies explicitely. The same can also be obtained from an old result of T. Skolem using quantifier elimination for MSOL over the empty vocabulary: Let $L_n(X)$ be the formula which says that $X$ has at least $n$ elements. Then every MSOL formula is equivalent to a boolean combination of formulas of the form $L_n(X)$ for suitable chosen variables $X$. See here.

   Links

   • Link to catalogue of graph properties