Independence from Set Theory Axioms I have often heard of various statements being independent from the axioms of set theory (typically ZFC). Some examples include


*

*The continuum hypothesis is probably the most famous

*The independence of the axiom of choice from plain ZF

*My professor told me that the following theorem is independent from the standard axioms: Theorem: If $U$ is a regular set then $U\times [0,1]$ is regular.


I'm wondering what a proof of such a statement would look like. What context do you do the proof in? What kind of theoretical framework do you have to build up before you can answer such questions?
In addition to answers I would also be interested in resources that would let me find out more about these ideas. I'm looking for books/web sites that start a relatively elementary level but still build up to dealing with some of the examples I mentioned above.
 A: It might help to understand look at how the fifth postulate is proved independent of Euclid's other axioms: One constructs a model, such as the Poincare disc, where the axioms can be given new interpretations. So the word LINE now means "arc perpindicular to the boundary of the disc", the word CONGRUENT now means "related by a Mobius transformation fixing the boundary of the disc" and so forth. One then checks that, if you take each axiom and replace the capitalized words by the quoted strings, the axiom remains true, except for the fifth postulate, which becomes false. 
Similarly, to show that AC is independent of ZF, one works inside ZFC and builds a model where the axioms of ZF, suitably reinterpreted, stay true but where choice is false. The technical tool used to build that model is called forcing. I don't really understand it, but Timothy Chow's introduction is the closest I have come to doing so.
A: I'm not qualified to answer your question, but the clearest introduction I've ever read to these ideas is Timothy Chow's A beginner's guide to forcing, which tries to explain the mathematical technique Paul Cohen used to prove the independence of CH from ZFC.
A: It's important to distinguish between the theory you're proving something about (say ZFC) and the metatheory you're working in. For a metatheory, people usually talk like they're using ZFC, but are only using a much weaker fragment of it.
The basic idea is that you start with a structure M with some binary relation E, so that E satisfies the ZFC axioms, just like, say, a group satisfying the group axioms. Then you modify this structure in some controlled way to get a new structure M' with a new relation E'. If you've done things right, (M', E') is a model of what you were trying to build. Typical M' is a subset or superset of M, and E and E' agree where appropriate.
If you want a book intended for nonlogicians, I would recommend An Introduction to Independence for Analysts by Dales and Woodin. It avoids more of the language of logic, and some assumptions which look strange to nonlogicians, such as standard models.
If you want a more standard presentation, Kunen's Set Theory An Introduction To Independence Proofs is a good place to start.
A: If you prefer slightly non-technical explanations, the best one I've seen is the book "Gödel, Escher, Bach" by Douglas Hofstadter. It explains Gödel's incompleteness theorems and what it means to be independent of a set of axioms.
In my humble opinion, it is one of the best books ever written, in any field, by anyone.
A: As for what "theoretical framework" is needed, you can think of the independence theorems as statements about finite sequences of formulas, so the "metatheory" doesn't need to assume the existence of any uncountable sets.
In more detail: first, assign different natural numbers to each formula (via Gödel coding), and then define a formal proof to be a finite sequence of such numbers where each one encodes a formula that follows logically from the previously-encoded formulas.  Consistency means that that the formula $x \neq x$ is not logically derivable in any finite number of steps.  This converts "ZFC is consistent" into a combinatorial statement about finite sequences of natural numbers.
With this reductive approach, you don't have to worry about assuming the existence of large infinite sets a priori.  In fact, I think that all the relative consistency results gotten using Cohen's forcing technique could, in principle, be formalized just in Peano arithmetic.
Kunen's Set Theory: An Introduction to Independence Proofs contains nice clear discussions of these foundational issues.
