Compacité du calcul propositionnel

J'ai cru longtemps que ce résultat était une Zornerie un peu subtile ou au moins un corollaire du théorème des ultrafiltres. Il n'en est rien (dans le cas d'un ensemble dénombrable de formules or on a quand même affaire in fine à des suites finies de symboles).

I) d'abord quelques préliminaires:
Si $X$ est un ensemble et $P$ une partie de $\mathcal P(X)$, $P$ est dite de caractère fini si pour toute partie $Y$ de $X$, $Y \in P$ si et seulement si toutes les parties finies de $Y$ sont dans $P$.

Exemple: soit $X$ l'ensemble de tous les fermés d'un espace topologique $T$ et $P$ l'ensemble des parties de $X$ dont l'intersection est vide. Alors $P$ est de caractère fini si et seulement si $T$ est quasi-compact.

Lemme de Teichmüller-Tukey :
Soit $X$ un ensemble, $P$ une partie de $\mathcal P(X)$ de caractère fini et $Y \in P$. Il existe alors un élément $M \in P$ tel que $Y \subseteq M$ et $M$ est maximal pour l'inclusion.
-La preuve de ce résultat fait environ une demi-ligne avec le Lemme de Zorn et est laissée en exercice pour le lecteur.
-Ledit énoncé est en fait équivalent à l'axiome du choix
(Spoiler: c'est conséquence simple d'un énoncé cité plus bas ).

Le lemme de Teichmüller-Tukey permet des démonstrations rapides des résultats suivants:
1) Tout ensemble ordonné contient un sous-ensemble totalement ordonné maximal pour l'inclusion.
2°) Le théorèmes des idéaux maximaux dans un anneau.
3°) Si $H$ est une algèbre de Heyting, une partie $A\subseteq H$ est dite inconsistante s'il existe $x_1,...,x_n \in A$ tels que $\perp = x_1 \wedge ... \wedge x_n$ (et consistante sinon). Toute partie consistante de $H$ est contenue dans une partie consistante maximale $M$. Une telle $M$ a automatiquement la propriété suivante: pour tous $a,b \in H$, $a\vee b \in M$ si et seulement si $a\in M$ ou $b \in M$ (c'est un filtre premier en fait).
4°) (en fait un cas particulier de 3°)Soit $A$ une algèbre de Boole (un anneau dans lequel $x^2=x$ pour tout $x$): une partie $X$ de $A$ est inconsistante si $0$ est le produit d'une famille finie d'éléments de $A$ (et consistante dans le cas contraire). Toute partie consistante $X$ de $A$ est contenue dans une partie consistante maximale $M$ de $A$ et il s'avère que $A\backslash M$ est un idéal maximal et que le quotient de $A$ par cet idéal est isomorphe à $\mathbf F_2$, les éléments de $X$ s'envoyant sur $1$.

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

II) Cas où $X$ est dénombrable.
[size=large]En fait la partie I était une publicité pour montrer l'intérêt du lemme en bleu. Le résultat clé est que lorsque $X$ est dénombrable, le lemme de Teichmüller-Tukey est démontrable sans axiome du choix et ce de manière intuitionniste!!![/size]
Je suis tombé sur ce fait par hasard au cours de lectures il y a quelques jours et souhaitais le partager. Les détails (élémentaires) sont ci-dessous. En fait c'est même faisable en coq.

