Formal proof of Con(ZFC) => Con(ZFC + not CH) in ZFC - MathOverflow

Formal proof of Con(ZFC) => Con(ZFC + not CH) in ZFC

2012-02-10T19:47:53Z

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?

Answer by Stefan Hoffelner for Formal proof of Con(ZFC) => Con(ZFC + not CH) in ZFC

2012-02-10T21:47:26Z

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

Answer by Goldstern for Formal proof of Con(ZFC) => Con(ZFC + not CH) in ZFC

2012-02-10T21:58:14Z

The reflection principle is a theorem scheme; each of its instances is provable in ZFC.

The following proof works entirely in ZFC: 1. Assume Con(ZFC) together with not-Con(ZFC+non-CH) 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 well-founded.
By compactness, there is some finite sub theory ZFC* of ZFC such that ZFC*+non-CH 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 non-CH 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 non-CH.
By the easy version of the completeness theorem, M therefore thinks that ZFC*+non-CH is consistent.
But then this theory is really consistent. (Becauses 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+non-CH) can really be shown in ZF minus infinity, or even in a weak version of Peano arithmetic.

Answer by Timothy Chow for Formal proof of Con(ZFC) => Con(ZFC + not CH) in ZFC

2012-02-10T22:44:58Z

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 "meta-theory." When you ask if Con(ZFC)→Con(ZFC+¬CH) can be proved purely within ZFC, this can only mean: "Can the meta-theoretic 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 meta-theoretic proof of Con(ZFC)→Con(ZFC+¬CH). But this doesn't mean that the meta-theoretical 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$.

Answer by Joel David Hamkins for Formal proof of Con(ZFC) => Con(ZFC + not CH) in ZFC

2012-02-11T00:38:28Z

The use of the Boolean-valued 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 Boolean-valued 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 first-order 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.