Is it possible to prove $Con(ZFC) \rightarrow Con(ZFC + \neg CH)$ purely within ZFC? To prove this (using forcing) one seems to need a countable transitive model of ZFC. The texts I am reading avoid this by proving Con(T + CH) for all (suitable) finite fragments T of ZFC using the Reflection principle to prove the existence of a countable transitive model of T. But doesn't the Reflection principle operate outside of ZFC? From what I understand it just shows how, given a list of axioms of ZFC, one can write down a proof that constructs a model of these axioms. Am I confused here or is there an other way to achieve this?

1$\begingroup$ Also this seems related to your question: mathoverflow.net/questions/57225/… $\endgroup$ – Stefan Hoffelner Feb 10 '12 at 20:36
The reflection principle is a theorem scheme; each of its instances is provable in ZFC.
The following proof works entirely in ZFC:
Assume Con(ZFC) together with notCon(ZFC+nonCH) and aim for a contradiction.
By assumption plus completeness theorem, there is a model (M,E) of ZFC. M may be nonstandard in the sense that its ordinals (even its natural numbers) are not wellfounded.
By compactness, there is some finite sub theory ZFC* of ZFC such that ZFC*+nonCH is inconsistent.
Find a (slightly larger) finite sub theory ZFC** of ZFC such that ZFC** proves all theorems you need about forcing, including that ZFC* plus nonCH holds in the extension.
(M,E) satisfies reflection for ZFC** , so there is some x in M which M thinks is a ctm (countable transitive model) of ZFC** . So M can find a Cohen extension y of x which satisfies ZFC* plus nonCH.
By the easy direction of the completeness theorem, M therefore thinks that ZFC*+nonCH is consistent.
But then this theory is really consistent. (Because any proof of an inconsistency would be coded by a natural number, which is represented in M.)
Btw, I think the sketch I just gave is not ideal since it seems to rely on the existence of infinite sets. The implication from Con(ZFC) to Con(ZFC+nonCH) can really be shown in ZF minus infinity, or even in a weak version of Peano arithmetic.

$\begingroup$ Thanks! This answers my question! I guess the main point is that one can apply the Reflection principle inside of M (in some sense). $\endgroup$ – Tobias Neukom Feb 10 '12 at 22:57
The use of the Booleanvalued model approach to forcing allows one to avoid any consideration of countable transitive models in the proof that Con(ZFC) implies Con(ZFC+$\neg$CH), and gives in my opinion a more satisfying account of the result by dealing directly with models of full ZFC, rather than working with models only of some fragment of set theory. The point is that we have a very general procedure enabling us, starting from any model of ZFC, to produce a closely related model of ZFC+$\neg$CH.
Specifically, suppose that $M$ is any model of ZFC. By the standard development of Booleanvalued models, as for example explained in Timothy Chow's A beginner's guide to forcing, or my notes on An introduction to the Boolean ultrapower, one may inside $M$ define the $\mathbb{B}$valued model $M^{\mathbb{B}}$, where $\mathbb{B}$ is the Boolean algebra in $M$ of the forcing $\text{Add}(\omega,\omega_2)^M$. These developments of forcing show that every axiom of ZFC gets Boolean value $1$ in $M^{\mathbb{B}}$, and further that $\\neg\text{CH}\=1$. Let $U$ be any ultrafilter on $\mathbb{B}$ in $M$, and form the quotient $M^{\mathbb{B}}/U$. The Los theorem for Boolean ultrapowers shows that this is a firstorder structure satisfying every statement whose Boolean value is in $U$. In particular, $M^{\mathbb{B}}/U$ satisfies ZFC+$\neg$CH.
So we've shown that if there is a model of ZFC, then there is a model of ZFC+$\neg$CH, and this establishes the relative consistency result, as desired.
The key to the success of the method is to develop the method of forcing internally in ZFC via the $\mathbb{B}$valued universe and its quotient. Thus, the construction of the model $M^{\mathbb{B}}$ and the quotient $M^{\mathbb{B}}/U$ is undertaken entirely inside the model $M$, as an internal ZFC construction. By this means, forcing becomes sensible over any model of ZFC.
A careful consideration of the method shows that in fact the relative consistency result Con(ZFC)$\to$Con(ZFC+$\neg$CH) can be made in PA. One need only verify that PA can prove that ZFC proves the required development. But I prefer to leave this to the expertise of the proof theorists.

2$\begingroup$ I wonder if these relative consistency results can be proved in $I\Sigma_1^0$ or PRA. The latter is presumed to be accepted by most finitists. $\endgroup$ – Ruizhi Yang Jun 23 '16 at 3:41


