Théorème de Löwenheim-Skolem
En théorie des modèles, le théorème de Löwenheim-Skolem, énoncé par Leopold Löwenheim en 1915 et démontré entièrement en 1920 par Thoralf Skolem, établit que si un ensemble de formules closes de la logique du premier ordre admet un modèle infini, alors il admet un modèle de n'importe quelle cardinalité infinie supérieure ou égale au cardinal du langage et de l'ensemble de formules. Le résultat est souvent présenté sous la forme de deux théorèmes : le théorème de Löwenheim-Skolem ascendant et le théorème de Löwenheim-Skolem descendant.
Formulations
[modifier | modifier le code]Cas d'un langage dénombrable
[modifier | modifier le code]Considérons que le langage est dénombrable (c'est souvent une hypothèse raisonnable notamment en informatique et c'est une hypothèse faite dans certains ouvrages de logique en informatique[1]). Le théorème de Löwenheim-Skolem peut alors s'énoncer par : si une formule est satisfaisable alors elle admet un modèle au plus dénombrable[1]. Ou plus généralement : si un ensemble T (dénombrable) de formules closes est satisfaisable alors T admet un modèle au plus dénombrable[1].
Théorèmes de Löwenheim-Skolem pour tout cardinal
[modifier | modifier le code]![](http://upload.wikimedia.org/wikipedia/commons/thumb/6/66/Lowenheim-skolem.svg/440px-Lowenheim-skolem.svg.png)
Soit σ une signature pour un langage du premier ordre qui contient l'égalité. Soit κ un cardinal infini tel que |σ| ≤ κ. Soit M un modèle infini sur la signature σ. Alors il existe un modèle N de cardinal κ tel que :
- (théorème de Löwenheim-Skolem descendant) N est une sous-structure[2] élémentaire (de) de M si κ < |M| ;
- (théorème de Löwenheim-Skolem ascendant) M est une sous-structure élémentaire de N si κ > |M|.
En particulier, M et N sont alors élémentairement équivalents[3].
Idées des démonstrations
[modifier | modifier le code]Théorème de Löwenheim-Skolem ascendant
[modifier | modifier le code]Soit σ, κ, M comme dans l'hypothèse du théorème ascendant : |σ| ≤ κ et |M| < κ . Ajoutons une constante ca pour tout élément a du domaine de M et appelons σ+ la signature σ augmentée de ces constantes ca. Soit M+ défini comme le modèle M mais où l'on interprète chaque constante ca par l'élément a du domaine de M. Soit T+ l'ensemble des formules closes vraies dans M+ sur le langage de signature σ+ (c'est le diagramme élémentaire (en) de M).
On considère maintenant un ensemble E de cardinal κ et des constantes di pour tout i dans E. On considère alors la théorie T' contenant T+ et les formules di ≠ dj pour i ≠ j. Toute partie finie T0 de T' est satisfiable : par exemple T0 admet comme modèle le modèle M', défini comme étant M+ dans lequel on interprète les constantes di de manière que les di intervenant dans T0 soient interprétés par des éléments distincts ; ceci est possible puisque T0 est finie et M infini. Par le théorème de compacité, T' admet un modèle N' dont le cardinal du domaine est au moins κ par définition de T', et qui est une extension élémentaire de M puisque T' contient le diagramme élémentaire T+ de M. Par le théorème de Löwenheim-Skolem descendant, il existe donc N'' qui est une sous-structure élémentaire de N'' et qui contient M, donc une extension élémentaire de M. Soit N le modèle N'' restreint à la signature σ ; c'est le modèle cherché[4].
Théorème de Löwenheim-Skolem descendant
[modifier | modifier le code]La partie descendante se montre en utilisant par exemple le théorème de complétude, ou au minimum la complétion du langage par des témoins de Henkin utilisée dans les versions modernes de la démonstration du théorème de complétude.
Corollaires
[modifier | modifier le code]- Le théorème de Löwenheim-Skolem permet par exemple de montrer que l'expressivité de la logique du premier ordre est strictement inférieure à celle de la logique du second ordre : en effet, la logique du second ordre permet de définir des théories cohérentes dont tous les modèles sont dénombrables, ce qui n'est pas possible avec la logique du premier ordre d'après le théorème de Löwenheim-Skolem ascendant.
- Considérons la signature de l'arithmétique 0, 1, +, ×, ≤ et le modèle des réels M = (R, 0, 1, +, ×, ≤). D'après le théorème de Löwenheim-Skolem, l'ensemble des formules vraies sur M admet un modèle dénombrable.
- Si l'on applique le théorème descendant à la théorie des ensembles, par exemple ZFC, ou à une autre théorie axiomatique destinée à fonder les théorèmes de Cantor, on obtient un univers dénombrable de tous les ensembles définis dans ZFC. Mais le théorème de Cantor permet de prouver dans ZFC qu'il existe des ensembles non dénombrables : c'est le paradoxe de Skolem, qui n'est contradictoire qu'en apparence. Le terme « dénombrable » est utilisé dans deux sens différents, au sens de la métathéorie pour « univers dénombrable », au sens de la théorie pour « il existe des ensembles non dénombrables ».
Notes et références
[modifier | modifier le code]- (en) Mordechai Ben-Ari (en), Mathematical Logic for Computer Science, London, Springer, , 346 p. (ISBN 978-1-4471-4129-7, lire en ligne).
- C'est-à-dire que le domaine de N est inclus dans le domaine de M et que les interprétations des fonctions et prédicats dans M sont les restrictions des interprétations dans N.
- C'est-à-dire que M et N satisfont les mêmes formules closes.
- (en) J. Malitz, Introduction to Mathematical Logic, Springer-Verlag, (lire en ligne).
Voir aussi
[modifier | modifier le code]Articles connexes
[modifier | modifier le code]Bibliographie
[modifier | modifier le code]- René Cori et Daniel Lascar, Logique mathématique II. Fonctions récursives, théorème de Gödel, théorie des ensembles, théorie des modèles [détail des éditions]
- Jean Ladrière, « Le théorème de Löwenheim-Skolem », Cahiers pour l'analyse, vol. 10 : La formalisation, 1969. [lire en ligne] [PDF]