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.