Théorème de Löwenheim-Skolem - Löwenheim–Skolem theorem

En logique mathématique , le théorème de Löwenheim-Skolem est un théorème sur l'existence et la cardinalité des modèles , du nom de Leopold Löwenheim et Thoralf Skolem .

La formulation précise est donnée ci-dessous. Cela implique que si un dénombrable premier ordre théorie a un infini modèle , alors pour tout infini nombre cardinal κ il a un modèle de taille κ , et qu'aucune théorie du premier ordre avec un modèle infini peut avoir un modèle unique à isomorphisme près . En conséquence, les théories du premier ordre sont incapables de contrôler la cardinalité de leurs modèles infinis.

Le théorème de Löwenheim-Skolem (vers le bas) est l'une des deux propriétés clés, avec le théorème de compacité , qui sont utilisées dans le théorème de Lindström pour caractériser la logique du premier ordre . En général, le théorème de Löwenheim-Skolem ne tient pas dans les logiques plus fortes telles que la logique du second ordre .

Théorème

Dans sa forme générale, le Löwenheim-Skolem Théorème indique que pour chaque signature σ , chaque infinie σ - la structure M et tout nombre cardinal infini la K ≥ | σ | , Il y a une σ -structure N tel que | N | = Κ et de telle sorte que

• si κ <| M | alors N est une sous-structure élémentaire de M ;
• si κ > | M | alors N est une extension élémentaire de M .

Le théorème est souvent divisé en deux parties correspondant aux deux cas ci-dessus. La partie du théorème affirmant qu'une structure a des sous-structures élémentaires de toutes les plus petites cardinalités infinies est connue sous le nom de théorème de Löwenheim-Skolem descendant . La partie du théorème affirmant qu'une structure a des extensions élémentaires de toutes les plus grandes cardinalités est connue sous le nom de théorème de Löwenheim-Skolem ascendant .

Discussion

Ci-dessous, nous expliquons le concept général de signatures et de structures.

notions

Signatures

Une signature est constituée d'un ensemble de symboles de fonction S _func , d'un ensemble de symboles de relation S _rel , et d'une fonction représentant l' arité des symboles de fonction et de relation. (Un symbole de fonction nulle est appelé un symbole constant.) Dans le contexte de la logique du premier ordre, une signature est parfois appelée un langage. On l'appelle dénombrable si l'ensemble des symboles de fonction et de relation qu'il contient est dénombrable, et en général la cardinalité d'une signature est la cardinalité de l'ensemble de tous les symboles qu'elle contient. ${\displaystyle \operatorname {ar} :S_{\operatorname {func} }\cup S_{\operatorname {rel} }\rightarrow \mathbb {N} _{0}}$

Une théorie du premier ordre consiste en une signature fixe et un ensemble fixe de phrases (formules sans variables libres) dans cette signature. Les théories sont souvent spécifiées en donnant une liste d'axiomes qui génèrent la théorie, ou en donnant une structure et en prenant la théorie pour se composer des phrases satisfaites par la structure.

Structures / Modèles

Compte tenu de la signature σ , une σ - la structure M est une interprétation concrète des symboles dans σ . Il se compose d'un ensemble sous-jacent (souvent également désigné par " M ") ainsi que d'une interprétation des symboles de fonction et de relation de σ . Une interprétation d'un symbole de constante σ à M est simplement un élément de M . Plus généralement, une interprétation d'un symbole de fonction n- aire f est une fonction de M ⁿ dans M . De même, une interprétation d'un symbole de relation R est une relation n- aire sur M , c'est-à-dire un sous-ensemble de  M ⁿ .

Une sous-structure d'une σ -structure M est obtenue en prenant un sous-ensemble N de M qui est fermé sous les interprétations de tous les symboles de fonction dans σ (inclut donc les interprétations de tous les symboles constants dans σ ), puis en restreignant les interprétations de la symboles de relation à N . Une sous - structure élémentaire en est un cas très particulier ; en particulier une sous-structure élémentaire satisfait exactement les mêmes phrases du premier ordre que la structure d'origine (son extension élémentaire).

Conséquences

L'énoncé donné dans l'introduction suit immédiatement en prenant M pour un modèle infini de la théorie. La preuve de la partie ascendante du théorème montre également qu'une théorie avec des modèles finis arbitrairement grands doit avoir un modèle infini ; parfois, cela est considéré comme faisant partie du théorème.

Une théorie est dite catégorique si elle n'a qu'un seul modèle, à isomorphisme près. Ce terme a été introduit par Veblen (1904) , et pendant un certain temps par la suite, les mathématiciens espéraient pouvoir mettre les mathématiques sur une base solide en décrivant une théorie catégorique du premier ordre d'une version de la théorie des ensembles. Le théorème de Löwenheim-Skolem a porté un premier coup à cet espoir, car il implique qu'une théorie du premier ordre qui a un modèle infini ne peut pas être catégorique. Plus tard, en 1931, l'espoir a été complètement brisé par le théorème d'incomplétude de Gödel .

