<p>For an excellent introduction to forcing in set theory, there's Timothy Chow's famous USENET post <a href="http://www-math.mit.edu/~tchow/mathstuff/forcingdum">"Forcing for dummies"</a> as well as the more formal paper that arose from it, <a href="http://www-math.mit.edu/~tchow/forcing.pdf">"A beginner's guide to forcing"</a>.</p>

CC BY-SA 3.0
2012-10-28T00:39:24.293Z
2012-10-28T04:51:12.633Z
2012-10-28T04:51:12.633Z
arnab
<p>For uses of forcing like techniques in proof complexity you might want to look at:</p>

<ul>
<li><p>M. Ajtai. <a href="http://doi.ieeecomputersociety.org/10.1109/SFCS.1988.21951" rel="nofollow">The complexity of the pigeonhole principle</a>. In Proceedings of the 29th Annual IEEE Symposium on Foundations of Computer Science, White Plains, NY, 1988, pp. 346–355; and</p></li>
<li><p>M. Ajtai. <a href="http://dx.doi.org/10.1007/BF01302964" rel="nofollow">The complexity of the pigeonhole principle</a>. Combinatorica 14 (1994), no. 4, 417–433. </p></li>
</ul>

<p>The method of proof is an arithmetical analogue
of forcing (of a kind already used by Paris and Wilkie). More combinatorial (and improved lower bounds) are in J. Krajıcek, P. Pudlak, and A. Woods, <a href="http://www.ams.org/mathscinet-getitem?mr=1346282" rel="nofollow">Exponential lower bounds to the size of bounded depth Frege proofs of the pigeonhole principle</a>, Random Structures Algorithms, 7 (1995),
pp. 15–39. and T. Pitassi, P. W. Beame, and R. Impagliazzo, <a href="http://dx.doi.org/10.1007/BF01200117" rel="nofollow">Exponential lower bounds for the pigeonhole
principle</a>, Comput. Complexity, 3 (1993), pp. 97–140. </p>

<p>See also: </p>

<ul>
<li><p>Miklos Ajtai. <a href="http://eccc.hpi-web.de/report/1994/014/" rel="nofollow">The Independence of the modulo $ p$  Counting Principles</a>. ECCC 1994.</p></li>
<li><p>Soren Riis. <a href="http://www.brics.dk/RS/94/23/" rel="nofollow">Finitisation in Bounded Arithmetic</a>. 1994, BRICS, Department of Computer Science University of Aarhus.</p></li>
</ul>

<p>Recently, Jan Krajicek published a book unifying these forcing techniques:</p>

<ul>
<li>J. Krajicek. <a href="http://www.ams.org.myaccess.library.utoronto.ca/mathscinet-getitem?mr=2768875" rel="nofollow">Forcing with Random Variables and Proof Complexity</a>. Cambridge University Press, Dec. 2010. (<a href="http://www.karlin.mff.cuni.cz/~krajicek/fdraft.html" rel="nofollow">Draft available from Krajicek's homepage</a>)</li>
</ul>

CC BY-SA 3.0
2012-10-31T17:15:21.960Z
interesting leap but havent seen anyone in papers/books actually compare forcing to pigeonhole principle/proofs...?
vzn
CC BY-SA 3.0
2012-11-01T06:35:26.377Z
Pigeonhole Principle here is a name of a statement. To show that the statement is independent of a certain theory one uses forcing-like constructions. The references above show how to do this.
Iddo Tzameret
CC BY-SA 3.0
2012-11-01T18:50:12.703Z
ok, but exponential size proofs of SAT using resolution (via pigeonhole constructions) are not "independent" it would seem... they are just "large"... any online refs pointing the connection out? admit am a bit surprised because many refs on pigeonhole proofs in SAT do not refer to anything about "forcing"....
vzn
CC BY-SA 3.0
2012-11-02T05:15:21.847Z
Establishing super-polynomial size lower bounds on propositional proofs for a (uniform) family of propositional statements implies the independence of the corresponding first- (or second-) order formula in the corresponding first- (or second-) order formal theory. E.g., the pigeonhole principle is independent (i.e., true in the standard model, but unprovable) of $V^0$, namely, the theory of "$AC^0$ reasoning"  which corresponds to constant-depth Frege (this is *NOT* resolution); (I use here the terminology of Cook & Nguyen, Logical Foundation of Proof Complexity, 2010; See Cor. VII.2.4 there).
Iddo Tzameret
CC BY-SA 3.0
2012-11-02T05:16:14.607Z
(cont.) See also Jan Krajicek's book "Bounded Arithmetic, Propositional Logic, and Complexity Theory", Cambridge, 1995, on this. All references above (excluding Krajicek's 1995 book) are available on-line. The connection with forcing is explained in e.g., the 2nd reference of Ajtai above.
Iddo Tzameret
CC BY-SA 3.0
2012-10-30T12:15:08.273Z
2014-07-11T12:28:37.493Z
2014-07-11T12:28:37.493Z
Iddo Tzameret
<p>see also <a href="http://repository.cmu.edu/cgi/viewcontent.cgi?article=1040&amp;context=philosophy" rel="nofollow">Forcing in proof theory</a> by Avigad, 30pp, 2004. he cites BGS75 but not in detail. there is some reference to Scott/Solovay as a rephrasing of forcing into boolean-valued models.</p>

