Théorème de complétude revisité
Bonsoir,
Le théorème de complétude de la logique du premier ordre est l'énoncé suivant :
Version 0 : Soit $T$ une théorie dans un langage $\mathcal{L}$. La théorie $T$ est cohérente si et seulement si elle a un modèle.
Alors voilà : j'ai l'impression que dès qu'on arrive à parler de type, beaucoup de livres s'autorisent une autre version du théorème de complétude.
Celle-ci va suivre, et j'ai envie de savoir si elle est vraie (j'ai essayé d'adapter la méthode de Henkin, en vain). J'introduis d'abord quelques variations du vocabulaire usuel : ce qui suit demande donc d'oublier le vocabulaire usuel.
La notion de langage est la même que d'habitude : soit $\mathcal{L}$ un langage qu'on fixe dans la suite.
Il en va de même de la notion de $\mathcal{L}$-structure ainsi que de la notion de satisfaisabilité dans une $\mathcal{L}$-structure, que je ne redéfinirai donc pas.
Définition 1 : Une théorie est un ensemble de formules.
Définition 2 : Si $\phi$ est une formule, on dit qu'une théorie $T$ démontre $\phi$ (noté $T\vdash\phi$) dès qu'il existe une suite $\phi_0,\dots,\phi_n$ de formules telles que :
1)soit $ \phi_i \in T$
2)soit $ \phi_i$ est un axiome logique (i.e. une tautologie ou un axiome des quantificateurs)
3)soit $ \phi_i$ s'obtient par généralisation ou par modus ponens à partir des $\phi_j (j<i)$
Définition 3 : On dit qu'une $\mathcal{L}$-structure $M$ est un modèle de la théorie $T$ s'il existe $\overline{a}\in M^{\omega}$ (i.e. $(a_1,a_2,\dots,a_n,\dots)\in M^{\omega}$) telle que pour tout $\phi(\overline{v})\in T$ on ait $M\vDash \phi(\overline{a})$.
Définition 4 : On dit qu'une théorie $T$ est cohérente s'il existe une formule $\phi$ telle que $T\nvdash \phi$ ou $T\nvdash \neg\phi$.
Je me demande alors si avec les définitions précédentes, la variante suivante du théorème de complétude est vraie :
Version 1 : Soit $T$ une théorie dans le langage $\mathcal{L}$. La théorie $T$ est cohérente si et seulement si elle a un modèle.
Ce qui nous intéresse quand on joue avec les types est plutôt l'énoncé du théorème de complétude où la définition $1)$ est remplacée par la suivante et où $N$ est fixé d'emblée :
Définition 1' : Une théorie est un ensemble de formules dont les variables libres sont dans $v_1,\dots,v_N$. (la suite des $v_i$ étant celle des variables du langage)
Version 1' : Soit $T$ une théorie dans le langage $\mathcal{L}$. La théorie $T$ est cohérente si et seulement si elle a un modèle.
Somme toute, ce qu'on utilise quand on joue avec les types, c'est plutôt le théorème de compacité pour les types qui est le suivant et qui est régi par la définition $1')$ :
Soit $T$ une théorie dont toute partie finie a un modèle, alors $T$ a un modèle.
Je vois comment démontrer ce dernier sans passer par la version $1'$, mais j'ai l'impression que l'usage de celle-ci est sous-entendu dans un certain nombre d'ouvrages.
Je cherche donc à savoir si les versions $1$ et $1'$ sont vraies.
Merci à ceux qui pourront éclairer ma lanterne.
Le théorème de complétude de la logique du premier ordre est l'énoncé suivant :
Version 0 : Soit $T$ une théorie dans un langage $\mathcal{L}$. La théorie $T$ est cohérente si et seulement si elle a un modèle.
Alors voilà : j'ai l'impression que dès qu'on arrive à parler de type, beaucoup de livres s'autorisent une autre version du théorème de complétude.
Celle-ci va suivre, et j'ai envie de savoir si elle est vraie (j'ai essayé d'adapter la méthode de Henkin, en vain). J'introduis d'abord quelques variations du vocabulaire usuel : ce qui suit demande donc d'oublier le vocabulaire usuel.
La notion de langage est la même que d'habitude : soit $\mathcal{L}$ un langage qu'on fixe dans la suite.
Il en va de même de la notion de $\mathcal{L}$-structure ainsi que de la notion de satisfaisabilité dans une $\mathcal{L}$-structure, que je ne redéfinirai donc pas.
Définition 1 : Une théorie est un ensemble de formules.
Définition 2 : Si $\phi$ est une formule, on dit qu'une théorie $T$ démontre $\phi$ (noté $T\vdash\phi$) dès qu'il existe une suite $\phi_0,\dots,\phi_n$ de formules telles que :
1)soit $ \phi_i \in T$
2)soit $ \phi_i$ est un axiome logique (i.e. une tautologie ou un axiome des quantificateurs)
3)soit $ \phi_i$ s'obtient par généralisation ou par modus ponens à partir des $\phi_j (j<i)$
Définition 3 : On dit qu'une $\mathcal{L}$-structure $M$ est un modèle de la théorie $T$ s'il existe $\overline{a}\in M^{\omega}$ (i.e. $(a_1,a_2,\dots,a_n,\dots)\in M^{\omega}$) telle que pour tout $\phi(\overline{v})\in T$ on ait $M\vDash \phi(\overline{a})$.
Définition 4 : On dit qu'une théorie $T$ est cohérente s'il existe une formule $\phi$ telle que $T\nvdash \phi$ ou $T\nvdash \neg\phi$.
Je me demande alors si avec les définitions précédentes, la variante suivante du théorème de complétude est vraie :
Version 1 : Soit $T$ une théorie dans le langage $\mathcal{L}$. La théorie $T$ est cohérente si et seulement si elle a un modèle.
Ce qui nous intéresse quand on joue avec les types est plutôt l'énoncé du théorème de complétude où la définition $1)$ est remplacée par la suivante et où $N$ est fixé d'emblée :
Définition 1' : Une théorie est un ensemble de formules dont les variables libres sont dans $v_1,\dots,v_N$. (la suite des $v_i$ étant celle des variables du langage)
Version 1' : Soit $T$ une théorie dans le langage $\mathcal{L}$. La théorie $T$ est cohérente si et seulement si elle a un modèle.
Somme toute, ce qu'on utilise quand on joue avec les types, c'est plutôt le théorème de compacité pour les types qui est le suivant et qui est régi par la définition $1')$ :
Soit $T$ une théorie dont toute partie finie a un modèle, alors $T$ a un modèle.
Je vois comment démontrer ce dernier sans passer par la version $1'$, mais j'ai l'impression que l'usage de celle-ci est sous-entendu dans un certain nombre d'ouvrages.
Je cherche donc à savoir si les versions $1$ et $1'$ sont vraies.
Merci à ceux qui pourront éclairer ma lanterne.
Réponses
-
Bonjour Gaussien,
Un problème est que ta notion de démonstration n'est pas correcte puisque dans tes axiomes tu as des variables libres. Je m'explique : disons que tu as un symbole de relation $R$, et que $T$ est $\{Rx\}$. Alors $Rx, (\forall x, Rx)$ est une démonstration donc $T\vdash \forall x, Rx$. Or tu peux très bien avoir un modèle de $T$ (en ton sens) qui ne soit pas un modèle de $\forall x,Rx$. Autrement dit, tu cherches à prouver un théorème de complétude mais tu n'as même pas de théorème de correction ! -
De manière générale, s'il est vrai que les théorèmes de complétude sont célèbres, ils n'en demeurent pas moins "triviaux" et surtout adaptables. Je ne comprends donc pas ta demande.
Le point crucial est juste que le modus ponens doit être "lu à l'envers", ie si $B$ n'est pas prouvé alors $A\to B$ ne l'est pas ou $A$ ne l'est pas, ce qui donne une structure assez similaire aux idéaux premiers d'un anneau commutatif aux théories complètes, etc, etc.
Il suit que ta demande ne pourra être vraiment traitée QUE quand tu auras bien distingué où se situe ton problème dans la somme des DEUX mécanismes: partie propositionnelle + partie quantificateurs. Or tu expédies ça bien trop vite pour qu'on n'ait pas à nous-même écrire 100 lignes et tout redécrire pour espérer t'aider.
Pour la partie purement propositionnelle "du grand champ de la logique", le théorème est complétude est juste le lemme de Zorn (toute théorie consistante est incluse dans une théorie complète), et il n'y a rien d'autre à dire. C'est + ou - valable pour toute logique "in some sense" (---> pour toi, je pense, pour d'autres, d'une logique à l'autre, il y a des nuances importantes, mais HS pour toi)
Pour la partie non propositionnelle des mécanismes de complétude, d'ailleurs très esthétique et raffinée, très aussi agréable à dompter, je t'invite à détailler et préciser "très considérablement" ta demande si tu ne veux pas recevoir "un traité complet en retour" (que personne n'aura d'ailleurs le courage d'écrire).
Je te donne ci-dessous une présentation simplifiée et non fondée des mécanismes généraux de complétude.
1/ Parler de modèles n'est pas pertinent. Un "modèle" est une théorie complète qui nomme tout le monde (autrement dit qui, quand elle déclare faux l'énoncé $\forall xR(x)$, déclare faux au moins un des énoncés de la forme $R(a)$ où $a$ est une constante)
2/ Toute théorie consistante est incluse dans une théorie complète
3/ Une théorie est complète ssi elle est maximale
4/ Toute théorie symétriquement présentée lève le problème des quantificateurs
Ces trois points sont des slogans tant qu'on n'a pas donné des définitions précises. Toutes les conditions sont appelées des "conditions fermées"** au sens topologique, SAUF celle qui "voudrait que" quand $T$ prouve, pour chaque $a$ l'énoncé $R(a)$ alors $T$ prouve $\forall xR(x)$. Seules les théories SYMETRIQUES (c'est un nom que j'invente pour te répondre, tu ne le trouveras pas dans la littérature) vérifie ça grace à une mécanisme FERMé.
[small]** Les exigences sont au nombre de 5:
1/ Ne pas contenir A, A=>B et B=>Faux
2/ Contenir A=>B dès qu'on contient B
3/ Contenir A=>B dès qu'on contient A=>faux
4/ Contenir certains axiomes
5/ Etre stable par modus ponens
"Consistant" voulant dire "ne pas contenir faux".
toutes fermées. Zorn s'applique.[/small]Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Je précise le mot "symétrique" que j'ai inventé pour l'occasion:
Si une théorie contient assez de constantes à propos desquelles elle ne suppose rien, la règle sémantique suivante, inutilisable en pratique:
D'une preuve $p_a$ de $R(a)$ pour chaque $a$,
j'infère une preuve $q:=Convention(a\mapsto p_a)$ de $\forall xR(x)$
Peut alors être remplacée par :
D'une SEULE PREUVE $p$ de $R(a)$, pour une
des constantes $a$ à propos de laquelle je n'ai rien supposé
j'infère LA preuve $q:=Convention(FonctionConstante(b\mapsto p))$ de $\forall xR(x)$
De sorte qu'au lieu d'avoir des fonctions, tu as des fonctions CONSTANTES (qu'en pratique on voit comme l'élément de leur image directe).
Le mot "symétrique" vient du rôle symétrique joué par les constantes "à propos desquelles la théorie ne suppose rien"
Cette "conquête" permet de retrouver une condition de FERMETURE, donc de récupérer "complétude et compacité". (Et d'avoir des fichiers finis archivés à l'académie des sciences)Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.
Bonjour!
Catégories
- 163.2K Toutes les catégories
- 9 Collège/Lycée
- 21.9K Algèbre
- 37.1K Analyse
- 6.2K Arithmétique
- 53 Catégories et structures
- 1K Combinatoire et Graphes
- 11 Sciences des données
- 5K Concours et Examens
- 11 CultureMath
- 47 Enseignement à distance
- 2.9K Fondements et Logique
- 10.3K Géométrie
- 64 Géométrie différentielle
- 1.1K Histoire des Mathématiques
- 68 Informatique théorique
- 3.8K LaTeX
- 39K Les-mathématiques
- 3.5K Livres, articles, revues, (...)
- 2.7K Logiciels pour les mathématiques
- 24 Mathématiques et finance
- 314 Mathématiques et Physique
- 4.9K Mathématiques et Société
- 3.3K Pédagogie, enseignement, orientation
- 10K Probabilités, théorie de la mesure
- 773 Shtam
- 4.2K Statistiques
- 3.7K Topologie
- 1.4K Vie du Forum et de ses membres
In this Discussion
Qui est en ligne 29
+17 Invités