# 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

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$_0$ de T' est satisfiable : par exemple T$_0$ 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$_0$ soient interprétés par des éléments distincts ; ceci est possible puisque T$_0$ 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 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 ».