De nombreuses conséquences du théorème de Löwenheim-Skolem semblaient contre-intuitives aux logiciens du début du 20e siècle, car la distinction entre les propriétés de premier ordre et de non-premier ordre n'était pas encore comprise. L'une de ces conséquences est l'existence d'innombrables modèles d' arithmétique vraie , qui satisfont à tous les axiomes d'induction du premier ordre mais ont des sous-ensembles non inductifs.

Soit N les nombres naturels et R les réels. Il résulte du théorème que la théorie de ( N , +, ×, 0, 1) (la théorie de l'arithmétique vraie du premier ordre) a d'innombrables modèles, et que la théorie de ( R , +, ×, 0, 1) (la théorie des champs réels fermés ) a un modèle dénombrable. Il existe bien entendu des axiomatisations caractérisant ( N , +, ×, 0, 1) et ( R , +, ×, 0, 1) à isomorphisme près. Le théorème de Löwenheim-Skolem montre que ces axiomatisations ne peuvent pas être du premier ordre. Par exemple, dans la théorie des nombres réels, la complétude d'un ordre linéaire utilisé pour caractériser R comme un champ ordonné complet, est une propriété non du premier ordre .

Une autre conséquence qui a été considérée comme particulièrement troublante est l'existence d'un modèle dénombrable de la théorie des ensembles, qui doit néanmoins satisfaire la phrase disant que les nombres réels sont indénombrables. Le théorème de Cantor affirme que certains ensembles sont indénombrables. Cette situation contre-intuitive a été connue sous le nom de paradoxe de Skolem ; cela montre que la notion de dénombrement n'est pas absolue .

Croquis de preuve

Partie descendante

Pour chaque formule du premier ordre, l' axiome du choix implique l'existence d'une fonction ${\style d'affichage \sigma }$${\displaystyle \varphi (y,x_{1},\ldots ,x_{n})\,,}$

${\displaystyle f_{\varphi }:M^{n}\to M}$

tel que, pour tous , soit ${\displaystyle a_{1},\ldots ,a_{n}\in M}$

${\displaystyle M\models \varphi (f_{\varphi }(a_{1},\dots ,a_{n}),a_{1},\dots ,a_{n})}$

ou

${\displaystyle M\models \neg \exists y\,\varphi (y,a_{1},\dots ,a_{n})\,.}$

En appliquant à nouveau l'axiome du choix, nous obtenons une fonction des formules du premier ordre à de telles fonctions${\style d'affichage \varphi }$${\displaystyle f_{\varphi }\,.}$

La famille de fonctions donne lieu à un opérateur de pré - fermeture sur l' ensemble de puissance de${\displaystyle f_{\varphi }}$ ${\style d'affichage F}$${\style d'affichage M}$

${\displaystyle F(A)=\{f_{\varphi }(a_{1},\dots ,a_{n})\in M\mid \varphi \in \sigma ;\,a_{1},\dots ,a_{n}\dans A\}}$

pour ${\displaystyle A\subseteq M\,.}$

L'itération dénombrable de nombreuses fois aboutit à un opérateur de fermeture. Prenant un sous-ensemble arbitraire tel que , et après avoir défini, on peut voir que Then est également une sous-structure élémentaire de par le test de Tarski-Vaught . ${\style d'affichage F}$ ${\displaystyle F^{\omega }\,.}$${\style d'affichage A\sous-ensemble M}$${\displaystyle \left\vert A\right\vert =\kappa }$${\displaystyle N=F^{\omega }(A)\,,}$${\displaystyle \left\vert N\right\vert =\kappa \,.}$${\style d'affichage N}$${\style d'affichage M}$

L'astuce utilisée dans cette preuve est essentiellement due à Skolem, qui a introduit des symboles de fonction pour les fonctions de Skolem dans le langage. On pourrait également définir la comme des fonctions partielles de telle sorte que définie si et seulement si le seul point important est que est un opérateur de pré - fermeture de telle sorte que contient une solution pour chaque formule à paramètres dans qui a une solution dans et en ce que ${\displaystyle f_{\varphi }}$${\displaystyle f_{\varphi }}$${\displaystyle f_{\varphi }}$${\displaystyle M\models \exists y\,\varphi (y,a_{1},\dots ,a_{n})\,.}$${\style d'affichage F}$${\style d'affichage F(A)}$${\style d'affichage A}$${\style d'affichage M}$

${\displaystyle \left\vert F(A)\right\vert \leq \left\vert A\right\vert +\left\vert \sigma \right\vert +\aleph _{0}\,.}$

Partie montante

Premièrement, on étend la signature en ajoutant un nouveau symbole constant pour chaque élément de M . La théorie complète de M pour la signature étendue ' est appelée le diagramme élémentaire de M . Dans l'étape suivante, on ajoute κ beaucoup de nouveaux symboles constants à la signature et ajoute au diagramme élémentaire de M les phrases c ≠ c' pour deux nouveaux symboles constants distincts c et c' . En utilisant le théorème de compacité , la théorie résultante est facilement considérée comme cohérente. Puisque ses modèles doivent avoir une cardinalité d'au moins κ , la partie descendante de ce théorème garantit l'existence d'un modèle N qui a exactement la cardinalité κ . Il contient une copie isomorphe de M comme sous-structure élémentaire.

Dans d'autres logiques

Bien que le théorème (classique) de Löwenheim-Skolem soit très étroitement lié à la logique du premier ordre, des variantes sont valables pour d'autres logiques. Par exemple, chaque théorie cohérente en logique du second ordre a un modèle plus petit que le premier cardinal supercompact (en supposant qu'il existe). La taille minimale à laquelle un théorème de type Löwenheim-Skolem (vers le bas) s'applique dans une logique est connue sous le nom de nombre de Löwenheim et peut être utilisée pour caractériser la force de cette logique. De plus, si nous allons au-delà de la logique du premier ordre, nous devons abandonner l'une des trois choses suivantes : la compacité dénombrable, le théorème de Löwenheim-Skolem descendant, ou les propriétés d'une logique abstraite .

