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[modifier | modifier le code]
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[modifier | modifier le code]
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[modifier | modifier le code]
- (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.
- (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 ).
- (en) « Lindström's theorem ».
- Johan Van Benthem et Balder Ten Cate, Lindström theorems for fragments of first-order logic, (lire en ligne).
