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 munis 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 isomorphismes, renommage, clos par négation, conjonction, quantification existentielle, et expansion libre.
Variantes
Il existe des variantes du théorème de Lindström pour des fragments syntaxiques de la logique du premier ordre[4].
Notes et références
- (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)