Démonstration théorème de complétude — Les-mathematiques.net The most powerful custom community solution in the world

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$ ?120572

Réponses

  • Désolé pour le dérangement. On applique juste l'axiome à la formule $F_{w/c}$.

    Je raconte n'importe quoi. J'en reviens donc à ma question initiale.
  • Ca n'est pas important, $(\forall v(F_{w/c})) \Rightarrow ((F_{w/c})_{s/v})$ est un axiome (je n'ai pas la liste sous les yeux mais j'imagine que ce type de formule en fait partie, c'est le cas dans un certain nombre de présentations) avec $s:=t_{w/c}$.
    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).
  • J'ai compris, merci beaucoup !
  • Bonjour,

    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 ?
  • On travaille avec des structures relevant de l'informatique en réalité. Les variables libres vont être des entiers ou assimilés. Rien n'empêche de prendre une théorie dont les constantes sont indexées par $\N$ i.e. $(c_n)_{n\in \N}$ et de remplacer partout $n$ par $2n$, les entiers impairs fournissant d'emblée les indices d'une infinité de nouvelles constantes à ajouter à la volée au besoin.
    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).
  • Merci beaucoup pour vos explications.
Connectez-vous ou Inscrivez-vous pour répondre.
Success message!