Démonstration théorème de complétude
Bonjour,
je bloque sur un passage dans l'une des démonstrations du théorème de complétude (Cori Lascar, tome 1, page 242). Je mets le lemme en question en pièce jointe.
Il est dit que si $H_{i}$ est un axiome logique alors $K_{i}$ en est un aussi. Si je regarde le troisième axiome donné dans le livre :
$\forall v F \Rightarrow F_{t/v}$, où $F$ est une formule, $t$ un terme et aucune occurrence libre de $v$ dans $F$ ne se trouve dans le champ d'un quantificateur liant une variable de $t$.
Si je comprends bien, partant de $\forall v F_{w/c} \Rightarrow (F_{t/v})_{w/c}$, on doit avoir $\forall v F_{w/c} \Rightarrow (F_{w/c})_{t/v}$. Pourquoi est-on sûr que le symbole de constante $c$ n'apparaît pas dans le terme $t$ ?
je bloque sur un passage dans l'une des démonstrations du théorème de complétude (Cori Lascar, tome 1, page 242). Je mets le lemme en question en pièce jointe.
Il est dit que si $H_{i}$ est un axiome logique alors $K_{i}$ en est un aussi. Si je regarde le troisième axiome donné dans le livre :
$\forall v F \Rightarrow F_{t/v}$, où $F$ est une formule, $t$ un terme et aucune occurrence libre de $v$ dans $F$ ne se trouve dans le champ d'un quantificateur liant une variable de $t$.
Si je comprends bien, partant de $\forall v F_{w/c} \Rightarrow (F_{t/v})_{w/c}$, on doit avoir $\forall v F_{w/c} \Rightarrow (F_{w/c})_{t/v}$. Pourquoi est-on sûr que le symbole de constante $c$ n'apparaît pas dans le terme $t$ ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Je raconte n'importe quoi. J'en reviens donc à ma question initiale.
Or $(F_{w/c})_{s/v}$ n'est rien d'autre que $(F_{t/v})_{w/c}$ (voir "lemme de double substitution" ou quelque chose qui s'appelle comme ça).
on a un langage $\mathscr{L}$, une théorie $T$ que l'on suppose cohérente et une formule $F$ à une seule variable libre du langage $\mathscr{L}$. On ajoute alors au langage un symbole de constante $c_{F}$ n'apparaissant ni dans $F$, ni dans $T$. La théorie $T \cup \{\exists v F(v) \Rightarrow F(c_{F})\}$ est alors cohérente dans le langage enrichi. Ma question est sans doute stupide, mais pourquoi l'existence de ce symbole de constante est-elle garantie ?
Les théorèmes de complétude partent d'une énumération $(F_n)_{n\geq 0}$ de toutes les formules à une variable libre (désignée par $v_n$ dans ce qui suit) et rajoutent à la théorie ambiante $G_n:=\exists v_n F_n \Rightarrow F_n[c_{\alpha(n)} / v_n]$ où $\alpha(n)$ est le plus petit entier $k$ (impair dans ma construction) tel que $c_k$ ne figure dans aucune des formules $G_0,G_1,...,G_{n-1}$ (ni dans les formules de la théorie de base,dont toutes les constantes sont indexées par un entier pair en l'espèce).