Some notes on Finite Model Theory

It was with great appreciation that I began to read Ronald Fagin's explicitly personal introduction to Finite Model Theory of 1993. Fagin was then working at the IBM Almaden Research Center in San Jose, California, and presented his thoughts at the 3rd International Conference on Database Theory in 1990. Fagin bemoans that so many results are for infinite structures, when databases are all finite. Logic, developed to deal with the hard part of mathematics, the infinite (Gurevich) [p4], but too many of the results for infinite structures do not hold for the finite [ibid]. In practice, finite model theory mostly found application in computability with its connection to algorithmic questions of complexity [p4], which Fagin devoted a whole section (5) to, showing that the class of generalized spectra from his thesis work are the class NP (non-deterministic polynomial time), while spectra are the NE (non-deterministic exponential time) [p.10].

But Fagin correctly pointed out that databases are finite structures [4].

As an aside: The Humanities are in a very similar situation. Even the analysis of an absurdist play like Ionescu's mathematics Lesson with its ridiculously huge numbers does not require an infinite domain of discourse like ℕ. The number of humans and objects and locations and years that matter for Humanities research are all finite. Yes, time and distance are reals, but for the purposes of most arguments, nano-seconds and angstrom provide more resolution that our sources possible allow us to handle anyway. (In fact, the Humanities have the opposite problem that the amazing accuracy of GPS and Google Maps belies knowledge about the exact location of past events on our present-day maps that misleads; but that is a separate rant.)

For example, Fagin shows that taking ℒ to be a "recursive, finitely controllable set [i.e. either unsatisfiable or finitely satisfiable] of first order sentences", then the decision problem is decidable, because each sentence p is either finitely satisfiable or its negation (¬p) is, via the completeness theorem (3.1).