<blockquote>
  <p>Ideas in forcing have been influential in computational complexity; for example, the separation of complexity classes relavitized to an oracle (e.g., as in BGS75) can often be viewed as resource-bounded versions of forcing.</p>
</blockquote>

CC BY-SA 3.0
2012-10-28T16:08:51.447Z
2012-10-28T16:08:51.447Z
vzn
<p>For more uses of forcing (via so-called generic oracles) in complexity theory, see <a href="http://dx.doi.org/10.1016/S0890-5401(03)00018-X">The Oracle Builder's Toolkit</a> (<a href="http://www.cs.uchicago.edu/~fortnow/papers/obt.pdf">freely available from Fortnow's homepage</a>) by Fenner, Fortnow, Kurtz, and Li. They give a general theory of generic oracles, and show its many applications in complexity. </p>

<p>If you're interested in how oracles in complexity are like independence proofs in set theory, you might be interested in the following papers:</p>

<ul>
<li><p>Arora, Impagliazzo, Vazirani. <a href="http://cseweb.ucsd.edu/~russell/ias.ps">Relativizing versus Nonrelativizing Techniques: the Role of Local Checkability</a>.</p></li>
<li><p>Impagliazzo, Kabanets, Kolokolova. <a href="http://dx.doi.org/10.1145/1536414.1536509">An Axiomatic Approach to Algebrization</a>. (<a href="http://www.cs.sfu.ca/~kabanets/Research/algebrization.html">full version freely available from Kabanets's homepage</a>)</p></li>
</ul>

<p>For the uses of forcing in set theory, see the book <a href="http://www.ams.org/mathscinet-getitem?mr=1940513">Set Theory</a> (<a href="http://rads.stackoverflow.com/amzn/click/3540440852">Set Theory on Amazon</a>) by Jech, especially Parts II and III of the book (not to be confused with "Introduction to Set Theory" by Hrbáček and Jech).</p>

CC BY-SA 3.0
2012-10-25T15:52:06.527Z
2012-10-25T15:52:06.527Z
Joshua Grochow
<p>I am generally interested in the forcing method used by Baker-Gill-Solovay and Cohen.  I am looking for as many sources as I can get my hands on concerning either the technique itself or its use. Does anyone have suggestions?</p>

CC BY-SA 3.0
2012-10-26T05:02:56.977Z
who points out that its the same technique?
vzn
CC BY-SA 4.0
2023-08-27T05:27:08.457Z
I second @vzn, i've never seen anyone seriously unifying both constructions. There is some analogy between the results, and the idea of constructing some artificial objects, but that is very very superficial. Presumably one could formalize some things in common, but that would not lead to new insights. Now that does not mean actual forcing (as invented by Cohen) could not be very useful in complexity theory, it has led to some results in weak arithmetic theories, but just that BGS' result, and their idea of relativization, is not a case of forcing (as invented by Cohen).
plm
<cc.complexity-theory><set-theory>
Forcing method used in Baker-Gill-Solovay Relativization paper and Cohen's Proof of Continuum Hypothesis Independence
djkern
# Forcing method used in Baker-Gill-Solovay Relativization paper and Cohen's Proof of Continuum Hypothesis Independence

(Asked by: username_0 on 2012-10-25)

I am generally interested in the forcing method used by Baker-Gill-Solovay and Cohen. I am looking for as many sources as I can get my hands on concerning either the technique itself or its use. Does anyone have suggestions?

**Tags:** cc.complexity-theory, set-theory
> **Comments:**
> **username_1**: who points out that its the same technique?  
> **username_2**: I second @vzn, i've never seen anyone seriously unifying both constructions. There is some analogy between the results, and the idea of constructing some artificial objects, but that is very very superficial. Presumably one could formalize some things in common, but that would not lead to new insights. Now that does not mean actual forcing (as invented by Cohen) could not be very useful in complexity theory, it has led to some results in weak arithmetic theories, but just that BGS' result, and their idea of relativization, is not a case of forcing (as invented by Cohen).  

---

## 4 answers

### Answer by username_5 on 2012-10-25. Score: 17 | Accepted answer

For more uses of forcing (via so-called generic oracles) in complexity theory, see [The Oracle Builder's Toolkit](http://dx.doi.org/10.1016/S0890-5401(03)00018-X) ([freely available from Fortnow's homepage](http://www.cs.uchicago.edu/~fortnow/papers/obt.pdf)) by Fenner, Fortnow, Kurtz, and Li. They give a general theory of generic oracles, and show its many applications in complexity.

If you're interested in how oracles in complexity are like independence proofs in set theory, you might be interested in the following papers:

* Arora, Impagliazzo, Vazirani. [Relativizing versus Nonrelativizing Techniques: the Role of Local Checkability](http://cseweb.ucsd.edu/~russell/ias.ps).
* Impagliazzo, Kabanets, Kolokolova. [An Axiomatic Approach to Algebrization](http://dx.doi.org/10.1145/1536414.1536509). ([full version freely available from Kabanets's homepage](http://www.cs.sfu.ca/~kabanets/Research/algebrization.html))

For the uses of forcing in set theory, see the book [Set Theory](http://www.ams.org/mathscinet-getitem?mr=1940513) ([Set Theory on Amazon](http://rads.stackoverflow.com/amzn/click/3540440852)) by Jech, especially Parts II and III of the book (not to be confused with "Introduction to Set Theory" by Hrbáček and Jech).


---

### Answer by username_3 on 2012-10-28. Score: 11

For an excellent introduction to forcing in set theory, there's Timothy Chow's famous USENET post ["Forcing for dummies"](http://www-math.mit.edu/~tchow/mathstuff/forcingdum) as well as the more formal paper that arose from it, ["A beginner's guide to forcing"](http://www-math.mit.edu/~tchow/forcing.pdf).


---

### Answer by username_4 on 2012-10-30. Score: 10

For uses of forcing like techniques in proof complexity you might want to look at:

* M. Ajtai. [The complexity of the pigeonhole principle](http://doi.ieeecomputersociety.org/10.1109/SFCS.1988.21951). In Proceedings of the 29th Annual IEEE Symposium on Foundations of Computer Science, White Plains, NY, 1988, pp. 346–355; and
* M. Ajtai. [The complexity of the pigeonhole principle](http://dx.doi.org/10.1007/BF01302964). Combinatorica 14 (1994), no. 4, 417–433.

The method of proof is an arithmetical analogue
of forcing (of a kind already used by Paris and Wilkie). More combinatorial (and improved lower bounds) are in J. Krajıcek, P. Pudlak, and A. Woods, [Exponential lower bounds to the size of bounded depth Frege proofs of the pigeonhole principle](http://www.ams.org/mathscinet-getitem?mr=1346282), Random Structures Algorithms, 7 (1995),
pp. 15–39. and T. Pitassi, P. W. Beame, and R. Impagliazzo, [Exponential lower bounds for the pigeonhole
principle](http://dx.doi.org/10.1007/BF01200117), Comput. Complexity, 3 (1993), pp. 97–140.

See also:

* Miklos Ajtai. [The Independence of the modulo $ p$ Counting Principles](http://eccc.hpi-web.de/report/1994/014/). ECCC 1994.
* Soren Riis. [Finitisation in Bounded Arithmetic](http://www.brics.dk/RS/94/23/). 1994, BRICS, Department of Computer Science University of Aarhus.

Recently, Jan Krajicek published a book unifying these forcing techniques:

* J. Krajicek. [Forcing with Random Variables and Proof Complexity](http://www.ams.org.myaccess.library.utoronto.ca/mathscinet-getitem?mr=2768875). Cambridge University Press, Dec. 2010. ([Draft available from Krajicek's homepage](http://www.karlin.mff.cuni.cz/~krajicek/fdraft.html))

> **Comments:**
> **username_1**: interesting leap but havent seen anyone in papers/books actually compare forcing to pigeonhole principle/proofs...?  
> **username_4**: Pigeonhole Principle here is a name of a statement. To show that the statement is independent of a certain theory one uses forcing-like constructions. The references above show how to do this.  
> **username_1**: ok, but exponential size proofs of SAT using resolution (via pigeonhole constructions) are not "independent" it would seem... they are just "large"... any online refs pointing the connection out? admit am a bit surprised because many refs on pigeonhole proofs in SAT do not refer to anything about "forcing"....  
> **username_4**: Establishing super-polynomial size lower bounds on propositional proofs for a (uniform) family of propositional statements implies the independence of the corresponding first- (or second-) order formula in the corresponding first- (or second-) order formal theory. E.g., the pigeonhole principle is independent (i.e., true in the standard model, but unprovable) of $V^0$, namely, the theory of "$AC^0$ reasoning"  which corresponds to constant-depth Frege (this is *NOT* resolution); (I use here the terminology of Cook & Nguyen, Logical Foundation of Proof Complexity, 2010; See Cor. VII.2.4 there).  
> **username_4**: (cont.) See also Jan Krajicek's book "Bounded Arithmetic, Propositional Logic, and Complexity Theory", Cambridge, 1995, on this. All references above (excluding Krajicek's 1995 book) are available on-line. The connection with forcing is explained in e.g., the 2nd reference of Ajtai above.  

---

### Answer by username_1 on 2012-10-28. Score: 4

see also [Forcing in proof theory](http://repository.cmu.edu/cgi/viewcontent.cgi?article=1040&context=philosophy) by Avigad, 30pp, 2004. he cites BGS75 but not in detail. there is some reference to Scott/Solovay as a rephrasing of forcing into boolean-valued models.

> Ideas in forcing have been influential in computational complexity; for example, the separation of complexity classes relavitized to an oracle (e.g., as in BGS75) can often be viewed as resource-bounded versions of forcing.


---

