Forcing

En mathématiques, et plus précisément en logique mathématique, le forcing est une technique inventée par Paul Cohen pour prouver des résultats de cohérence et d'indépendance en théorie des ensembles. Elle a été utilisée pour la première fois en 1962 pour prouver l'indépendance de l'hypothèse du continu vis-à-vis de la théorie ZFC. Combinée avec la technique des modèles de permutation de Fraenkel-Mostowski-Specker, elle a permis également d'établir l'indépendance de l'axiome du choix relativement à ZF. Le forcing a été notablement remanié et simplifié dans les années 1960 et s'est révélé être une technique extrêmement puissante, à la fois en théorie des ensembles et dans d'autres branches de la logique mathématique, comme la théorie des modèles ou la logique intuitionniste. Le forcing est équivalent à la méthode des , qui est parfois ressentie comme plus naturelle et intuitive, mais qui est en général plus difficile à appliquer. Intuitivement, le forcing consiste à étendre l'univers V. Dans cet univers plus large, V*, on pourra par exemple avoir de nombreux nouveaux sous-ensembles de ω = {0,1,2,...} qui n'existaient pas dans l'univers V, violant ainsi l'hypothèse du continu. A priori impossible, cette construction ne fait que refléter l'un des « paradoxes » de Cantor concernant l'infini, et en particulier le fait qu'il existe des modèles dénombrables de ZFC, contenant pourtant des ensembles non dénombrables (au sens du modèle), d'après le théorème de Löwenheim-Skolem. En principe, on pourrait par exemple considérer , identifier avec , et introduire une relation d'appartenance étendue mettant en jeu les « nouveaux » ensembles de la forme . Le forcing est une version élaborée de cette idée, réduisant l'expansion à l'existence d'un nouvel ensemble, et permettant un contrôle fin des propriétés de l'univers ainsi étendu. La technique initialement définie par Cohen, connue à présent sous le nom de , est légèrement différente du forcing non ramifié qui sera exposé ici.