Problème dans la démonstrations du théorème de complétude

Congru

Bonjour, dans la démonstration classique du théorème de complétude, et notamment dans la construction d'une théorie consistante qui a des témoins de Henkin, n' y a-t-il pas un problème dans le "choix" des témoins ?

N.B. Je trouvais déjà cette construction bizarre quand j'étais étudiant, en me replongeant sur le sujet, je la trouve même incomplète (il faut dire comment ce choix est fait) maintenant.

Cyrano

Cette démonstration utilise le méta-axiome du choix. 

Congru

Bonjour @Cyrano, le seul endroit où on aurait éventuellement besoin d'utiliser l'axiome du choix c'est dans la complétion de la théorie. Le choix des témoins peut se faire sans l'axiome du choix. Le pire dans tout ceci c'est que quoiqu'on choisisse de faire, il faudrait au moins clarifier comment on choisit ces témoins, dans la démonstration classique on dit juste "on rajoute un nouveau symbole de constante $c_F$ pour chaque formule $F$ à une seule variable libre", cela donne un nouveau langage et on refait de même $\aleph _0$ fois ...

C'est horrible.

Cyrano

Sauf erreur de ma part, la fonction $F \mapsto c_F$ est une fonction de choix. Il faut préciser les ensembles sous-jacents bien entendu.
Par ailleurs, pour démontrer que la théorie consistante avec témoins de Henkin est incluse dans une théorie complète consistante avec témoins de Henkin, on utilise le lemme de Zorn. (La théorie complète étant en fait celle qui est maximale consistante.)

Congru

Définition: $[apply]fx:=f(x)$

Définition: $\pi _1 (x;y)=x$

Définition: on appelle fonction choix toute application $f$ tel que $\forall x(x\in [dom]f\implies [apply]fx\in x)$.

L'axiome du choix dit que pour tout ensemble $A$ dont aucun élément n'est vide, il existe une fonction choix de domaine $A$.

Mais tu n'as pas nécessairement besoin de cet axiome pour montrer qu'un ensemble a une fonction choix. Par exemple si tu prends un ensemble $E$ d'espaces vectoriels tel que $\forall x\forall y((x\in E\wedge y\in E\wedge \pi _1x=\pi _1y)\implies x=y)$ , $\{\pi _1 x\vert x\in E\}$ a une fonction choix, pas besoin de l'axiome du choix.

J'affirme qu'il est possible de choisir les témoins sans aucunement utiliser l'axiome du choix.

samok

J'ai appris ce soir que déduction et sémantique sont équivalentes mais que ça se discute.
Après le théorème de Pythagore qui n'est pas de Pythagore, les témoins de Henkin, qui méta-axiomatiquement existent, ils sont de Henkin ou pas
Bien à vous.

Congru

Pas mal, @samok

samok

Louis Henkin (1917-2010), un des penseurs les plus influents sur les lois internationales et la politique étrangère des États-Unis. A l'université Columbia, il est professeur émérite à la Faculté de droit. Il dirige, jusqu'à la fin de sa vie, le Centre d'études des droits humains de l'université Columbia.

Même pas mal ?

Foys

Ces raisonnements n'utilisent pas du tout d'axiome du choix. Ils se basent sur l'idée suivante: soit $T$ une théorie du premier ordre  (i.e. un ensemble de formules du premier ordre sur un certain langage), $C$ un ensemble  contenant toutes les variables libres des formules de $T$, $F$ une formule dont toutes les variables libres sont dans $C \cup \{x\}$ (où $x$ peut appartenir ou non à $C$, peu importe). Soit enfin $\theta$ une lettre n'appartenant pas à $C$.

Remarque importante : on suppose dans toute la suiteque $T$ démontre au moins un énoncé de la forme $\exists y H$, où $H$ est une formule à variables libres dans $C \cup \{y\}$,  où $y$ est une lettre.

Cette circonstance est automatiquement vérifiée si le langage contient au moins un symbole de constante (le résultat qui va suivre est une variante du "paradoxe du buveur" et est faux dans un univers vide).

Résultat fondamental qui est à la base de toutes ces constructions à la Henkin:
$T \cup \{(\exists x F) \Rightarrow F[x:= \theta]\}$ est une extension conservative de $T$ (pour la logique classique).

Il s'agit d'un simple exo de théorie de démonstration.
Pour le voir soit $G$ un énoncé à variables libres dans $C$ qui est conséquence de $T \cup \{(\exists x F) \Rightarrow F[x:= \theta]\}$.

On va voir que $T \cup \{\neg \exists x F\} \vdash G$ (1) et $T \cup \{\exists x F\} \vdash G$ (2). Ainsi le résultat va découler du tiers exclu.