Notes historiques

Ce compte est basé principalement sur Dawson (1993) . Pour comprendre les débuts de la théorie des modèles, il faut distinguer la cohérence syntaxique (aucune contradiction ne peut être déduite en utilisant les règles de déduction pour la logique du premier ordre) et la satisfiabilité (il existe un modèle). De manière assez surprenante, même avant que le théorème de complétude ne rende la distinction inutile, le terme cohérent était utilisé parfois dans un sens et parfois dans l'autre.

Le premier résultat significatif de ce qui deviendra plus tard la théorie des modèles fut le théorème de Löwenheim dans la publication de Leopold Löwenheim « Über Möglichkeiten im Relativkalkül » (1915) :

Pour chaque signature dénombrable σ , chaque σ -sentence qui est satisfiable est satisfiable dans un modèle dénombrable.

L'article de Löwenheim portait en fait sur le calcul plus général de Peirce- Schröder des relations ( algèbre de relation avec les quantificateurs). Il a également utilisé les notations désormais archaïques d' Ernst Schröder . Pour un résumé de l'article en anglais et utilisant les notations modernes, voir Brady (2000 , chapitre 8).

Selon le point de vue historique reçu, la preuve de Löwenheim était erronée car elle utilisait implicitement le lemme de Kőnig sans le prouver, bien que le lemme n'était pas encore un résultat publié à l'époque. Dans un récit révisionniste , Badesa (2004) considère que la preuve de Löwenheim était complète.

Skolem (1920) a donné une preuve (correcte) en utilisant des formules dans ce qui sera appelé plus tard la forme normale de Skolem et en s'appuyant sur l'axiome du choix :

Toute théorie dénombrable qui est satisfiable dans un modèle M , est satisfiable dans une sous-structure dénombrable de M .

Skolem (1922) a également prouvé la version plus faible suivante sans l'axiome de choix :

Toute théorie dénombrable qui est satisfiable dans un modèle est également satisfiable dans un modèle dénombrable.

Skolem (1929) simplifié Skolem (1920) . Enfin, Anatoly Ivanovich Maltsev (Анато́лий Ива́нович Ма́льцев, 1936) a prouvé le théorème de Löwenheim-Skolem dans sa pleine généralité ( Maltsev 1936 ). Il a cité une note de Skolem, selon laquelle le théorème avait été prouvé par Alfred Tarski lors d'un séminaire en 1928. Par conséquent, le théorème général est parfois connu sous le nom de théorème de Löwenheim-Skolem-Tarski . Mais Tarski ne se souvenait pas de sa preuve, et il reste un mystère comment il a pu le faire sans le théorème de compacité .

Il est quelque peu ironique que le nom de Skolem soit lié à la direction ascendante du théorème ainsi qu'à la direction descendante :

« J'ai l'habitude d'appeler le corollaire 6.1.4 le théorème ascendant de Löwenheim-Skolem. Mais en fait, Skolem n'y croyait même pas, car il ne croyait pas à l'existence d'ensembles innombrables. – Hodges (1993) .

« Skolem […] a rejeté le résultat comme dénué de sens ; Tarski […] a très raisonnablement répondu que le point de vue formaliste de Skolem devrait considérer le théorème de Löwenheim-Skolem vers le bas comme dénué de sens tout comme le théorème vers le haut. » – Hodges (1993) .

