It is a trivial fact that forcing can not produce finite sets of ground model objects. However there are situations, where we can use forcing to prove the existence of finite objects with some properties. For example consider the following result of Shelah (I learned this example from the answer given by Prof. Komjath in Forcing as a tool to prove theorems):

Theorem (Shelah) There exists a finite $K_4$-free graph which, when the edges colored by $2$ colors, always contains a monocolored triangle.

Shelah's proof of the theorem is simply as follows: He constructs a forcing extension which adds a graph $X$ with the same property but with $\aleph_0$ colors. Then $X$ has the edge-coloring property for $2$ colors, as well. Then using compactness theorem, $X$ must contain a finite subgraph $Y$ with the same property. As forcing cannot create new finite graphs, $Y$ is already present in the ground model. By Godel, $ZFC$ proves that there is such a graph.

Now my question is that if there are more examples of the above kind. To be more precise:

Question 1. Are there any other examples for producing some finite object $Y$ (with some properties) in the following way:

1) We provide a suitable generic extension in which there is an infinite object $X$ with the required properties,

2) By compactness (or other devices), we can conclude that there must be a finite subset $Y$ of $X$ with the same properties,

3) So we can conclude that the object must exist in the ground model.

Remark 1. I am mostly interested in examples where it is not known (or it is difficult) to produce such finite object directly

Remark 2. It seems that some partition type theorems are of this type: It is possible to derive some kind of finite partition theorems (like finite Ramsey theorem) using infinite versions of them. So if we can prove the infinite version of these partition theorems, then we have produced examples of the required type (there are cases where we can prove infinite partition theorems using forcing).

Question 2. Is Shelah's result the first non-trivial example of an answer to question 1? Are there othe non-trivial constructions of the above kind before him?

Remark 3. Here by non-trivial I mean the above strategy is, in some sense, the only method for producing the required finite object.


Question 3. Are there any results of the above type proved in other parts of mathematics other than logic?

Of course Shelah's result is of this type, but the example given by Hamkins is in mathematical logic.

  • $\begingroup$ See also mathoverflow.net/q/29945/1946 and mathoverflow.net/q/42569/1946. $\endgroup$ Dec 15, 2014 at 12:13
  • 1
    $\begingroup$ Not exactly what you're asking for because it doesn't involve forcing, but Harvey Friedman has used axioms beyond ZFC to prove the existence of finite objects. mathoverflow.net/questions/27864/… $\endgroup$ Dec 15, 2014 at 15:21
  • 1
    $\begingroup$ This comment is clearly outside the scope of this question, but I think is relevant: Using 'forcing' to construct an object is actually a common technique in intuitionist/constructive mathematics. The localic tychonof theorem, or the localic Hahn-Banach theorem can be sought of as theorem asserting that some object can be constructed in a forcing model ( a linear form or a point in an infinite product). And it is frequent that those "localic" theorem actually allows to construct an object by first constructing it in the new model and then using a descent argument. $\endgroup$ Dec 16, 2014 at 16:48
  • 1
    $\begingroup$ The Shelah result you quote fails to be "non-trivial" in the sense of being "the only method for producing the required finite object." A finite graph with that Ramsey property was constructed (without forcing!) by Jon Folkman, Graphs with monochromatic complete subgraphs in every edge coloring, SIAM J. Appl. Math. 18 (1970), 19–24, apparently some years before Shelah's forcing result. $\endgroup$
    – bof
    Jan 7, 2017 at 9:40

1 Answer 1


Here is another example.

The theorem is: every finite partial order can be found as a suborder of the partial order of the Turing degrees.

On the one hand, one can prove this by undertaking a priority construction, a detailed argument constructing the degrees directly. On the other hand, one can force to add countably many mutually generic Cohen reals $x_n$, and then noting that finite sums of them show that any finite power set algebra can be found in the degrees. But every finite partial order is a suborder of a finite power set order. Finally, the existence of any particular such pattern in the Turing degrees is a $\Sigma^1_1$ property and hence absolute to the ground model by Shoenfield absoluteness. So there was already such a pattern in the ground model.

A similar argument finds every countable order as a suborder of the Turing degrees. In both cases, what the direct argument amounts to is the construction of sufficiently generic degrees. With forcing, we can just go all the way to a fully generic real, and this simplifies things.

  • 1
    $\begingroup$ Although you mentioned a priority construction, I think your last paragraph implies that priority isn't really involved. Won't "the construction of sufficiently generic degrees" amount to a Kleene-Post argument? (Priority would presumably become relevant if you wanted to do this with c.e. degrees.) $\endgroup$ Dec 15, 2014 at 15:41
  • 1
    $\begingroup$ Yes, I agree with that, although don't we think of the priority argument as a more refined and careful version of the simpler constructions? It is easier just to get the degrees somewhere, and the priority construction produces c.e. degrees. Do you know if one may use this forcing way of thinking to get actual c.e. degrees? $\endgroup$ Dec 15, 2014 at 15:58
  • 1
    $\begingroup$ On the one hand, I don't ordinarily say "priority" when all the requirements are compatible, so no prioritization is needed. On the other hand, I suppose the hierarchy "finite injury, infinite injury, monster, ..." could be extended backward to "0 injury", which would be Kleene-Post. As for making "genuine" priority arguments look like forcing, I think there have been many attempts over the years, but I haven't really learned about any of them. Some (surely not all) of the relevant names are Yates, Lachlan, and Lerman. $\endgroup$ Dec 15, 2014 at 16:55
  • $\begingroup$ I had intended to inquire about whether we might undertake a more refined absoluteness argument, using actually generic objects, in order to produce a c.e. example of something, rather than merely making a priority argument look like forcing. But perhaps these aren't so different actually... $\endgroup$ Dec 15, 2014 at 17:13
  • 5
    $\begingroup$ But the question was about using forcing to prove the existence of a finite object. I'm not sure that a Turing degree, or even a finite set of Turing degrees, counts as a finite object. $\endgroup$
    – bof
    Dec 31, 2016 at 9:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.