Finite model theory

Go to home page

Finite variable logics

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
  1. 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.
  2. Some corrections and additions.  This appeared as Addendum to: Finite Variable Logics, Bull. Europ. Assoc. Theor. Comp. Sci. 52 (1994) p278.
  3. 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.

Logics and Complexity in Finite Model Theory

I Hodkinson
These are notes (13 pages) of a talk given in the Swansea finite model theory tutorial, 8-9 July 1996.