Le lemme de maximalité

Martial

Bonjour à tous,

Je suis en train de retravailler mon chapitre 21, consacré au forcing itéré (il y a du taf). J'en suis au lemme de maximalité, qui dit la chose suivante : Soient $\mathbb{P}$ un ordre partiel, et $\varphi(x)$ une formule ensembliste à une variable libre (et éventuellement à paramètres). Alors il existe un $\mathbb{P}$-terme $\tau$ tel que
$$\Vdash \exists x \varphi(x) \Rightarrow \varphi(\tau),$$
où l'écriture $\Vdash blabla$ signifie $\mathbb{1}_{\mathbb{P}} \Vdash blabla$ ou, ce qui revient au même, $\forall p \in \mathbb{P}, p \Vdash blabla$.

J'ai la preuve sous les yeux mais ce n'est pas tellement ça qui me pose problème. Ce que je ne vois pas c'est :
a) "en substance", que dit ce résultat ?
b) Quelle est l'utilité de ce fameux $\tau$ ?
c) Et aussi, quand se sert-on du lemme de maximalité ?

Merci d'avance pour vos écalircissements.

Foys

Ce résultat ressemble furieusement à celui qui dit qu'on peut ajouter des témoins de Henkin à une théorie du premier ordre. Si $u$ est une lettre non présente (en tant que variable libre) dans un ensemble d'énoncés $\Gamma$ et $F$ une formule du premier ordre à une variable libre $y$, alors $\Gamma \cup \{\exists y F \Rightarrow F[y:=u]\}$ est une extension conservative de $\Gamma$.
En fait $u$ est un exemple d'objet satisfaisant $F$ et nommé à l'avance (ou bien n'importe quoi si $F$ n'est satifsaite par rien).

Maxtimax

En principe, le $\mathbb P$-terme $\tau$ va représenter un élément de l'extension qui satisfait $\phi$ (si tant est que $\exists x, \phi(x)$ y est satisfaite)

Je pense que ce lemme est là pour te dire que les phrases que $1_\mathbb P$ force sont vraies dans l'extension par un générique - enfin, c'est l'étape "$\exists$" de cet énoncé :-D

Martial

Merci Foys et Max. J'ai du mal avec ces trucs. Je sais bien que c'est une histoire de témoin, mais ça ne me parle guère. (Alors qu'en revanche, pour les témoins de Henkin, j'ai compris... bon, pas du 1er coup mais j'y suis finalement arrivé).

Demain je vous donnerai un exemple d'exercice (que je ne sais pas résoudre) censé être une application immédiate du lemme de maximalité.

Bonne soirée à tous

christophe c

Ce terme est obtenu grâce à l'axiome du choix. C'est utile car te donne une terme "définitif" en quelque sorte, plutôt qu'avoir à gérer, pour chaque $p$ un terme $t(p)$ qui dépend de $p$.

C'est une sorte de propriété qui fait des modèles booléens (donc où tu n'as pas choisi encore un générique) des trucs très "platonisés", c'est à dire qui se rapprochent d'une situation où il n'y aurait in fine jamais besoin d'aller jusqu'à choisir un générique