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

Cas d'un langage dénombrable

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). 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. 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.

Théorèmes de Löwenheim-Skolem pour tout cardinal

À partir de M, il existe un modèle N de cardinal κ tels que M et N soient élémentairement équivalents et si κ est plus petit que le cardinal du domaine de M, alors N est un sous-modèle de M et sinon M est un sous-modèle de N.

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 é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.

Idées des démonstrations

Théorème de Löwenheim-Skolem ascendant

Soit σ, κ, M comme dans l'hypothèse du théorème ascendant : |σ| ≤ κ et |M| < κ . Ajoutons une constante c_a pour tout élément a du domaine de M et appelons σ⁺ la signature σ augmentée de ces constantes c_a. Soit M⁺ défini comme le modèle M mais où l'on interprète chaque constante c_a 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 d_i pour tout i dans E. On considère alors la théorie T' contenant T⁺ et les formules d_i ≠ d_j pour i ≠ j. Toute partie finie T₀ de T' est satisfiable : par exemple T₀ admet comme modèle le modèle M', défini comme étant M⁺ dans lequel on interprète les constantes d_i de manière que les d_i intervenant dans T₀ soient interprétés par des éléments distincts ; ceci est possible puisque T₀ 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é.

Théorème de Löwenheim-Skolem descendant

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

• Le théorème de Löwenheim-Skolem permet par exemple de montrer que la logique du premier ordre est strictement inférieure à celle du second ordre^{[incompréhensible]}.
• 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 ».

Voir aussi

Articles connexes

• Théorème de Lindström
• Nombre de Löwenheim (en)

Bibliographie

• 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]