Talk:Forcing (mathematics)

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Mathematics (Rated B-class, Mid-priority)
WikiProject Mathematics
This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of Mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Mathematics rating:
B Class
Mid Priority
 Field:  Foundations, logic, and set theory

Formating Math[edit]

I'm a bit new to the guidelines for formatting math in WP, so forgive me if this isn't in line with the policies. I don't have the symbol &#x22a9. Seems like here would be a good place to use <math>, especially since this is a critical symbol and I can't tell what it is.--Luke Gustafson 08:08, 21 December 2005 (UTC)

Which browser are you using? I have edited the article to use the LaTeX symbol, but generally this is not preferred for inline symbols. Have you seen the same problem on other browsers and computers? - Gauge 23:54, 7 January 2006 (UTC)

What to Add/Remove[edit]

Since this is a pretty bulky wiki, I propose to delete the stuff on finding a generic filter that's already in the Rasiowa-Sikorski lemma, namely:

The existence of such a G is follows from the Rasiowa-Sikorski lemma. In short, because M is really countable, one can enumerate the dense subsets of P in M as D0, D1, …. (In general, M thinks the number of such dense subsets is uncountable, and hence this enumeration is not in M. This is a version of the Skolem paradox.) By assumption, there exists p0∈D0. Then by density, there exists p1≤p0 with p1∈D1. Repeating, one gets …≤p2≤p1≤p0 with pi∈Di. Then G={ q∈P : ∃i, q ≥ pi } is a generic filter. In fact, slightly more is true: given a condition p ∈ P, one can find a generic filter G such that p ∈ G. This holds because one can start with p0 ≤ p.

Any objections? Baarslag 22:12, 17 July 2005 (UTC)

I agree, it might as well go, it's redundant with Rasiowa-Sikorski lemma and sort of interrupts the flow of the article.--Luke Gustafson 08:08, 21 December 2005 (UTC)

I am interested in adding a lot of basic graduate level set theory to WP. The existing articles on forcing, constructibility, large cardinals and the like strike me as terribly lame, mere conceptual stubs. On the other hand, this stuff is not trivial, and perhaps people don't want it on WP. What I've written is a first draft, perhaps too hard, perhaps too much notation, in other words, perhaps not worth it. In particular, at the moment the article is in an internally inconsistent state. It's unclear to me whether I should go forward or not.

So I'll wait for comments.

If the consensus is it's too much, I'll accept that and even do the revert myself.

But I think I can provide a good outline here, and even summarize other various famous results with decent outlines of the proofs, from Martin's axiom to the Solovay model and more-- 19:49, 1 Mar 2005 (UTC).

There is no reason why such material should not be here. I've written some stubby things on set theory, and they're stubby because my energies have been devoted to other subjects; I'd have to re-learn the subject. (In very elementary "naive" set theory, I've contributed to Cantor's theorem, Cantor–Bernstein–Schroeder theorem, and others.) Michael Hardy 22:23, 1 Mar 2005 (UTC)
What I'm most uncertain about is if I'm walking over a general outline that serves a useful purpose that I'm incapable of seeing. My reaction is "no way", "lame", etc., here, and in related articles, and I have been noticing a proliferation of very high level stubs and red links for topics which really can't have a low level description.
Anyway, I'll wait a day or two and see if there is more feedback.-- 22:48, 1 Mar 2005 (UTC)

I've expanded things, and I hope it is clearer. More to come in a few days.

