Talk:Forcing (mathematics)
This level-5 vital article is rated B-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | |||||||||||
|
Formatting Math
editI'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 ⊩. 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
editSince 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--192.35.35.36 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.--192.35.35.34 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.)--192.35.35.36 17:24, 3 Mar 2005 (UTC)
Notation and Names
editAleph4: the most common convention is p ≤ q, regardless of whether you are forcing up or down. So, yes, Shelah typically has later letters stronger, but I'm following the down convention.--192.35.35.35 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.)--192.35.35.34 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?--192.35.35.36 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, 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.
- Well, duh, me. Of course. Actually, that's much better, since it looks almost identical to the canonical name G for G.--192.35.35.36 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.--192.35.35.35 20:04, 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.
- Have you tried changing the math settings in your preferences? Logicnazi 01:52, 30 August 2007 (UTC)
Needs Editing
editSome 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)
editI'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 (talk • contribs) 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
editWhere 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. --71.112.146.3 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
editAm 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.
Cohen Forcing
editI 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)
Math dummie question: "incomplete" versus "inconsistent"
edit"By Gödel's second incompleteness theorem, one cannot prove the consistency of any sufficiently strong formal theory, such as {\displaystyle {\mathsf {ZFC}}} {\displaystyle {\mathsf {ZFC}}}, using only the axioms of the theory itself, unless the theory is inconsistent."
Should the phrase "unless the theory is inconsistent" in this sentence read "unless the theory is incomplete" instead? Based on what little understanding I have of Godel that would seem to make more sense. Plus the idea that one cannot prove the consistency of a theory unless that theory is inconsistent doesn't ring true. But I could be mistaken! — Preceding unsigned comment added by Ron9500 (talk • contribs) 00:36, 2 December 2017 (UTC)
- By the principle of explosion, an inconsistent theory proves "everything" (that is, everything that can be expressed in its language), including its own consistency.
- With that explanation, do you have any suggestion for less confusing wording in the article? --Trovatore (talk) 00:49, 2 December 2017 (UTC)
Some sentences are more confusing than helpful
editThis is one example:
"Intuitively, forcing consists of expanding the set theoretical universe to a larger universe. In this bigger universe, for example, one might have many new subsets of ω = {0, 1, 2, ...} that were not there in the old universe, and thereby violate the continuum hypothesis.
"While impossible when dealing with finite sets, this is just another version of Cantor's paradox about infinity. "
Oops. What? What is "just another version of Cantor's paradox about infinity" ???
But wait! What is "Cantor's paradox about infinity" ??? Is that phrase a technical term? Not a term that is common. Of course, he has a number of *theorems* (like that aleph0 < 2aleph0), and there's his famous *hypothesis* that there are no in-between infinities. But what is "Cantor's paradox" ???
Suggestion: Either make that sentence a lot clearer, or remove it.2600:1700:E1C0:F340:857F:235F:86C8:1DDD (talk) 03:48, 24 April 2018 (UTC)
- From the explanation following that sentence, I suspect the writer was thinking about Hilbert's paradox of the Grand Hotel instead of Cantor's paradox. What really ought to be explained is the concept of models: I believe the approach the writer was really describing is to take as a (class) model of ZFC that is isomorphic to , and then try to expand this model with elements of .
- However, I'm not sure that such an approach could actually work. It seems counter-intuitive to me that there could exist an object that could be interpreted as a "new" subset of ω that is not in , and even though in fact such an object could exist (e.g. if itself is a countable model), I am not sure if it would be possible to describe that object within in any sense. This is why the "standard" approach is to take a transitive model that is "significantly smaller than" , and then expand using an object that can be described in .
- Should we rewrite the "Intuition" section completely? Bbbbbbbbba (talk) 08:42, 27 March 2023 (UTC)
- I tried to rewrite the section. However, now that I've studied forcing further, I've realized how much of forcing is working within , so it might indeed make sense to call it instead of , and/or talk more about what looks like from the inside of . I'm still under the impression that using a model in the first place is necessary for the soundness of the proof: Within we can prove various properties of , but only by looking at could we show that actually exists. (Apparently the way to get around the requirement that a standard model exists in the first place is to use models of finite fragments of ZFC, the existence of which is guaranteed by the reflection principle.) Bbbbbbbbba (talk) 01:17, 31 March 2023 (UTC)
Definition of
editShouldn't it have rather than ? As written, is not in . Unhandyandy (talk) 19:57, 16 March 2023 (UTC)
- If it is , then how is related to at all? Although I am also struggling to see the meaning of . The underline notation is only used below once for , which has a definition that seems not quite the same. Bbbbbbbbba (talk) 05:17, 17 March 2023 (UTC)
- The disappear in if . Unhandyandy (talk) 17:23, 17 March 2023 (UTC)
- The point is that is a way of referring to within . Unhandyandy (talk) 17:24, 17 March 2023 (UTC)
- Is there a need to define in this section (where neither nor has been defined yet) at all? The entire article is quite confusing, and it may be necessary to rethink about the organization completely. Bbbbbbbbba (talk) 19:08, 17 March 2023 (UTC)
- Good point, delaying till after has been introduced might help.
- Of course, forcing is a rather confusing subject, in that one must think on at least two levels, and , simultaneously. Maybe it would help if the article separated these levels more clearly throughout. Unhandyandy (talk) 20:48, 17 March 2023 (UTC)
- I am contemplating making some structural changes to this article, but since I don't feel familiar with forcing even after consulting some more reference materials, I'm not sure if I am a suitable person to do it. One of the things I wonder is if it is necessary for forcing to use a standard transitive model, or indeed any set model at all, or if there is some clever way to prove the necessary statements by directly working on . I'm wondering this because one of the references say that the existence of a standard model of ZFC is a stronger assumption than the consistency of ZFC. If the use of is necessary then I'll feel comfortable mentioning it in the first section or even in the introduction. Bbbbbbbbba (talk) 05:01, 27 March 2023 (UTC)
- I just found out from Boolean-valued model#Relationship to forcing that syntactic forcing is a viable approach that "directly works on ". I guess it is even less intuitive than using a model though... Bbbbbbbbba (talk) 02:00, 4 April 2023 (UTC)
- Is there a need to define in this section (where neither nor has been defined yet) at all? The entire article is quite confusing, and it may be necessary to rethink about the organization completely. Bbbbbbbbba (talk) 19:08, 17 March 2023 (UTC)
- The point is that is a way of referring to within . Unhandyandy (talk) 17:24, 17 March 2023 (UTC)
- The disappear in if . Unhandyandy (talk) 17:23, 17 March 2023 (UTC)
- Well, I fixed the immediate problem, but my head still hurts when I think about how to restructure this article. Bbbbbbbbba (talk) 18:02, 30 March 2023 (UTC)
Good example of a forcing poset?
editThis article currently states that "A good example of a forcing poset is , where and is the collection of Borel subsets of having non-zero Lebesgue measure." However, I am unsure whether this is actually a good example:
- The concepts of Borel subsets and Lebesgue measure may not be familiar to readers who are primarily interested in logic and set theory. For that matter, since we are talking about forcing posets and not Boolean algebras, why not just open intervals in ?
- The concept of Borel subsets is not very absolute (only real numbers in the universe can be used as endpoints of intervals). I guess for previous revisions of this article this was not a problem because at this point the idea of using a countable model hadn't been introduced yet, but I think introducing early is a less confusing way to talk about forcing.
- It is not immediately clear forcing with this poset gives a universe with what property (it contains a real number that is not constructible?).
I think the forcing poset used in Cohen forcing, (or even ), is simple enough for any reader to understand, and would be an improvement on all three of the points above. As a bonus, if we introduce this forcing poset here we won't need to introduce it later. Bbbbbbbbba (talk) 04:37, 8 April 2023 (UTC)
- Upon further reading, I realized that the Borel subsets example is connected to the "Random reals" section, and I guess for whatever reason open intervals do not suffice for this purpose. However that section itself is quite dense, and for now I still prefer the Cohen forcing example. Bbbbbbbbba (talk) 15:22, 22 April 2023 (UTC)
- The Cohen partial order is easier to understand in itself, but it may be harder to understand what the generic object added is, given that more people are familiar with measure than with category. Still, I kind of agree that if we want to give one p.o. as an example, the Cohen one is the obvious thing to start with. --Trovatore (talk) 19:21, 22 April 2023 (UTC)
- Hmm... Isn't the generic object added just a generic subset of or ? Where does category come into play? Bbbbbbbbba (talk) 19:36, 22 April 2023 (UTC)
- The generic object is an element of every comeager set with a Borel code in the ground model. --Trovatore (talk) 19:43, 22 April 2023 (UTC)
- Oh, so in the random forcing example, the generic object is an element of every Borel subset with measure 1 (again in the ground model). This is indeed a more intuitive description. I guess this might actually be a fine example if we talk about the this desirable property first and use it to motivate the mathematical process, instead of burying it deep in a bunch of math. Bbbbbbbbba (talk) 20:14, 22 April 2023 (UTC)
- You have to be a little careful. The generic real isn't in the ground model, so it's not in any sets in the ground model. But if there's a conull Borel set in the extension that has a Borel code that's in the ground model, then the generic real is in that set.
- Basically the idea is that the ground model knows enough to describe the set, and to figure out that its complement has measure zero. But it can't find the generic real in the set, because it can't "see" the generic real at all. The extension can see the generic real, and can unpack the description to see that the generic real is in the set.
- Whether that's reasonable to try to explain in the article I'm not sure. We probably don't want to go into full detail on Borel codes and their interpretation. We could maybe get as far as , which is enough (because every conull set has a conull subset). But even that is getting a little elaborate. It would be something like, we can code an open set by a countable sequence of pairs of rationals (because it's a countable union of intervals with rational endpoints), and then we can code a by a countable sequence of those codes (take the union of the complements of the open sets thus described). --Trovatore (talk) 22:53, 22 April 2023 (UTC)
- Oh, so in the random forcing example, the generic object is an element of every Borel subset with measure 1 (again in the ground model). This is indeed a more intuitive description. I guess this might actually be a fine example if we talk about the this desirable property first and use it to motivate the mathematical process, instead of burying it deep in a bunch of math. Bbbbbbbbba (talk) 20:14, 22 April 2023 (UTC)
- The generic object is an element of every comeager set with a Borel code in the ground model. --Trovatore (talk) 19:43, 22 April 2023 (UTC)
- Hmm... Isn't the generic object added just a generic subset of or ? Where does category come into play? Bbbbbbbbba (talk) 19:36, 22 April 2023 (UTC)
- The Cohen partial order is easier to understand in itself, but it may be harder to understand what the generic object added is, given that more people are familiar with measure than with category. Still, I kind of agree that if we want to give one p.o. as an example, the Cohen one is the obvious thing to start with. --Trovatore (talk) 19:21, 22 April 2023 (UTC)
"No mention of set or class models" in Cohen's original method?
editThe current "Consistency" section says: "Less commonly seen is the approach using the "internal" definition of forcing, in which no mention of set or class models is made. This was Cohen's original method, and in one elaboration, it becomes the method of Boolean-valued analysis."
When I read the references (both Cohen's paper The Independence of the Continuum Hypothesis in the external links section, and Cohen's 1966 book), it seems to me that Cohen mentions models a lot. I can imagine how one can avoid mentioning models (by focusing on formal consistency); I don't see how that was Cohen's original method.
I am also unsure how such a method is notably different from just "forcing over " (which the "Consistency" section mentions as a different approach). From my understanding, when forcing over , it is impossible to define the class model in the conventional sense, since the interpretations of and depend on the specific choice of . The best one can do is to define as a Boolean-valued model. Or does "forcing over " mean "I'm actually forcing over a model, but I'll call this model , so everything I write is by default within this model"? Bbbbbbbbba (talk) 02:30, 23 April 2023 (UTC)
- I think "internal" is just the same as "syntactic" (you define a forcing relation inductively on formulas, then look at sentences that are forced by the empty condition). As for "Cohen's original method", I think it's a bit confusing to bring that up at this point in the text, because Cohen originally used something called "ramified forcing", which I've never learned in detail, but I gather involved somehow recapitulating the hierarchy while taking forcing into account. That difference doesn't seem to be the one the text in question is talking about, which to me means the text in question could be misleading. --Trovatore (talk) 20:06, 23 April 2023 (UTC)
- My understanding of ramified forcing is: Forcing involves a lot of transfinite recursion, and whereas unramified forcing uses to rigorize transfinite recursion, ramified forcing uses . Apparently, when proving the expanded model is a model of ZFC, these two methods encounter difficulties on different axioms. I haven't looked into the detailed proofs myself, but if my references are to be trusted, then A Cheerful Introduction to Forcing and the Continuum Hypothesis says that Foundation and Choice are the really difficult ones for unramified forcing, while Cohen (1966) says that Power Set and Replacement are the non-trivial ones for ramified forcing. This does make some sense since Power Set and Replacement already causes troubles when proving the constructible universe itself is an inner model. Bbbbbbbbba (talk) 02:25, 24 April 2023 (UTC)