Théorème de Lindström

En logique mathématique, le théorème de Lindström[1],[2] (publié en 1969 par le logicien suédois Per Lindström) caractérise la logique du premier ordre comme suit : en gros, il s'agit de la logique qui possède le théorème de compacité et le théorème de Löwenheim-Skolem descendant. L'énoncé du théorème est le suivant[3] :

Soit L une logique abstraite (i.e. qui vérifie certaines conditions, voir plus loin) qui est plus expressive que la logique du premier ordre. Les deux propriétés suivantes sont équivalentes :

  • le théorème de compacité et le théorème de Löwenheim-Skolem descendant sont vrais pour la logique L ;
  • L est d'expressivité égale à la logique du premier ordre.

Conditions vérifiées par une logique abstraite

Plus précisément, une logique abstraite est un ensemble de formules muni de conditions de vérité pour interpréter les formules dans des structures. De plus, on demande à cet ensemble de formules d'être clos par isomorphisme, renommage, négation, conjonction, quantification existentielle et expansion libre.

Variantes

Il existe des variantes du théorème de Lindström pour des fragments syntaxiques[pas clair] de la logique du premier ordre[4].

Notes et références

  1. ↑ (en) Per Lindström, On Characterizing Elementary Logic, Springer Netherlands, coll. « Synthese Library », (ISBN 9789401021937 et 9789401021913, DOI 10.1007/978-94-010-2191-3_12, lire en ligne), p. 129–146.
  2. ↑ (en) Per Lindström, « On Extensions of Elementary Logic », Theoria, vol. 35,‎ , p. 1–11 (ISSN 1755-2567, DOI 10.1111/j.1755-2567.1969.tb00356.x, lire en ligne, consulté le ).
  3. ↑ (en) « Lindström's theorem ».
  4. ↑ Johan Van Benthem et Balder Ten Cate, Lindström theorems for fragments of first-order logic, (lire en ligne).