Théorème de Lindström

En logique mathématique, le théorème de Lindström (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 : 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. 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. Il existe des variantes du théorème de Lindström pour des fragments syntaxiques de la logique du premier ordre.