1$\begingroup$ If you just chow syntactically that “$\mathrm{ZFC+\neg CH}\vdash\phi\implies\mathrm{ZFC}\vdash\\phi\=1$”, this argument can be formalized in weak fragments of arithmetic such as the theory $PV_1$ of polynomialtime functions. $\endgroup$ – Emil Jeřábek Sep 8 '19 at 7:34

$\begingroup$ @EmilJeřábek I have so little experience with theories with limited coding techniques that I didn't dare to claim anything lower than ISigma_1. (But, at least for arithmetized completeness you need ISigma_1 to build the branch). You, people in Czechoslovakia, are masters of weak arithmetic proofs, so I'll trust you here. $\endgroup$ – andrey bovykin Sep 9 '19 at 12:34
You have almost answered your own question; it seems that the only part you are confused about is whether "the reflection principle operates outside ZFC."
One must, as always, distinguish between the formal system whose properties we are analyzing (in this case, ZFC), and the theory inside which we are making our arguments about said formal system. The latter is what we call the "metatheory." When you ask if Con(ZFC)→Con(ZFC+¬CH) can be proved purely within ZFC, this can only mean: "Can the metatheoretic argument itself be formalized in ZFC?" Note here that ZFC is playing two roles; it is the theory being studied, and also the (meta)theory being used to prove things about ZFC. It's important to not to confuse these two roles.
Now, the reflection principle takes place "outside ZFC" only in the sense that it is being used in the metatheoretic proof of Con(ZFC)→Con(ZFC+¬CH). But this doesn't mean that the metatheoretical argument can't itself be formalized in ZFC; in fact, it can, and in fact it can be formalized in much weaker systems (I think primitive recursive arithmetic suffices).
For more explanation about how to prove Con(ZFC)→Con(ZFC+¬CH) finitistically, I'd recommend Chapter VII, §9 of Kunen's book Set Theory: An Introduction to Independence Proofs. Here is one relevant paragraph:
We show that, given any finite list, $\phi_1, \ldots, \phi_n$, of axioms of, say, ZFC+¬CH, we can prove in ZFC that there is a countable transitive model for $\phi_1, \ldots, \phi_n$. The procedure involves finding (in the metatheory) another finite list $\psi_1, \ldots, \psi_m$ of axioms of ZFC, and proving in ZFC that given a countable transitive model $M$ for $\psi_1, \ldots, \psi_m$, there is a generic extension, $M[G]$, satisfying $\phi_1, \ldots, \phi_n$. The inelegant part of this argument is that the procedure for finding $\psi_1, \ldots, \psi_m$, although straightforward, completely effective, and finitistically valid, is also very tedious. We must list in $\psi_1, \ldots, \psi_m$ not only the axioms of ZFC "obviously" used in checking that $\phi_1, \ldots, \phi_n$ hold in $M[G]$ (e.g., if $\phi_1$ is the Power Set Axiom, then $\phi_1$ should be listed among $\psi_1, \ldots, \psi_m$), but also all the axioms needed to verify that various concepts are absolute for $M$ ("finite", "p.o.", etc.), as well as the axioms needed to show that certain mathematical results, such as the Δsystem lemma, hold in $M$.

$\begingroup$ Thanks for your answer! That's what Stefan Hoffelner is doing in his reply, isn't it? He is taking the metatheoretic argument and executing it inside a model M of ZFC? $\endgroup$ – Tobias Neukom Feb 10 '12 at 23:01

$\begingroup$ Well, I would phrase it as, he's taking the metatheoretic argument and showing how it can be carried out on the basis of ZFC. No model M of ZFC enters the picture. $\endgroup$ – Timothy Chow Feb 10 '12 at 23:11

$\begingroup$ I don't quite get that, what about the Model (M,E) of ZFC in step one? $\endgroup$ – Tobias Neukom Feb 10 '12 at 23:14

$\begingroup$ Oh sorry I meant the answer by Goldstern not Stefan Hoffelner $\endgroup$ – Tobias Neukom Feb 10 '12 at 23:25

