Finite model theory
Go to home page
I Hodkinson
Bull. Europ. Assoc. Theor. Comp. Sci. 51 (1993) 111--140
With addendum, volume 52
In this survey article, we discuss some aspects of finite variable logics.
We translate some well-known fixed-point logics into the infinitary logic
$\L^\omega_{\infty\omega}$, discussing complexity issues. We give a game characterisation
of $\L^\omega_{\infty\omega}$, and use it to derive results on Scott sentences.
In this connection we consider definable linear orderings of types realised
in finite structures. We then show that the Craig interpolation and Beth
definability properties fail for $\L^\omega_{\infty\omega}$. Finally we examine
some connections of finite variable logic to temporal logic.
Article history
- Original version: Finite variable logics,
Bull. Europ. Assoc. Theor. Comp. Sci. 51 (1993) 111--140.
This appeared as a guest article in Yuri Gurevich's column
in the Bulletin. It is written as a dialogue between the author and `Quisani',
a character invented by Gurevich.
- Some corrections and additions. This appeared as
Addendum to: Finite Variable Logics,
Bull. Europ. Assoc. Theor. Comp. Sci. 52 (1994) p278.
- Revised version (October 1996) (unpublished)
with corrections and additional material. For example, there are more details of the
Abiteboul--Vianu theorem, and more about Beth definability.
I Hodkinson
These are notes (13 pages) of a talk given in the Swansea finite model theory
tutorial, 8-9 July 1996.