Théorie des ensembles et logique mathématique

raoul.S

Thierry Poma a dit :
Inutile d'être hypocrite, l'arsenal de la théorie des ensembles a été abondamment utilisé...

Sans oublier que pour avoir la forme la plus générale possible du théorème de compacité pour le calcul propositionnel, ils utilisent l'axiome du choix au niveau intuitif, sans être dans ZFC. Disons qu'on s'autorise pas mal de choses au niveau méta...

Médiat_Suprème

Oui, je pensais à cela, c'est "un peu" ce que je disais à Homo Topi sur un autre fil, mais je ne vois pas cela comme flou.
C'est le cas pour toutes les théories non catégoriques (et encore on peut discuter ce point)

Quant aux théories d'ordre supérieur, je suis assez d'accord pour parler de flou dans la mesure où l'ensemble des parties que l'on parcourt avec un quantificateur est rarement indiqué.

Foys

raoul.S a dit :

Thierry Poma a dit : 

Inutile d'être hypocrite, l'arsenal de la théorie des ensembles a été abondamment utilisé...

Sans oublier que pour avoir la forme la plus générale possible du théorème de compacité pour le calcul propositionnel, ils utilisent l'axiome du choix au niveau intuitif, sans être dans ZFC. Disons qu'on s'autorise pas mal de choses au niveau méta...

La bonne nouvelle est que la partie de la logique qui est nécessaire pourfonder les maths n'utilise pas ces chapitres. Ils peuvent être vus comme un  plus. Des ouvrages comme Bourbaki: "théorie des ensembles" ou encore (pour la théorie des ensembles authentique on va dire) le livre de Krivine, sont totalement self contained (sauf si vous avez l'impression de dépendre des mathématiques pour repérer les pages d'un livre par leurs numéros).

raoul.S

Foys a dit : 
sauf si vous avez l'impression de dépendre des mathématiques pour repérer les pages d'un livre par leurs numéros

Généralement les livres ont un nombre fini de pages, donc ça va. J'imagine le Krivine avec un nombre $\omega$ de pages...

Foys a dit :
La bonne nouvelle est que la partie de la logique qui est nécessaire pourfonder les maths n'utilise pas ces chapitres. Ils peuvent être vus comme un  plus.

Oui, le dire n'aurait pas été un luxe je trouve. Pour un débutant ça peut être déroutant.

Foys

@raoul.S ce fait est peu connu mais en fait lorsque le langage est dénombrable ces théorèmes (complétude/compacité) sont intuitionnistes.

Pour le calcul des prédicats, voir: https://www.irif.fr/~krivine/articles/completude.pdf

De façon générale, soit $X:=\{d_n, n \in \N\}$ un ensemble dénombrable et $\mathcal C$ un ensemble de parties de $X$ tel que pour tout $Y \subseteq X$, $Y$ est dans $\mathcal C$ si et seulement si toutes ses parties finies sont dans $\mathcal C$ (on dit que $\mathcal C$ est de "caractère fini" lorsque cette condition est réalisée). Alors tout élément de $\mathcal C$ est contenu dans un élément de $\mathcal C$ qui est maximal pour l'inclusion (Teichmüller-Tukey).

Preuve: Noter que l'hypothèse entraîne que $\mathcal C$ est stable par sous-ensemble.

lemme: soit $Y\subseteq X$ et $t\in X$. Soit $A(Y,t):=Y \cup \{x\in X \mid x = t \wedge Y \cup \{t\} \in \mathcal C\}$. Alors si $Y\in \mathcal C$, $A(Y,t) \in \mathcal C$.