"La légende raconte que Thoralf Skolem, jusqu'à la fin de sa vie, fut scandalisé par l'association de son nom à un résultat de ce type, qu'il considérait comme une absurdité, les décors non dénombrables étant, pour lui, des fictions sans existence réelle." – Poizat (2000) .

Les références

Sources

Le théorème de Löwenheim-Skolem est traité dans tous les textes d'introduction à la théorie des modèles ou à la logique mathématique .

Publications historiques

• Löwenheim, Leopold (1915), "Über Möglichkeiten im Relativkalkül" (PDF) , Mathematische Annalen , 76 (4) : 447-470, doi : 10.1007/BF01458217 , ISSN  0025-5831 , S2CID  116581304
  • Löwenheim, Leopold (1977), "Sur les possibilités dans le calcul des parents", De Frege à Gödel: A Source Book in Mathematical Logic, 1879-1931 (3e éd.), Cambridge, Massachusetts: Harvard University Press, pp. 228- 251, ISBN 0-674-32449-8( copie en ligne , p. 228, sur Google Books )
• Maltsev, Anatoly Ivanovich (1936), "Untersuchungen aus dem Gebiete der mathematischen Logik" , Matematicheskii Sbornik , Novaya Seriya, 1(43) (3) : 323-336
• Skolem, Thoralf (1920), "Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen", Videnskapsselskapet Skrifter, I. Matematisk-naturvidenskabelig Klasse , 4 : 1-36
  • Skolem, Thoralf (1977), « Investigations Logico-combinatoires dans la satisfiabilité ou la provabilité de propositions mathématiques : Une preuve simplifiée d'un théorème par L. Löwenheim et généralisations du théorème », De Frege à Gödel : A Source Book in Mathematical Logic, 1879-1931 (3e éd.), Cambridge, Massachusetts : Harvard University Press, pp. 252-263, ISBN 0-674-32449-8( copie en ligne , p. 252, sur Google Books )
• Skolem, Thoralf (1922), "Einige Bemerkungen zu axiomatischen Begründung der Mengenlehre", Mathematikerkongressen I Helsingfors den 4-7 juillet 1922, den Femte Skandinaviska Matematikerkongressen, Redogörelse : 217-232
  • Skolem, Thoralf (1977), "Quelques remarques sur la théorie des ensembles axiomatisée", De Frege à Gödel: A Source Book in Mathematical Logic, 1879-1931 (3e éd.), Cambridge, Massachusetts: Harvard University Press, pp. 290-301 , ISBN 0-674-32449-8( copie en ligne , p. 290, sur Google Books )
• Skolem, Thoralf (1929), "Über einige Grundlagenfragen der Mathematik", Skrifter Utgitt av Det Norske Videnskaps-Akademi I Oslo, I. Matematisk-naturvidenskabelig Klasse , 7 : 1–49
• Veblen, Oswald (1904), "A System of Axioms for Geometry", Transactions of the American Mathematical Society , 5 (3) : 343-384, doi : 10.2307/1986462 , ISSN  0002-9947 , JSTOR  1986462

Sources secondaires

• Badesa, Calixto (2004), La naissance de la théorie des modèles : le théorème de Löwenheim dans le cadre de la théorie des parents , Princeton, NJ : Princeton University Press, ISBN 978-0-691-05853-5; Un récit plus concis apparaît au chapitre 9 de Leila Haaparanta , éd. (2009), Le développement de la logique moderne , Oxford University Press, ISBN 978-0-19-513731-6
• Brady, Geraldine (2000), De Peirce à Skolem : un chapitre négligé dans l'histoire de la logique , Elsevier, ISBN 978-0-444-50334-3
• Crossley, JN ; Ash, juge en chef ; Brickhill, juge en chef ; Stillwell, JC; Williams, NH (1972), Qu'est-ce que la logique mathématique ? , Londres/Oxford/New York : Oxford University Press , p. 59-60, ISBN 0-19-888087-1, Zbl  0251.02001
• Dawson, John W., Jr. (1993), "The compactness of First-Order Logic: From Gödel to Lindström", History and Philosophy of Logic , 14 : 15-37, doi : 10.1080/01445349308837208
• Hodges, Wilfrid (1993), Théorie des modèles , Cambridge : Cambridge Univ. Pr., ISBN 978-0-521-30442-9
• Poizat, Bruno (2000), A Course in Model Theory: An Introduction to Contemporary Mathematical Logic , Berlin, New York : Springer, ISBN 978-0-387-98655-5

Liens externes

• Sakharov, A. ; Weisstein, EW "Théorème de Löwenheim-Skolem" . MathWorld .
• Burris, Stanley N., Contributions of the Logicians, Part II, De Richard Dedekind à Gerhard Gentzen
• Burris, Stanley N., Théorème descendant de Löwenheim-Skolem
• Simpson, Stephen G. (1998), Théorie des modèles