Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I am looking at the following passage in Halbeisen's book "Combinatorial Set Theory" (p 260 at the bottom):

enter image description here

What is the role of $\Phi$? It seems to me that a finite fragment is the same as a finite subset of axioms. Then the sentence saying that for a finite subset $\Phi \subset ZFC$ there is a finite subset $ZFC^\ast \subset ZFC$ seems to contain redundancy. What am I missing? Or is this a "writo"? Many thanks for your help.

share|improve this question
My immediate reaction, without thinking about it too hard, is that $\mathsf{ZFC}^*$ might have to be a proper superset of $\Phi$ in order to ensure that any set model $\mathbf{M}$ of $\mathsf{ZFC}^*$ can be extended as desired. –  Brian M. Scott Dec 25 '12 at 10:30
It looks to me as if $\varphi$ is the formula outside ZFC which you're aiming to prove consistent with ZFC using forcing. Or were you asking about $\Phi$? –  Henning Makholm Dec 25 '12 at 10:40
Are you wondering about $\varphi$ (\varphi) or $\Phi$ (\Phi)? –  Arthur Fischer Dec 25 '12 at 11:04
Dear Henning and Arthur: I am wondering about $\Phi$ in my question. –  Rudy the Reindeer Dec 25 '12 at 11:06

2 Answers 2

up vote 6 down vote accepted

(This is basically exactly what Brian mentioned in his comment, but in way more than 600 characters.)

Note that if $\mathsf{ZFC}$ refutes the sentence $\varphi$, then there must be a finite fragment $\Phi$ of $\mathsf{ZFC}$ which refutes $\varphi$. So what we are aiming for is to show that (relative to the consistency of $\mathsf{ZFC}$) this cannot happen.

So we begin with a finite fragment $\Phi$ of $\mathsf{ZFC}$, and we have in mind a forcing notion that should produce generic extensions satisfying $\Phi + \varphi$. Unfortunately, even demonstrating that the desired forcing notion $\mathbb{P}$ is an element of an arbitrary set model $\mathsf{M}$ of $\Phi$ might require axioms not in $\Phi$. Furthermore, the demonstration that the generic extension satisfies $\Phi + \varphi$ might also require axioms of $\mathsf{ZFC}$ not in $\Phi$ (because we will have to construct the required names, which will in all likelihood require, for example, instances of Replacement not in $\Phi$).

We must then analyse exactly what we need so that the above process can be carried out, and get a suitable finite fragment $\mathsf{ZFC}^*$ of $\mathsf{ZFC}$ such that if you begin with a set model $M$ of $\mathsf{ZFC}^*$ the forcing notion $\mathbb{P}$ is an element of $\mathsf{M}$, and, moreover, constructing a generic extension $\mathsf{M}[X]$ results in a model of $\Phi + \varphi$. This then shows (relative to the consistency of $\mathsf{ZFC}$) that the finite fragment $\Phi$ cannot refute $\varphi$.

This analysis can be carried out for any finite fragment $\Phi$ of $\mathsf{ZFC}$, leading to an appropriate finite fragment $\mathsf{ZFC}^*$ so that the above works. In this manner we can demonstrate the relative consistency of $\varphi$ with $\mathsf{ZFC}$.

Note that there are many relative consistency results that begin not with finite fragments of $\mathsf{ZFC}$, but rather of stronger theories, such as $\mathsf{ZFC} + \exists \text{ inaccessibles}$. The above description, mutatis mutandis, will handle those cases as well.

(But in practice we don't tend to worry about the particulars, and think of forcing over models of $\mathsf{ZF(C)}$ -- or stronger theories. Even more, (and perhaps far more often than the formalist in me would like to admit) we generally think of forcing over the entire von Neumann universe $\mathsf{V}$.)

share|improve this answer
Thank you so much for this clear answer. I have one question about it: How can we be sure that the additional axioms we need to prove $\mathbb P$ is in $\mathsf M$ are only finitely many? (The other case you mention seems clear: If $\Phi$ is finite then so is any model $\mathsf M$ of $\Phi$ and then there will also only be finitely many names so that proving $\mathsf M$ satisfies $\Phi$ can be done using finitely many names $\mathbb P^{\mathsf M}$ where $\mathbb P \subseteq \mathsf M$ for which we need finitely many instances of Replacement.) –  Rudy the Reindeer Apr 29 '13 at 19:00
@MattN. Well, if $\sf{ZFC}$ proves that a forcing notion can be constructed, then there are only finitely many axioms used in the proof. (Note that a finite theories can have infinite models; heck, some finite theories have only infinite models, such as the theory of dense linear orders without endpoints. The point is that (formal) proofs are finite objects, and so only finitely many axioms are ever employed in any given proof.) –  Arthur Fischer Apr 29 '13 at 19:16
Ahh, thank you. I somehow thought of axioms as assumptions. I know that the definition of formal proof means it's a finite sequence of steps. But "steps" here really also includes the assumptions. : ) –  Rudy the Reindeer Apr 29 '13 at 20:43

Reading pages 260 and 261, I believe that Halbeisen's idea is to workaround the limitation of having definable models (sets) for only finite part of ZFC.

The role of $\Phi$ is to allow us (by using the Compactness theorem) to move from a finite sub-theory $T$ of ZFC, to the whole theory. (When using forcing you analyze "metamathematics" within mathematics. You assume some countable model $M$ for a specific finite list of axiom (the exact list of axioms is built during your forcing construction) and you show how $M$ can be "extended" to provide the desired new "model" (a new set). )

The only problem I have with Halbeisen's approach is that the Compactness theorem 3.7 was proved for meta-mathematical objects (real formulas etc.) not with their mathematical counterparts (Gödel encoding of formulas, proofs etc.), and there needs to be at least a note saying that the same proof can be used with the encoded objects.

share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.