$(\dagger )$Dans ce qui suit, on appelle "parties finies" d'un ensemble $E$ les éléments de l'intersection de toutes les parties $\mathcal X$ de $\mathcal P (E)$ ayant les propriétés suivantes: i) $\emptyset \in \mathcal X$ ii) pour tout $A \in \mathcal X$ et tout $u \in E$, $A \cup \{u\} \in \mathcal X$.
(Cette définition convient pour les résultats de type compacité que nous envisageons et est équivalente au moins dans ZF classique à celle habituelle d'ensemble fini). Noter que par définition, pour tous $Y,t$, $s\in Y \cup \{t\}$ si et seulement si $s\in Y$ ou $s=t$.

Soit $X=\{x_n \mid n \in \N\}$ un ensemble, $P\subseteq \mathcal P(X)$ une propriété de caractère fini.
Soit $Y\subseteq X$ appartenant à $P$.
On pose $M_0:= Y$. Puis on définit par récurrence $M_{n+1}:= M_n \cup \left \{x \mid x=x_n \wedge (M_n \cup \{x_n\}) \in P \right \}$ (*)
Pour tout $n\in \N$, $M_n$ est dans $P$. Cela se fait par récurrence sur $n$.
NB: cf note en bas de page: en logique classique le résultat est trivial.
Si on s'interdit le tiers exclu, on peut procéder comme suit.
Le cas $n=0$ est juste la définition.
Soit $n \in \N$. Supposons $M_n$ dans $P$. Alors pour toute partie finie $X$ de $M_{n+1}$, on a $X\subseteq M_n$, ou il existe $Y\subseteq M_n$ fini tel que $Y \cup \{x_n\} = X$ $(\clubsuit)$. Pour le voir, il suffit de vérifier que l'ensemble des parties $X$
de $M_{n+1}$ vérifiant $(\clubsuit)$ satisfait les propriétés i) et ii) de la définition marron $(\dagger)$ ci-dessus.

- il est évident que $\emptyset$ satisfait $(\clubsuit)$
- Soient $T$ satisfaisant $(\clubsuit)$ et $u \in M_{n+1}$ alors il y a 4 cas:
(a)$T\subseteq M_n$ et $u\in M_n$:alors $T\cup \{u \} \subseteq M_n$
(b)$T = S\cup \{x_n\}$, $S\subseteq M_n $ et $u \in M_n$: alors $T\cup \{u\}= \left ( S \cup \{u\}\right ) \cup \{x_n\}$
(c) $T \subseteq M_n$, $u=x_n$ (et $M_n \cup \{x_n\} \in P$ quoique ça n'a pas d'importance ici): $T\cup \{u\}= T \cup \{x_n \}$.
(d) $T = S\cup \{x_n\}$, $S\subseteq M_n $ et $u=x_n$: $T \cup \{x_n\}=S \cup \{x_n\}$.

Bref $T \cup \{u\}$ vérifie $(\clubsuit)$ dans tous les cas, d'où la propriété voulue.
Montrons à l'aide de ce résultat que si $M_n$ est dans $P$ alors $M_{n+1}$ aussi.
Compte tenu de ce que $P$ est à caractère fini, il suffit d'établir que pour tout $F\subseteq M_{n+1}$ fini, $F \in P$. Considérons une tel $F$ et appliquons le lemme ci-dessus:
-si $F\subseteq M_n$, c'est l'hypothèse de récurrence.
-si $F = G \cup \{x_n\}$ avec $G$ fini, $x_n \in M_{n+1}$. Donc $x_n$ est dans $M_n$ ou bien $x_n=x_n$ et $M_{n+1}\in P$. dans le premier cas $F\subseteq M_n$ et on applique le fait que $P$ est de caractère fini. Dans le second, $F \subseteq M_{n+1}$ qui est encore de caractère fini et le tour est joué.

Comme tous les $M_n$ sont dans $P$ leur réunion $M$ aussi (si $F\subseteq \bigcup_{n \in \N} M_n$, il existe un entier $k$ tel que $F\subseteq M_k$ par un raisonnement trivial analogue à celui tenu plus haut pour $(\clubsuit)$, mais plus court)
Par suite $M \in P$.

Montrons que $M$ est maximal. Si $L\subseteq X$ vérifie $P$ et si $M\subseteq L$, soit $x\in L$. Alors il existe $n\in \N$ tel que $x_n = x$. Si $H$ est une partie finie quelconque de $M_n \cup \{x_n\}$, alors (cet ensemble étant une partie de $L$ et $P$ étant de caractère fini), $H \in P$. Donc $M_n \cup \{x_n\} \in P$. Donc $x = x_n \in M_n \cup \left \{t \in X \mid t = x_n \wedge M_n \cup \{x_n\} \in P \right \} = M_{n+1} \subseteq M$.

Cela démontre le résultat.

[size=x-small](*)pour la clarté: en fait si on écrit cette preuve en logique classique, $M_{n+1}=M_n$ si $M_n\cup \{x_n \} \notin P$, et $M_{n+1}= M_n \cup \{ x_n\}$ si $M_n \cup \{x_n\} \in P$[/size]