(1) : Soit $H$ tel que $T \vdash \exists y H$. On rajoute $\theta$ aux variables déclarées du système (contexte). $T  \cup \{\neg \exists x F, H[y:= \theta]\} $ entraîne $\exists x F \Rightarrow F[x := \theta]$ ($\neg A \Rightarrow (A \Rightarrow B )$ est une tautologie du calcul propositionnel pour tous $A, B$). Or par hypothèse $T \vdash ((\exists x F) \Rightarrow F[x:= \theta]) \Rightarrow G$ et donc (affaiblissement) $T \cup \{\neg \exists x F, H[y:= \theta]\} \vdash ((\exists x F) \Rightarrow F[x:= \theta]) \Rightarrow G$. Donc au final, $T \cup \{\neg \exists x F, H[y:= \theta]\} \vdash G$. Mais comme $\theta$ ne figure (libre) ni dans $G$ ni dans $T$ ni dans $\exists x F$ et que par hypothèse, $T\vdash \exists y H$ (et donc a fortiori $T\bigcup \{\neg \exists x F\} \vdash \exists y H$), on a $T \cup \{\neg \exists x F\} \vdash G$ par la règle d'élimination du quantificateur existentiel appliqué à $\exists y H$.

(2): $T \cup \{\exists x F, F[x:= \theta]\}$ entraîne $F[x:= \theta]$ et donc aussi $(\exists x F) \Rightarrow F[x:= \theta]$ (rappel: $A \Rightarrow (B \Rightarrow A)$ est une tautologie). Comme au (1) on en déduit que $T \cup \{\exists x F, F[x:= \theta]\} \vdash G$. comme $\theta$ ne figure libre ni dans $G$ ni dans $T$ ni dans $\exists x F$ et que $T \cup \{\exists x F\} \vdash \exists x F$, on en déduit par la règle d'élimination du quantificateur existentiel que $T \cup \{\exists x F\} \vdash G$. D'où le résultat.

####################################################

Le théorème de complétude (de Henkin) consiste à itérer la construction précédente afin de ramener la logique du premier ordre à une logique propositionnelle.

