In Search of New Lindström Theorems
Jouko Väänänen, University of Helsinki and ILLC, University of Amsterdam
The combination of Löwenheim-Skolem Theorem and Compactness Theorem limits the expressive power of a logic to that of first order logic. This maximality principle is the famous Lindström Theorem for first order logic. It reveals that first order logic is at an optimal point of balance: by adding expressive power to it one necessarily loses model-theoretic properties. Soon after Lindström’s result, the question was raised, whether there are other logics at a similar point of equilibrium. More precisely: are there strict strengthenings of first order logic satisfying a Lindström-type characterization? Despite the naturality of this question, it remained unanswered, until recently.
In 2012 Saharon Shelah offered a solution to this problem in the form of a new infinitary logic. It has a Lindström-type characterization in terms of model-theoretic properties combining weak forms of Compactness and a Löwenheim-Skolem type property. In all known cases, a proof of a Lindström-type characterization automatically gives a proof of Craig Interpolation. This is the case for Shelah’s logic, too. There is, however, one aspect where Shelah’s logic seems to be rather weak: the syntax. The logic is derived from a game, in the sense that a sentence is, by definition, a class of structures, closed under a certain Ehrenfeucht-Fraïssé type of a game. This results in the absence of a syntax defined in such a way that the set of all formulas could be obtained by closing the set of atomic formulas under negation, conjunction, quantifiers, and possibly other logical operations. The lack of syntax complicates further study of it and logics in its neighborhood. In the present talk, we address the general question of deriving a syntax from a game, and the more localized question of finding a syntax for Shelah’s logic. Partial answers are provided to both questions. This is joint work with Andres Villaveces and Siiri Kivimäki.