Le théorème de complétude arithmétique
Dans l'article de Kikuchi sur la complexité de Kolmogorov et le deuxième théorème d'incomplétude, il énonce le "théorème de complétude arithmétique" comme suit:
Laisser $T$ être une théorie récursivement axiomatisable dans une langue $\mathcal{L}$, $C$ être un ensemble de nouvelles constantes et $\overline{\mathcal{L}}=\mathcal{L}\cup C$. Nous disons une formule$\phi(x)$ dans $\mathcal{L}_{A}$ définit un modèle de $T$ dans une théorie $S$ dans $\mathcal{L}_{A}$ si nous pouvons prouver à l'intérieur $S$ que l'ensemble
$$ \{ \sigma : \text{$\ sigma$ is a sentence in $\ overline {\ mathcal {L}}$ that satisfies $\ phi (\ ulcorner \ sigma \ urcorner)$} \} $$
forme un diagramme élémentaire d'un modèle de $T$ avec un univers de $C$.
Théorème 4.1. (Le théorème de complétude arithmétique). Il existe une formule$\text{Tr}_{T}({\ulcorner}x{\urcorner})$ dans $\mathcal{L}_{A}$ [le langage de l'arithmétique] qui définit un modèle de $T$ dans $\text{PA} + \text{Con}(T)$ , où $\text{Con}(T)$ est une phrase dans $\mathcal{L}_{A}$ cela signifie $T$ est consistent.
Il y a plusieurs aspects de ce théorème que je ne comprends pas:
La notion de formule définissant un modèle de $T$ dans $\text{PA} + \text{Con}(T)$ implique l'ensemble $ \{ \sigma : \text{$\ sigma$ is a sentence in $\ overline {\ mathcal {L}}$ that satisfies $\ phi (\ ulcorner \ sigma \ urcorner)$} \} $. Je ne sais pas comment formaliser cela en$\text{PA}$, et encore moins prouver quelque chose à ce sujet.
La même chose avec le discours sur les modèles de $T$. Dire$T = \text{ZFC}$, alors comment pouvez-vous même déclarer dans le langage de l'arithmétique qu'il existe un modèle de $T$ avec telle ou telle propriété (son diagramme élémentaire est l'ensemble ci-dessus et son univers)?
Un autre type de question: à quoi sert ce théorème (en termes généraux, au-delà du papier mentionné)? Pourquoi s'appelle-t-il le théorème de complétude arithmétique?
Réponses
Ré: $(1)$, il y a moins ici qu'il n'y paraît. Le point clé est que nous pouvons concocter une formule$\theta$ qui définit l'ensemble des nombres de Godel de $\overline{\mathcal{L}}$-Phrases; avec ça en main, on regarde juste$$S=\{x: \theta(x)\wedge\phi(x)\}.$$ C'est assez ennuyeux à définir.
Maintenant quand on dit ça $S$ est le diagramme élémentaire d'une structure avec domaine $C$, nous voulons dire que $S$ satisfait les propriétés habituelles d'un diagramme élémentaire - et comme ce sont des propriétés syntaxiques, nous pouvons via la numérotation Godel exprimer que $S$les a ou ne les a pas. Par exemple, nous voulons chacun des éléments suivants:
Si $\ulcorner\sigma_0\urcorner$, $\ulcorner\sigma_1\urcorner\in S$ puis $\ulcorner\sigma_0\wedge\sigma_1\urcorner\in S$.
Si $\ulcorner \exists x\sigma(x)\urcorner\in S$ alors pour certains $c\in C$ nous avons $\ulcorner\sigma(c)\urcorner\in S$. (Cela concerne le "avec l'univers de$C$"peu.)
$\ulcorner\perp\urcorner\not\in S$.
Un peu plus précisément, nous avons des fonctions récursives primitives correspondant par exemple à la conjonction et à la quantification existentielle par rapport à une variable fixe, et les deux premiers points ci-dessus correspondent à des conditions de fermeture / existence appropriées sur $S$par rapport à ces fonctions. Le troisième point empêche quant à lui la trivialité.
Fondamentalement, le fait est que la propriété d'être le diagramme élémentaire d'une structure avec domaine $\mathbb{N}$ est exprimable de premier ordre (car cela équivaut à des "conditions de fermeture / d'existence / de non-existence locales" comme ci-dessus).
Ré: $(2)$, intuitivement parlant, le fait est que nous ne parlons pas de modèles arbitraires de eg $\mathsf{ZFC}$, mais uniquement ceux avec domaine $\mathbb{N}$. Une structure avec domaine$\mathbb{N}$ est entièrement décrit par un seul ensemble de nombres naturels $X$, et "$X$ est le diagramme atomique d'un modèle de $\mathsf{ZFC}$"est exprimable au premier ordre ci-dessus: nous disons simplement"$X$ a les propriétés syntaxiques de base ci-dessus, et chaque $\mathsf{ZFC}$-axioms est dans $X$. "
Je pense que cela pourrait être rendu plus mystérieux parce que nous pensons généralement à des modèles de $\mathsf{ZFC}$comme étant très compliqué et n'ayant certainement pas de domaine$\mathbb{N}$. Mais par Lowenheim-Skolem,$\mathsf{ZFC}$(en supposant que ce soit cohérent) a également beaucoup de modèles avec domaine$\mathbb{N}$. Ce sont les modèles que nous pouvons considérer dans cette approche.
Ré: $(3)$, le fait est que la formulation habituelle du théorème d'exhaustivité
toute théorie cohérente a un modèle
est totalement dingue dans le contexte de l'arithmétique. Fondamentalement, nous ne pouvons parler directement d' ensembles finis que dans le langage de l'arithmétique, donc si nous «formulons naïvement» la phrase «l'arithmétique de Presburger n'a pas de modèles», nous obtenons quelque chose de vrai.
(Voir par exemple l' interprétation Ackermann . On peut passer de (disons)$\mathsf{PA}$ à une théorie des ensembles convenablement équivalente, mais cette théorie prouve que «tout ensemble est fini.»)
Donc, si nous voulons qu'une version du théorème de complétude soit valable dans une théorie de l'arithmétique, ses «modèles» doivent consister en des relations sur l'univers entier; et bien sûr ils devront consister en des relations définissables , puisque nous ne pouvons pas parler de relations indéfinissables en interne.
Une autre option serait d'utiliser des extensions conservatrices qui peuvent parler directement d'ensembles infinis; c'est par exemple l'approche adoptée ici . Dans tous les contextes où j'ai joué avec cette approche fonctionne et donc je la préfère généralement. Cela dit,$(i)$ si je me souviens bien, il y a des situations où cette approche est soit désagréable ou obscurcit des informations précieuses (je pense que cela se produit avec de très faibles théories de l'arithmétique) et $(ii)$ le fait que l'on puisse obtenir un théorème d'exhaustivité uniquement dans le langage de l'arithmétique du premier ordre est intéressant en soi.