nLab Lindström's theorem

Idea

Lindström’s theorem, or more precisely, Lindström’s theorems, are important results in abstract model theory due to the Swedish logician Per Lindström that give syntax-free characterizations of (classical untyped) first-order logic (‘syntax-free’ in the sense of not referring to the specific syntactic make up of the formulas).

The first theorem of Lindström

This (semantic) version of Lindström’s characterization is the best known and is usually meant when one speaks of ‘ the theorem of Lindström’ . It states that the validity of the downward Löwenheim-Skolem theorem (a sentence that holds in some model already holds in an at most countable model) and the compactness theorem (a set of sentences has a model if every finite subset has a model) characterizes up to expressive power standard first-order logic among all logics satisfying certain regularity conditions¹:

A gain in expressive power comes at the price of the loss of the validity of at least one of these theorems e.g. in second-order logic both theorems fail to hold.

Barwise (1977, p.45, cf. below) has called the first Lindström theorem

one of the first, and still most striking, results in abstract model theory

and VäänänenWesterståhl, p. 102 write that the

11-page paper (ed.: the authors refer to (#Lindstrom1969) ) is without a doubt Pelle Lindström’s most important single contribution to mathematical logic. In it, he uses a surprisingly general notion of a logic []

and go on to write VäänänenWesterståhl, p. 104

Lindström’s Theorem tells us that any proper extension of first-order logic has to detect something non-trivial about the set-theoretic universe. On the other hand, Lindström’s theorem reveals a deep robustness of first-order logic: it does not matter which way you define your syntax - as long as your semantics obeys certain basic principles [] you will get the same logic.

The second theorem of Lindström

The second Lindström theorem is of a more proof-theoretic nature and involves the concept of an effective logical system which draws on computability theory. It achieves a characterization of standard first-order logic in the class of all effective regular logical systems by the two properties of having an enumerable set of tautologies and validity of the Löwenheim-Skolem theorem.

Discussion

These results are sometimes viewed as an explanation of the privileged role that standard first-order logic plays in mathematical logic.

In the end, what lesson one draws from them (once the classical background assumptions accepted), largely hinges on how one assesses the role of the Löwenheim-Skolem theorem in mathematical logic, which enjoys a rather controversial status and has encountered skepticism already by Thoralf Skolem, the man himself. This scepticism is clearly present in the following comment by Hao Wang (1974, quoted after Flum(1985), pp.77-78):

..what is established (by Lindström’s theorem) is not that first-order logic is the only possible logic but rather that is the only possible logic when we in a sense deny the reality to the concept of uncountability …

Further alternative characterizations and extensions to other logics are known and constitute the field of abstract model theory.

Related concepts

• predicate logic

• higher order logic

• Löwenheim-Skolem theorem

• compactness theorem

• abstract model theory

References

• Per Lindström: On Extensions of Elementary Logic, Theoria 35 pp.1-11 (1969)

• Barwise (ed.): Handbook of Mathematical Logic , Elsevier Amsterdam 1977.

A textbook account of the results appears in:

• Ebbinghaus, Flum, Thomas : Einführung in die mathematische Logik, Wissenschaftliche Buchgesellschaft Darmstadt 1986.

A more recent overview of Lindström’s results can be found here:

• Jouko Väänänen, Lindström’s Theorem . Ms. (pdf)

• Jouko Väänänen, Dag Westerståhl: In Memoriam: Per Lindström. Theoria 76 (2010), 100-107

Further material (including a discussion of the broader implications of Lindström’s results for logic) can be found in

• Jörg Flum, Characterizing Logics , (pdf), chap. III of

• Barwise, Feferman (eds.), Model-theoretic Logics , Springer Heidelberg 1985 (toc)

---

1. These conditions formalize some classical background assumptions on logical systems like the restriction of semantics to standard set-theoretic structures and the existence of negation in the sense that for every sentence $\varphi$ there is $\psi$ such that $\mathfrak{A}\models\varphi$ iff not $\mathfrak{A}\models\psi$. ↩