Lecture 11 (6.1.97)
Previous lecture:
Lecture 10 ,
Overview ,
Course home page ,
Material of this and subsequent lectures:
- [EFT]
H.D. Ebbinghaus, J. Flum, Finite Model Theory,
Springer 1994, Chapter 6.2-4
Trakhtenbrots' Theorem
There is a vocabulary $\tau$ with at least one binary relation symbol
such that set of $\tau$-sentences which have finite models
is not computable (not even recursive enumerable).
- Repetition on Turing Machines.
- Assigning formulas to Turing machines.
- Reduction to the Halting Problem.
The complexity of the Meaning Function
- FOL has a LogSpace meaning function.
- SOL has a P-Space meaning function.
- Exist-SOL has an NP meaning function.
- IFP has an polynomial time meaning function.
Next lecture:
Lecture 12