Méthode de forçage utilisée dans l'article sur la relativisation de Baker-Gill-Solovay et la preuve de l'indépendance de l'hypothèse de continuum de Cohen

Je m'intéresse généralement à la méthode de forçage utilisée par Baker-Gill-Solovay et Cohen. Je recherche autant de sources que possible sur la technique elle-même ou son utilisation. Quelqu'un a-t-il des suggestions?

Pour plus d'utilisations du forçage (via des oracles soi-disant génériques) dans la théorie de la complexité, voir The Oracle Builder's Toolkit ( disponible gratuitement sur la page d'accueil de Fortnow ) par Fenner, Fortnow, Kurtz et Li. Ils donnent une théorie générale des oracles génériques et montrent ses nombreuses applications en complexité.

Si vous êtes intéressé par la façon dont les oracles dans la complexité sont comme des preuves d'indépendance dans la théorie des ensembles, vous pourriez être intéressé par les articles suivants:

• Arora, Impagliazzo, Vazirani. Techniques relativisantes ou non relativisantes: le rôle de la vérifiabilité locale .

• Impagliazzo, Kabanets, Kolokolova. Une approche axiomatique de l'algèbre . ( version complète disponible gratuitement sur la page d'accueil de Kabanets )

Pour les utilisations du forçage dans la théorie des ensembles, voir le livre Set Theory ( Set Theory on Amazon ) de Jech, en particulier les parties II et III du livre (à ne pas confondre avec "Introduction to Set Theory" de Hrbáček et Jech).

Pour une excellente introduction au forçage dans la théorie des ensembles, il y a le célèbre article USENET de Timothy Chow "Forcing for dummies" ainsi que le document plus formel qui en découle, "A beginner's guide to forcing" .

Pour les utilisations du forçage comme des techniques dans la complexité de la preuve, vous voudrez peut-être regarder:

• M. Ajtai. La complexité du principe du pigeonnier . Dans les actes du 29e symposium annuel de l'IEEE sur les fondements de l'informatique, White Plains, NY, 1988, pp. 346–355; et

• M. Ajtai. La complexité du principe du pigeonnier . Combinatorica 14 (1994), no. 4, 417–433.

La méthode de la preuve est un analogue arithmétique du forçage (d'un type déjà utilisé par Paris et Wilkie). Des combinaisons plus combinatoires (et des limites inférieures améliorées) figurent dans J. Krajıcek, P. Pudlak et A. Woods, Limites inférieures exponentielles à la taille de la profondeur limitée . 15–39. et T. Pitassi, PW Beame et R. Impagliazzo, Limites inférieures exponentielles pour le principe du pigeonhole , Comput. Complexity, 3 (1993), p. 97–140.

Voir également:

• $p$

• Soren Riis. Finitisation en arithmétique bornée . 1994, BRICS, Département d'informatique Université d'Aarhus.

Récemment, Jan Krajicek a publié un livre unifiant ces techniques de forçage:

• J. Krajicek. Forçage avec variables aléatoires et complexité de la preuve . Cambridge University Press, déc. 2010. ( Projet disponible sur la page d'accueil de Krajicek )

voir aussi Forcing in proof theory par Avigad, 30pp, 2004. il cite BGS75 mais pas en détail. il est fait référence à Scott / Solovay comme une reformulation du forçage en modèles à valeur booléenne.

Les idées de forçage ont eu une influence sur la complexité informatique; par exemple, la séparation des classes de complexité relavitisées dans un oracle (par exemple, comme dans BGS75) peut souvent être considérée comme des versions de forçage limitées par les ressources.