Talk:Forcing (mathematics)

From Wikipedia, the free encyclopedia

WikiProject Mathematics
Mathematics Portal
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: B Class Mid Priority  Field: Foundations, logic, and set theory
Please update this rating as the article progresses, or if the rating is inaccurate. Please also add comments to suggest improvements to the article.

Contents

[edit] Formating Math

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)

[edit] What to Add/Remove

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--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)

[edit] Notation and Names

Aleph4: 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 \{ (\check{q}, (q,\infty)): q \in {\mathbb Q}\}, but apparently you want to really work in 10ω... -- 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, 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)
Have you tried changing the math settings in your preferences? Logicnazi 01:52, 30 August 2007 (UTC)

[edit] Needs Editing

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.

[edit] Move to Forcing_(Set Theory)

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)".

[edit] Proofs seem to gloss over a lot

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. --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)