In the long run, I expect it best to break this up into smaller articles. Presumably c.c.c. and the delta-system lemma (implicit in my write up) deserve their own pages, along with cardinal collapsing. In fact, every forcing poset should have its own page in the end. But for now, I think it best to keep everything on one page. (That is why I've decided to keep Boolean-valued models here for now.)-- 17:24, 3 Mar 2005 (UTC)

Notation and Names[edit]

Aleph4: the most common convention is pq, regardless of whether you are forcing up or down. So, yes, Shelah typically has later letters stronger, but I'm following the down convention.-- 20:23, 7 Mar 2005 (UTC)

First: I am not questioning the "down" convention. Stronger conditions are smaller -- at least if Boolean algebras are involved, anything else would lead to madness.
I didn't think you were trying to change the convention. Perhaps more papers are written with the up convention, just by counting Shelah's output, but everyone else pretty much follows the down convention, for precisely the reason you mentioned. Since at some point the article is going to directly compare forcing with BAs, there's no choice at the WP-level but to follow the down convention.
In fact, Shelah has been known to cheat. In PAIF he was once doing something so complicated, he tells the reader just to take the appropriate "Boolean" combination of conditions, despite that fact that the algebra is upside down.
But in the current article (mainly written by you, it seems; great job!), in most cases the weaker condition is called p, the stronger is q or r. (Look at your definition of "generic filter", for example. This is quite natural, because -- as you undoubtedly know -- most proofs proceed along the lines of
"Let p be an arbitrary condition, then we can find a stronger q deciding bla. ... We can now strengthen q even further to r such that..."
Or, slightly more formally: take any lemma that you prove in a forcing argument, write it in prenex form. If the matrix asserts that p is stronger than q, for two variables p and q, then almost always p will appear after q in the string of quantifiers. Which means that it is more Special:Watchlistnatural (linguistically of course) to choose the names in the opposite order.
For sure! In the middle of a forcing proof, you will typically go to the next letter in the alphabet when you need a stronger condition. But when it comes to first defining the forcing, it is most natural to pick p on the left, and q on the right, with the inequality in-between whichever it happens to be. This is what Jech and Kunen do.
I don't think there will be very many forcing arguments at the level where taking stronger conditions matters. The proofs will all be outlines, right? The generic filter will be looked at, the implications of it existing will be followed, I will try to name names of interesting objects, in short, the issue shouldn't come up.
Anyway, it is not a big deal... -- Aleph4 21:24, 7 Mar 2005 (UTC)
Given that I've got a bunch of expansion lined up, I think convention tweaking should be saved until it's clear what's best for the upcoming article as a whole, when it's time to split it up. For an example of how I'm thinking, when it comes to the Suslin hypothesis, I will kill Suslin lines directly, using their topologies as the posets, with no mention of the trees. My write-up on measure forcing has been influenced, obviously, for the sake of the Solovay model down the road, but also for its similarity to this way of killing Suslin lines. (Please don't tell me its "original research". It's way too trivial to publish separately, and just somehow never got noticed by the textbook writers when running on historical inertia. As far as I'm concerned, it's change-of-notation.)-- 22:57, 7 Mar 2005 (UTC)
Btw, I don't think your definition of the name of the random real is correct. If I would write the text, I would use a name for its Dedekind cut, something like , but apparently you want to really work in ... -- Aleph4 23:55, 7 Mar 2005 (UTC)
It's effectively (read, intuitively) equivalent to giving the decimal expansion of the random real. It's my experience that the constructive approach is easier to understand (not just me, but most people), and if you can't actually give the constructive approach, then mimicking it goes a long way towards comprehensibility. When it comes to actually doing the mathematics of random reals, the existing approaches in terms of what the generic filter converges to is certainly more efficient.
Also, this approach in terms of intervals will be very similar to the forthcoming Suslin line topology self-destruct argument. Instead of decimal based intervals, there will be maximal antichains of open intervals. The one interval which is in the generic filter gets split by a countable but non-dense subset, giving more intervals. Now iterate ω1 many times. See the similarity?-- 14:53, 8 Mar 2005 (UTC)
Still not quite right. You mean ((n,k) ̌, [...]), I guess. Assuming that "decimal expansion" is a shorthand for "infinite sequence of decimal digits", and not "nested tower of decimal intervals".
Well, I consider "decimal expansion" shorthand for whatever fits the given situation. That's probably a poor attitude on my part, but it is one of those terms we all learn way before we are ready for formal definitions. As it is, I want to keep it in nested interval form, since it's the simplest. The generic filter literally contains the "decimal expansion", so to speak.
If you identify reals with sets (not sequences) of nested decimal intervals, the name should be { (Eˇ, E): E is of the form [k.10-n, (k+1).10-n]} -- Aleph4 10:22, 10 Mar 2005 (UTC)
Well, duh, me. Of course. Actually, that's much better, since it looks almost identical to the canonical name G for G.-- 13:50, 10 Mar 2005 (UTC)
Btw, my default font does not show the spacing character (u+2005) correctly, and in fact it obscures the "check" (u+030c) following it; this is much worse than having the check a little bit off-center. (I assume that if my browser displays it incorrectly, then there is a positive measure set of other users with the same problem.) -- Aleph4 18:19, 8 Mar 2005 (UTC)
How does xˇ look to you? That's x followed by a non-combining hacek. I'll change them, if this is satisfactory.
Looks fine to me -- Aleph4 10:22, 10 Mar 2005 (UTC)
Actually, when I use IE 6.0, much of the Unicode is messed up. Switching the encoding doesn't seem to make a difference.-- 20:04, 8 Mar 2005 (UTC)
Have you tried changing the math settings in your preferences? Logicnazi 01:52, 30 August 2007 (UTC)

Needs Editing[edit]

Some things need adding:

Some points (which are maybe obvious to everyone else, but confused the hell out of me when I studied this material):

  • It needs to be clear that (mostly for useful applications) G \not \in M
  • Also M \neq M[G]
  • the notion of absoluteness needs to be metioned a bit more to give the flavor
  • be clear that c.c.c. is not absolute!

Another thing that I found very useful was seeing forcing conditons as being analogous to Cauchy sequences forcing real numbers into existence from the rationals, using e.g. the surd symbols as things to compose names with. I don't know how rigourous this analogy can be made, (and thus how appropriate it is) but it certainly helped me.

Some things need correcting:

Complete atomless Boolean algebra B is always uncountable and by this reason it can not be in countable transitive model M. But for application in forcing satisfying of sentence "B is complete" by model M suffices. This means that for any . Nedeljko Stefanovic (talk) 18:17, 11 October 2011 (UTC)

What you're missing is that, in the Boolean-valued model approach, there ordinarily just isn't any countable transitive M in the picture. One looks at sentences whose truth value in VB is 1 (the greatest element of B). A countable transitive M is generally superfluous. --Trovatore (talk) 08:15, 11 October 2011 (UTC)

This is true for Boolean valued forcing, but it is also true for the traditional Cohen's approach. Both approaches, traditional Cohen's and Boolean valued have both approaches - syntax and semantic. One can start with a countable transitive model M and make generic extension M[G] (semantic approach) or one can doing everything in V by calculating what formula (evaluated by names) is forced by what condition or what is Boolean value of what formula evaluated by names (syntax approach). Forcing relation between conditions and formulas evaluated by names is definable syntactical and Boolean value of formula evaluated by names. Relation between traditional and Boolean valued forcing is: The Boolean valued forcing can be considered as the special case of the traditional forcing where the complete atomless Boolean algebra (with excluded 0) is chosen as poset. The general case of traditional forcing is reducible this special case. Boolean value of formula (where are names) is exactly supremum of all conditions (i.e. elements of Boolean algebra) that forces . Also, if we start with a transitive countable model M, generic filters are always ultrafilters and iff Boolean value of is in G.

Yes, definability of the traditional forcing relation also eliminates need for transitive model in the traditional approach. Nedeljko Stefanovic (talk) 18:17, 11 October 2011 (UTC)

The whole point of the Boolean-valued approach is that it is semantic, but does not need a countable model. The compromise is that you have to liberalize your semantics so that they are no longer two-valued, but take truth values in B. But having done that, there is really no point in dragging in a countable model, or at least I have never seen a reason to do so. --Trovatore (talk) 10:01, 11 October 2011 (UTC)

Traditional forcing relation can also be defined in V. What is essential difference between computing the Boolean value of formula and computing what is forced by what condition? No fundamental difference. Your notes are also true for the traditional forcing. Nedeljko Stefanovic (talk) 18:15, 13 October 2011 (UTC)

You can perhaps argue that there's no fundamental difference. I don't think it's a good use of our time to argue that point. Whether there's a fundamental difference or not, nevertheless the Boolean-valued approach is not treated in the literature using countable transitive models. My basic reference is Bell, Boolean-valued models and independence proofs in set theory, which does not mention countable transitive models except perhaps once in an exercise. This make sense to me; I don't know why you would go to all the trouble to set up Boolean-valued semantics, only to pass to a transitive countable model, which then allows you to use two-valued semantics. --Trovatore (talk) 19:21, 13 October 2011 (UTC)

Move to Forcing_(Set Theory)[edit]

I'm about to make an edit to the introduction mentioning the use of forcing in areas other than set theory, in particular in recursion theory (hopefully sometime I can even write up that article). There has even been a bit of use of forcing in model theory even though for the most part they just define genericity directly without forcing.

However, I'm wondering if we would be better off moving all the stuff specific to set theory to it's own page and using this page as a short description of the basic concept (truth by meeting dense sets or something) and providing links to the different notions. Let me know if you object otherwise someday I might get around to doing this (though I should probably write up the recursion theory page first).Logicnazi 01:38, 30 August 2007 (UTC)

Forcing is used in many areas, sure, but we can probably keep it in one article. The applications to recursion theory are more esoteric (in some sense) so they could probably be kept to a section in this article plus a mention in the lede. THe idea of coming up with a general definition of forcing is nice, but it isn't done much in the literature, and it needs to appear there before appearing here. — Carl (CBM · talk) 01:52, 30 August 2007 (UTC)
As things stand, forcing is split into two categories on the disambiguation page: mathematics and recursion theory. I think a single page on forcing, with perhaps links to more specifics on forcing in set theory, recursion theory, model theory, what have you, would be reasonable. But if not, surely we ought not to have recursion theory portrayed as though it does not belong to mathematics, no? I will change the disambiguation page to "Forcing (Set Theory)".

Reviving an old topic... I changed the disambiguation page. Anyone object to renaming this page Forcing (set theory) (i.e., having the point do the reverse of what it does now)? Recursion theory is a part of mathematics, so this seems to me just wrong. —Preceding unsigned comment added by Ddzhafar (talkcontribs) 15:49, 10 March 2010 (UTC)

I think it's reasonable to have a page called forcing (mathematics) (or possibly forcing (mathematical logic)) that treats all flavors of forcing. The set-theoretic version will probably be the most prominent because it's the one with which the most has been done, but the others should be represented as well. Right now forcing (recursion theory) is pretty slim and I don't know why the content couldn't be merged here. If someone wanted to do enough with recursion-theoretic forcing to warrant a separate article, then I would treat that article as a fork, with a summary section in this article and a {{main}} pointing to the forked article. --Trovatore (talk) 20:40, 10 March 2010 (UTC)

Proofs seem to gloss over a lot[edit]

Where did we get a transitive model from? The Mostowski collapsing theorem only works if the membership relation is well-founded. Is there some trick in model theory that gives us a model with a well-founded membership relation? It's easy to come up with models of ZFC that aren't well-founded using hyperproducts, but how do we find one that is well founded?

What is the point in saying: "Note that we don't actually want or need to produce a model M for all of ZFC (or ZFC + ~CH), but merely the finite portion we subsequently use in the proof; Gödel's second incompleteness theorem prevents us creating a model for the whole theory." Since our goal is to show that ZFC+~CH is equiconsistent with ZFC, I thought we assumed that ZFC is consistent (which gives us a model of ZFC by Gödel's completeness theorem).

The proof seems to skip over the fact that M[G] satisfies all the axioms of ZFC. This seems non-trivial, especially showing that the axiom of choice holds in M[G]. Incidentally, to show that M[G] satisfies all the axioms implicitly shows that ZFC is consistent, which means that we must have assumed that ZFC was consistent (since this can't be demonstrated from ZFC). So the quoted text above is really irrelevant and misleading. (unless I'm misunderstanding the structure of the proof... see below).

Back on the axiom of choice: if forcing can be used to show the independence of the axiom of choice, then it mustn't necessarily hold in M[G]. So don't we need to demonstrate that the model that satisfies ~CH also satisfies the axiom of choice? Or any of the other axioms, for that matter...

The article needs to make clearer the distinction between things that exist inside of M and things that are being done from the outside. For example, the P-names exist within M, but their valuations don't (since G isn't in M).

Also, the definition of antichain isn't the standard one given in Antichain. Those should be called "strong antichains."

The general framework of the proof seems hard to understand. The first few times I read this, I thought that we were given a model of ZFC, and creating a model of ZFC+~CH. However, it now seems like the idea behind this proof is to assume that we have a proof of CH, which necessarily uses a finite set of axioms, and then to use a Reflection principle to find some set M that satisfies enough axioms to show that M[G] satisfies the finite set of axioms, and also ~CH. This shows that any proof of CH also gives a proof of a contradiction, so that ZFC is equiconsistent with ZFC+~CH. -- 23:09, 7 September 2007 (UTC)

(Responding mostly to the final paragraph, but partly to the first paragraph) well, forcing is a whole technology, not a single proof structure with fill-in-the-blanks. The way that you would organize a proof of (for example) the independence of CH from ZFC, depends on what you want out of the proof.
So if all you want is to show that Con(ZFC)→Con(ZFC+¬CH), and if you want to show this with minimum assumptions in the metatheory, then yeah, you can arrange it as a purely syntactic proof, and you should be able to carry it out in just Peano Arithmetic as your metatheory, which means you don't officially have any models running around at all -- Peano Arithmetic just deals with natural numbers so it's pretty limited when it comes to proving things about models. But the way you would get that proof is by first understanding a proof using wellfounded models, and then painstakingly translating. I would venture to guess that no one has actually done this, just convinced themselves and others that "in principle" it could be done.
But if what you want at the end is a description of an actual model of ZFC in which CH fails, and you want to be able to ask other questions about the model itself (not just its first-order theory), then more likely what you want to do is start with a wellfounded model of ZFC and force over that. The existence of such a model does not follow, strictly speaking, from Con(ZFC) itself, so you need to assume more.
These are general remarks; I'm not really talking about the proof in the article as it stands. I haven't read it in detail, at least not recently. --Trovatore (talk) 09:11, 12 December 2007 (UTC)

Dumb Question[edit]

Am I missing something? I am not much of a mathematician, but I see a problem in the following definition:

Name(0) = {};
Name(α + 1) = the power set of (Name(α) × P);
Name(λ) = ∪{Name(α) : α < λ}, for λ a limit ordinal,

The second line worries me. I always thougt that A × B = {(a,b): a ∈ A \wedge b ∈ B}. It follows from this that {} × X = {} for any X, and hence, by induction, that V(P) = ∪{Name(α) : α is an ordinal} = {}.

I can only assume that something else is meant. For example, it would work if you used {{}} or P in the first line instead of {}. The result would be different, but not significantly: every tuple would get a {} appended to the front if you used {{}} rather than P.

This may seem like a pedantic quibble, but, like a lot of people (I should think), I am struggling with the concepts anyway, and throwing in logical inconsistencies doesn't help. Rdbenham (talk) 06:18, 2 April 2009 (UTC)

It's true that the empty set cross anything is again the empty set. But the powerset of the empty set is not the empty set. So the definition works (or at least doesn't fail for the reason you think it does). It just takes one more iteration at the beginning to get going, than maybe you were expecting. --Trovatore (talk) 09:28, 2 April 2009 (UTC)
Yes, thanks for putting me straight about that. I should have looked into it more carefully. I last studied mathematics 30 years ago, and I am just now trying to get back into it. For some reason I ignored the powerset operation, maybe because it was written out in words rather than symbols.

Rdbenham (talk) 15:13, 5 April 2009 (UTC)

Cohen Forcing[edit]

I have a general question regarding notions of forcing that can be formulated exactly in the context of the section Cohen Forcing in this article.

I use notation as in the article. Additionally, let denote the universe of the model of set theory under consideration. The subset is not an element of as is shown in the article. I buy this. Equivalently, the function constructed from is not an element of (my conclusion).

Now, is constucted using axioms of set theory. From we get using union. If is a notion of forcing (as defined), then since is a filter. But then we must have since . It follows that

There is the possibility (close to a certainty) that I don't understand this. There is also the possibility that there is some fuzziness in the definition of a generic filter. If the definition of a generic filter reads G contains a filter or G behaves like a filter instead of G is a filter, then I'd be happier. I'd certainly be happier if the definition of a generic filter didn't require the subset property.

In short, I see an existing generic filter as paradoxical in this case unless the definitions are reworded. I have finally, after many years of layman interest in mathematics, acquired a real book , Set Theory by Thomas Jech. The passage in his book on this particular question (the same forcing notion is used) parallels the article more or less excatly, so that doesn't help me. YohanN7 (talk) 11:26, 21 May 2012 (UTC)

Reading the section Countable transitive models and generic filters didn't resolve matters. On the contrary, that section underlines my problems with this. When is a countable transitive model, then exists and and . It is the part of it that I can't digest. By transitivity, we get which hardly matches . YohanN7 (talk) 13:01, 21 May 2012 (UTC)

In the proof of the Rasiowa-Sikorski lemma a set qualifying as a generic filter is explicitly constructed. Must I reconsider what means for something to be a subset? Does this only show that is never ever a set, once again pointing out Russels Paradox? It doesn't make things better to allow for being a class. If is , the Von Neumann universe, things are the same in this respect. It appears to me that no model of set theory can be closed with respect to clever subset operations. YohanN7 (talk) 14:33, 21 May 2012 (UTC)

Taking note of the fact that transitive means that elements are subsets, there may be subsets that aren't elements in a transitive model?

I am desperate to keep subsets of subsets as subsets, so that if and . But then will appear as an element in , and should be closed under the power set operation. YohanN7 (talk) 16:41, 21 May 2012 (UTC)

The article about the Mostowski collapse lemma provides a clue: There exists a model M (assuming the consistency of ZF) whose domain has a subset A with no R-minimal element, but this set A is not a "set in the model" (A is not in the domain of the model, even though all of its members are).

Thus if our model is of the above type, then there is an escape hatch. I am still having trouble if our model is transitive to begin with. Back to the workbench. YohanN7 (talk) 09:39, 22 May 2012 (UTC)

I think my dilemma is resolved. I applied the Power Set Axiom incorrectly (quite whimsically actually). It reads


If one puts the forcing poset as A, then one might naively expect the generic set G to appear as one of the B's in P above because it is a subset of the forcing poset. The point here is that the variable B doesn't ever evaluate to G because G isn't an element in our model. Hence G is not an element in the power set either, consistent with what we had to begin with. (Also, I wrote above that one could the the power set of the whole model P(M). That is of course nonsense seen from within the model wether the model is a set (in a larger model) or not.)

Maybe I shouldn't have written about this at all in this talk page in the first place, but I think that the article could perhaps elaborate a little bit more than it does on the fact that the existence of generic sets isn't paradoxical. Subsets of sets aren't necessarily sets from the point of view of the model. B t w, I checked out the definition of the term subset and it says that a set is a subset if ... . What is the standard terminology? Does e.g. the generic set count as a subset of the forcing poset (in terms of terminology) even if it isn't a set in the model? YohanN7 (talk) 21:19, 30 May 2012 (UTC)