Dans cet exposé (très largement inspiré des travaux de Krivine présentés en juin dernier), je propose d'étudier à travers la correspondance de Curry-Howard la transformation de preuves sous-jacente à la méthode de forcing. Pour cela, je me placerai en arithmétique d'ordre supérieur (PAw) avec termes de preuves à la Curry. Je définirai d'abord la transformation qui à une proposition A associe la proposition p ||- A (où p est une condition arbitraire), puis une transformation t |-> t^ sur les termes de preuves bruts (i.e. non typés) telle que si t : A, alors t^ : p ||- A. Je montrerai alors comment le terme traduit effectue ses calculs, et en quoi il est légitime de voir cette transformation comme la mise en place d'un petit système d'exploitation.