$\begingroup$ Goldstern is also showing that the metatheoretic argument can be carried out on the basis of ZFC. Arguments are not "executed inside models." They proceed from axioms according to rules of inference, and are therefore syntactic and not semantic. $\endgroup$ – Timothy Chow Feb 11 '12 at 2:08
The other answers are perfectly correct, but I'd like to add that the implication Con(ZFC) $\to $Con(ZFC + $\neg$CH) is not only provable in ZFC, it is provable in Peano arithmetic. I consider this a better and more natural version of the result  better since PA is much weaker than ZFC, so this version is more informative, and more natural because consistency is a number theoretic concept (no number $n$ is the Gödel number of a proof of 0=1).
The reflection principle indeed operates outside of ZFC  it is a "theorem scheme" consisting of one theorem of ZFC for each sentence of set theory. However, the pattern of the proofs is quite simple, so that we can prove in PA a single theorem to the effect that each instance of reflection is a theorem of ZFC.
A nice elementary way to treat forcing from the point of view of PA is to introduce a new system ZFC${}^+$ whose language is the language of ZFC augmented by a constant symbol $M$ and whose axioms consist of
$\bullet$ the axioms of ZFC
$\bullet$ the single assertion that $M$ is countable and transitive
$\bullet$ the relativization of each axiom of ZFC to $M$.
We then use reflection to prove, in PA, that if ZFC is consistent and we can construct in ZFC${}^+$ a set $N = M[G]$ in which both the axioms of ZFC and (say) $\neg$CH hold, then ZFC + $\neg$CH is consistent. I believe this technique is due to Shoenfield.
(Shameless selfpromotion: this is the approach I use in my forthcoming book on forcing.)

$\begingroup$ (Just poking the usual fun with this usual caveat, if $\sf PA$ is inconsistent then every number encodes a proof that $0=1$ :)) $\endgroup$ – Asaf Karagila Feb 23 '14 at 23:42

$\begingroup$ (By the way, the idea of augmenting the language by a constant and axioms which state that it satisfies the axioms of $\sf ZFC$ is due to Feferman, if I am not mistaken. It might have been Shoenfield who used this for forcing, though.) $\endgroup$ – Asaf Karagila Feb 23 '14 at 23:44

$\begingroup$ @Asaf, can you give me a reference for the Feferman comment? $\endgroup$ – Nik Weaver Feb 24 '14 at 2:42

$\begingroup$ See the footnote on the first page of Feferman, "Foundations of unlimited category theory: what remains to be done" (math.stanford.edu/~feferman/papers/FCTRSL2013.pdf), there Feferman points out that this suggestion appears in a text from 1969 which I couldn't find as open access (and my paywall didn't get through the Springer website). $\endgroup$ – Asaf Karagila Feb 24 '14 at 10:26

1$\begingroup$ I wonder if the consistency results produced by forcing can be proved in even weaker systems, e.g. $I\Sigma^0_1$? $\endgroup$ – Ruizhi Yang Jun 22 '16 at 15:53
The usual strategy to prove that the negation of $CH$ is consistent with $ZFC$ is the following: One shows (under the assumption $Con(ZFC)$ that for any finite fragment $T$ of $ZFC$ we have that $T+ \lnot CH$ has a model. Here 'for any finite fragment' means that for each instance of such a finite $T$ one gets in a uniform way such a model. This is actually a scheme of theorems, one for each $T$. But this is still enough to obtain a proof for $Con (ZFC) \rightarrow Con(ZFC+ \lnot CH)$ inside $ZFC$:
I will try it indirectly. Thus assume, to get a contradiction, that ''$ZFC \vdash CH$'' (this is an arithmetical statement using Gödel numbers, and should say in plain english: 'There exists a proof of $CH$ from $ZFC$'), then by Gödel we have: ''There exists a finite fragment $T$ of $ZFC$ such that $T \vdash CH$''(again this should read: 'There exists a proof...). We take this $T$ and apply our theorem scheme for $T$, i.e we actually prove in our uniform way that for our explicit theory $T+ \lnot CH$ has a model, which again by Gödel means that $T \nvdash CH$ which is a contradiction.
This whole argument has taken place completely inside $ZFC$.

$\begingroup$ Your answer appeared while I was writing mine. I don't get the point of your theory T'. If there is a finite extension T' of T such that T' plus nonCH has a model, then T':=T will do as well. $\endgroup$ – Goldstern Feb 10 '12 at 22:16

$\begingroup$ Yes you are right. I falsely thought it would be necessary for any reason $\endgroup$ – Stefan Hoffelner Feb 10 '12 at 22:26
I guess you can do it even lower: in ISigma_1 (with lots of coding), or its comfortable secondorder version WKL_0 (which will take care of any compactness).
I don't see why much stronger compactness (Peano Arithmetic or its secondorder version ACA_0) would be necessary.

1$\begingroup$ This is an overkill. You can get away with much weaker theories, such as $PV_1$. $\endgroup$ – Emil Jeřábek Sep 8 '19 at 7:34