IMPORTANT: la construction qui suit est ALGORITHMIQUE (pas d'axiome du choix ou que sais-je).

En effet, supposons désormais le langage $L$ sous-jacent au propos dénombrable (c'est toujours le cas dans les situations concrètes). On suppose que $T$ démontre au moins un énoncé de la forme $\exists y H$ (cf plus haut). Soit $T$ une théorie du premier ordre sur $L$ et dont toutes les variables libres sont dans un ensemble dénombrable $C$.

Soit $D:= \{\gamma_n, n\in \N\}$ un ensemble dénombrable de constantes disjoint de $C$. Soit $n \mapsto \Phi_n$ une fonction surjective de $\N$ dans l'ensemble $K$ de toutes les formules de $L$ à variables dans $\{x\} \cup C \cup D$. On suppose également (*) que pour tout $F \in K$, $\Phi^{-1} (\{F\})$ est infini (i.e. la suite atteint chaque formule une infinité de fois ce qui est toujours possible si on remplace $\Phi$ par sa composée avec une fonction de $\N$ dans $\N$ qui a cette propriété, comme la fonction qui à $n\in \N$ associe le plus grand entier $m$ tel que $2^m$ divise $n$).

Alors on construit une suite de formules analogues à celles du théorème du premier paragraphe et une suite d'entiers en posant $u_0:= 0$ $X_0:=\exists y H$,  et pour tout $n\in \N$:

(i) si toutes les variables libres de $\Phi$ sont dans $\{x, \gamma_0, \gamma_1, .... \gamma_{u_{n - 1}}\}$, on pose $u_n = 1+u_{n-1}$ et
$X_n:= \exists x \Phi_n \Rightarrow \Phi_n[x:= \gamma_{u_n}]$.

(ii) si la condition de (i) n'est pas remplie on pose $X_n:= \exists y H$ et $u_n := u_{n-1}$

On pose enfin $T':= T \cup \{X_n, n\in \N\}$. La condition de répétition (*)  va entraîner que pour tout entier $n$, il existe $k$ tel que $\exists x \Phi_n \Rightarrow \Phi_n[x:= \gamma_k]$ est dans $T'$; d'autre part, par une récurrence évidente et le théorème du premier paragraphe, $T'$ est une extension conservative de $T$.

Enfin on pose $T'':= T \cup S$ où $S$ est l'ensemble de toutes les formules de $L$ avec $C \cup D$ comme ensemble de variables, et de la forme $F[z:= t] \Rightarrow \exists z F$, où $t$ est un terme quelconque de $L$ (avec $C \cup D$  comme ensemble de variables.

Alors comme tous les énoncés de $S$ sont prouvables (au premier ordre et sans aucune hypothèse), $T''$ est à nouveau une extension onservative de $T$.

L'idée est que l'ensemble des théorèmes propositionnels (i.e. ceux démontrés sans utiliser aucune règle portant sur les quantificateurs, en supposant mettons toutes les formules écrites avec $\exists, \neg, \Rightarrow$) de tout surensemble de $T''$ est exactement l'ensemble de ses théorèmes tout court.

Le théorème de complétude est obtenu en prenant alors un surensemble maximal consistant (au sens des démonstrations propositionnelles) de formules contenant $T''$ (cf lemme de Teichmüller -Tukey qui ne requiert pas l'axiome du choix; il en existe même des preuves intuitionnistes).

Foys

Je rappelle ce qu'est le lemme de Teichmüller-Tukey.

Soit $A:=\{a_n \mid n\in \N\}$ un ensemble dénombrable et $\mathcal B$ un ensemble de parties de $A$ qui a la propriété suivante:

Pour tout $X\subseteq A$, $X$ appartient à $\mathcal B$ si et seulement si toutes les parties finies de $X$ appartiennent à $\mathcal B$.

Alors tout élément de $\mathcal B$ est contenu dans un élément de $\mathcal B$ maximal pour l'inclusion.

Preuve: Soit $Y_0\in \mathcal B$. Pour tout entier $n\geq 1$, on pose $Y_n:= Y_{n-1}$ si $Y_{n-1} \cup \{a_{n-1}\} \notin \mathcal B$, et on pose $Y_n:= Y_{n-1} \cup \{a_{n-1}\}$ si $Y_{n-1} \cup \{a_{n-1}\} \in \mathcal B$. Alors la partie $\bigcup_{n\in \N} Y_n$ de $A$ possède la propriété voulue.

(la preuve intuitionniste de ce résultat est un peu plus astucieuse, je l'avais mise sur le phorum il y a quelques années de ça)

###############################

Comme une démonstration, notamment d'une contradiction, ne fait jamais appel qu'à un nombre fini de formules et notamment d'axiomes, l'ensemble $\mathcal B$ des théories consistantes (une théorie n'est jamais qu'un ensemble de formules) sur un ensemble dénombrable de formules $A$ vérifie clairement les hypothèses du lemme de Teichmüller-Tukey, d'où son application au théorème de complétude de mon dernier paragraphe.

Cyrano

Merci pour ce développement intéressant dans le cas où $\mathcal{L}$ est dénombrable.
Il est vrai que je partais du principe qu'on allait traiter d'un langage quelconque, en mentionnant l'axiome du choix.

Congru

Merci @Foys.

J'étais trop fatigué pour lire cela hier, mais c'est très instructif ce que tu écris.

Congru

Donc, voilà ce que je propose pour la construction à la Henkin.
On prend un langage du premier ordre $L_0$.
Soit $R$ l'ensemble des symboles de raltions de $L_0$, soit $V$ l'ensemble des variables de $L_0$, soit $N$ l'ensemble des symboles de fonction de $L_0$.
On se fixe  $c:= \{t\in  \bigcup \bigcup \bigcup \{ V;R;N \} \vert t\not \in t\}$.

...Début de construction:
Soit $[fv]$ une fonction qui à chaque formule de $L_0$ associe l'ensemble de ses varibales libres.
Soit $F:=\{g\in \mathcal F L_0\vert [cardinal][fv]g=1\} $.
On définit $L_1:= \bigcup \{L_0; F\times \{c \} \}$
On définit de la même façon $L_2$ à partir de $L_1$ ...
...Fin de construction

On définit $L:=\bigcup \{ L_i\vert i\in \mathbb N\}$. Soit $[FV]$ une fonction qui à toute formule de $L$ associe l'ensemble de ses variables libres. Soit $W:=\{a \in \mathcal F L\vert [cardinal][FV]a=1\}$.
L'ensemble des témoins de Henkin serait alors $C:=W\times \{ c \}$.

Edit. J'ai pris l'idée de la diagonale de @Foys, dans l'autre fil:
https://les-mathematiques.net/vanilla/discussion/2337239/transformer-un-couple-en-un-couple-densembles-disjoints#latest

Edit2. Je fais la construction de $L_2$: soit $[fv_1]$ une fonction qui à chaque formule de $L_1$ associe l'ensemble de ses variables libres, soit $F_1:=\{g\in \mathcal F L_1\vert [cardinal][fv_1]g=1\} $. On définit $L_2:= \bigcup \{L_1; F_1\times \{c \} \}$

Congru

OK, la rédaction est correcte maintenant