En effet, par définition, $A(Y,t)\subseteq Y \cup \{t\}$. Soit $F := \{u_1,...,u_n\}$ une partie finie de $A(Y,t)$. Alors pour tout $i=1,,...,n$, $u_i \in Y$ ou $u_i = t$. Donc (c'est intuitionniste: faire une récurrence sur $n$) $F$ est contenu dans $Y$ ou bien $t\in F$.

Dans le premier cas $F\in \mathcal C$ par la remaque ci-dessus. Dans le second, $F = F \cup \{t\}\subseteq A(Y,t)$. Donc $t \in A(y,t)$. Donc $t\in Y$ et donc $A(Y,t) = Y$ donc $A(Y,t) \in\mathcal C$, ou alors $t \in \{x\in X \mid  x = t \wedge Y \cup \{t\} \in \mathcal C\}$ et donc $Y \cup \{t\} \in \mathcal C$. Comme $A(Y,t)$ est un sous-ensemble de $Y \cup \{t\}$ donc à nouveau, $A (Y,t) \in \mathcal C$.

Montrons le lemme de Teichmüller-Tukey. Soit $Z=: Z_0 \in \mathcal C$. Pour tout entier $n$, on pose par récurrence $Z_{n+1}:= A(Z_n,d_n)$.

On pose $Z_{\infty}:= \bigcup_{n\in \N} Z_n$. Alors $Z_{\infty}$ est l'ensemble maximal cherché. En effet:

(i) par récurrence et en exploitant le lemme ci-dessus, $n\mapsto Z_n$ est une suite croissante et pour tout $n$, $Z_n \in \mathcal C$

(ii) soit $F\subseteq Z_{\infty}$ une partie finie. Alors par récurrence sur le nombre d'éléments de $F$ et en exploitant (i) ci-dessus, il existe $k\in \N$ tel que $F\subseteq Z_k$.

Il résulte de (i) et (ii) que pour toute partie finie $G$ de $Z_{\infty}$, $G\in \mathcal C$ et donc que $Z_{\infty } \in \mathcal C$.

Montrons la maximalité de $Z_{\infty}$. Soit $A\in \mathcal C$, tel que $Z_{\infty} \subseteq A$. Soit $x\in A$. ll existe $n\in \N$ tel que $x=d_n$. Alors $Z_n \cup \{d_n\} \subseteq A$ et donc $Z_n \cup \{d_n\} \in \mathcal C$ (puisque $\mathcal C$ est stable par sous-ensemble) et donc $d_n \in Z_{n+1} = A(Z_n,d_n)$. Donc $d_n \in Z_{\infty}$ et donc $A \subseteq Z_{\infty}$ ce qui conclut la preuve.

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

Le théorème de complétude et le théorème de compacité du calcul des prédicats en découlent aussitôt lorsque le langage est dénombrable. On suppose à cet effet toutes les formules écrites avec $\to$. On note $P$ leur ensemble. Pour tout $X \subseteq P$ et toute $\psi \in P$, on note $X \vdash \psi$ pour "$\psi$ est conséquence prouvable de $X$" dans un système de preuves permettant la logique classique, voir plus bas (*)

On appelle "modèle propositionnel" ou simplement "modèle" toute partie $Q$ de $P$ telle que pour tous $\sigma, \theta\in P$, $(\sigma \to \theta \in Q) \Leftrightarrow \left [ (\sigma \in Q) \Rightarrow (\theta \in Q)\right ]$ et telle que pour tous $\alpha,\beta \in P$, $((\alpha \to \beta) \to \alpha) \to \alpha \in Q$ (cette deuxième condition découlerait automatiquement de la première si on était en logique classique).

(*)Comme système de preuves on peut prendre: $H \vdash \epsilon$ si:

(pr1) $\epsilon \in H$

(pr2) $\epsilon$ est de l'une des formes suivantes: $\alpha \to (\beta\to \alpha)$, $(\alpha \to (\beta \to \gamma)) \to ((\alpha \to \beta) \to (\alpha \to \gamma))$, ou encore $((\alpha \to \beta) \to \alpha) \to \alpha$ où $\alpha, \beta,\gamma \in P$.

(pr3) il existe $\delta\in P$ telle que $H \vdash \delta$ et $H \vdash \delta \to \epsilon$

NB: dans beaucoup de cas concrets il existe $\omega \in P$ tel que $H$ contient toutes les formules de la forme $\omega \to \varphi$, avec $\varphi \in P$. Dans de tels cas $\omega$ est un symbole dédié, par exemple "$\perp$". Le présent développement n'a pas besoin de le supposer cependant.

Soit $T$ un ensemble de formules, $\varphi$ une formule et on note $\mathcal C:= \{E \subseteq P \mid (T \cup E \vdash \varphi) \Rightarrow T \vdash \varphi\}$. Alors $\mathcal C$ est de caractère fini (provient de ce qu'une preuve ne fait appel qu'à un nombre fini d'hypothèses). Soit $M\subseteq P$ maximal pour l'inclusion. Alors on peut montrer que $M$ est un modèle contenant $T$.

Finalement: Soit $U$ un ensemble de formules et $\omega$ une formule telle que pour toute partie finie $V$ de $U$, il existe un modèle contenant $V$ et pas $\omega$. Alors $U$ ne prouve pas $\omega$ et la construction précédente fournit un modèle contenant tout $U$ et non pas $\omega$. 

Foys

Je parle d'ensembles finis mais tout est faisable en COQ (remplacer ensemble fini par liste etc).

raoul.S

Ok merci Foys. Je ne connaissais pas le lemme de Teichmüller-Tukey.

PS. J'ai l'impression de lire Krivine... tu ne serais pas lui par hasard ?

Foys

Ca n'est pas moi!