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.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I think of forcing in the following context: Truth and Definability Lemmas. So forcing is a schema in the meta theory.

Now in his Set Theory book (the first edition), Kunen claims that setting up the following schema also deals with the mathematics required for showing $ZFC\vdash{\forall{\text{ctm } M \text{ of } {\ulcorner{ZFC}\urcorner}}} \implies \exists{N} (M\subseteq{N} \wedge N \text{ is a ctm of } \ulcorner{ZFC+\neg{CH}}\urcorner)$

Here in order to eliminate the use of relativization we can replace the occurrences of $(\text{Forces}_{\varphi}{(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})})^{M}$ by $M\models\ulcorner\text{Forces}_{\varphi}^{*}\urcorner{[(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})]}$ if we want. That I'm fine with. But I'm not sure how to we can replace the forcing schema with a single theorem inside of $ZFC$ (I would need to do this to verify $N\models{\ulcorner{ZFC}\urcorner}$).

The "follow my nose solution" is to say that after formalizing logic and model theory inside of set theory I can prove (as pointed out by justus87 I don't need to keep the corner notation anymore since I'm proving a result about sets inside of set theory.):

$ZFC\vdash\forall\varphi(x_{1},...,x_{n})\in{Fm_{L=\{\in\}}}$ with all free variables shown, $\exists\text{Forces}_{\varphi}^{*}(x_{1},...,x_{n},y_{1},...,y_{4})\in{Fm_{L=\{\in\}}}$ s.t. $\forall$ ctm $M\models{{ZF-P}}$, $\forall{\mathbb{(P,\leq,1)}}\in{M}$, $\varkappa_{1},...,\varkappa_{n}\in{M^{\mathbb{P}}}, \forall{G}$ that is $\mathbb{P}-$generic over $M$,

a) If $p\in{G}$ and $M\models\text{Forces}^{*}_{\varphi}{(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})}$ then $M[G]\models\varphi{({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})}$
b) If $M[G]\models\varphi{({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})}$, then there is $p\in{G}$ s.t. $M\models\mbox{Forces}^{*}_{\varphi}(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})$

This looks correct and should follow but I'm not a $100\%$ certain. Writing a schema inside the meta-theory as a theorem is somewhat tricky and I haven't quite mastered it (if we try to do this with the reflection theorems and do it improperly we end up obtaining that $ZFC$ is inconsistent).

Edit 1: I realized that I had the symbols for the codes down wrong. Now in this case the codes will be the codes for $L(M)$ and $L(M[G])$

Edit 2: I removed the use of codes after I formalized logic and model theory in ZFC. My initial idea was I would have the original codes for set theoretic formulas and when considering formulas of $L(M)=L\cup{\{c_{m}:m\in{M}\}}$ I could extend the codes in such a way so that the new codes($\ulcorner\urcorner_{1}$) had the property that if $\ulcorner\phi\urcorner_{1}$ used symbols only in $L$, then $\ulcorner\phi\urcorner_{1}=\ulcorner\phi\urcorner$. (It should work even without that, i.e. even if $L(M)$ has new codes that does not extend the old codes we can still insist that the new code $\ulcorner\phi\urcorner_{1}$ represents the formula that was originally represented by $\ulcorner\phi\urcorner$)

share|cite|improve this question
up vote 1 down vote accepted

If you formalize all the stuff in Kunen's presentation of forcing, you will get (in $ \mathsf{ZFC} $) a map $ \mathrm{Fm} \to \mathrm{Fm}, \ \phi \mapsto \mathrm{Forces}_\phi^* $.

So the main lemma says (as a theorem of $ \mathsf{ZFC} $):

Let $ n < \omega $. Let $ M $ be a c.t.m. for $ \ulcorner \mathrm{ZFC} \urcorner $ and let $ \phi \in \mathrm{Fm}_n $ a formula with exactly $ n $ free variables. Let $ \mathbb{P} := (P, \leq, \mathbb{1}) \in M $ be a preorder with largest element. Let $ \tau_0, \ldots, \tau_{n - 1} \in M^\mathbb{P} $ be names and $ G \subseteq P $ a $ \mathbb{P} $-generic filter over $ M $.

(a) If $ p \in G $ and $ M \models \mathrm{Forces}_\phi^* [\tau_0, \ldots, \tau_{n - 1}, P, \leq, p] $, then $ M[G] \models \phi[{\tau_0}_G, \ldots, {\tau_{n - 1}}_G] $.

(b) ... [similar] …

Note that $ \ulcorner \mathrm{ZFC} \urcorner := \{ x \in \mathrm{Fm} : \chi_\mathsf{ZFC}(x) \} $ relies on choosing a meaningful representing formula $ \chi_\mathsf{ZFC} $ in the meta-theory. (See IV §10 in Kunen's book (1980 edition)!)

For example, your statement does not make sense at these points:

  • "$ \exists \ulcorner \mathrm{Forces}_\varphi(x_1, \ldots, x_n, y_1, \ldots, y_4) \urcorner \in Fm_{L=\{\in\}} $" is not good because $ \mathrm{Fm} \to \mathrm{Fm}, \ \phi \mapsto \mathrm{Forces}_\phi^* $ is a mapping (within $ \mathsf{ZFC} $) now. So you must not use the Quine corners. These corners denote a formal representation of a meta-theoretical object - but that's what you want to avoid.

  • "$ M[G] \models \ulcorner \varphi({\varkappa_1}_G, \ldots, {\varkappa_n}_G) \urcorner $" should be "$ M[G] \models \ulcorner \varphi \urcorner [{\varkappa_1}_G, \ldots, {\varkappa_n}_G] $" or better (for the same reason as above) "$ M[G] \models \varphi [{\varkappa_1}_G, \ldots, {\varkappa_n}_G] $".

  • etc.

Also remark that this forcing for the formal representation of $ \mathsf{ZFC} $ yields $$ \mathsf{ZFC} \vdash \forall M \ ((M \text{ is a c.t.m. for } \ulcorner \mathrm{ZFC} \urcorner) \longrightarrow \exists N \supseteq M \ (N \text{ is a c.t.m. for } \ulcorner \mathrm{ZFC} \urcorner \ \land \ N \models \ulcorner \mathrm{CH} \urcorner)) $$ for example, but $$ \mathsf{ZFC} \nvdash \exists M \ (M \text{ is a c.t.m. for } \ulcorner \mathrm{ZFC} \urcorner), $$ so the logical interpretation is different.

share|cite|improve this answer
I'm not sure why you say that the first bullet doesn't make sense. It says that there is a particular formula in the language of set theory. For the second bullet point: I'm assuming that logic and model theory has been formalized inside of ZFC, so the code actually refers to a code in $L(M)$ (as you would do in Tarski definition of truth) with an underlying function to keep track of the fact that $\ulcorner\phi(\varkappa_{1},...\urcorner)$ is in fact $\phi$ with the correct things plugged in. (I wasn't really sure how to do this notationally so I might be wrong) – UserB1234 Apr 7 '14 at 15:49
Sorry, I don't get what you mean. What is $ L(M) $ for you? And what is that "underlying function" you are talking of? If you formalized first-order logic within $ \mathsf{ZFC} $, you do not need Quine corner notation anymore in the way you used it. – Justus87 Apr 8 '14 at 10:58
L(M) is the language $L\cup{\{c_{m}:m\in{M}\}}$ where the $c_{m}$ are constant symbols. This is the canonical language with which you can define truth inside of $M$ (you interpret $c_{m}$ as $m$)(This is how I was taught model theory). I see your comment about the corner notation. I kept using it because my question has both things (relativization and model theory) going on it at the same time which is why I still have the Quine notation. I'll change it back to match Kunen and I'll edit the question so as to reflect this. Thank you! – UserB1234 Apr 8 '14 at 11:42
Ah, I see. You're welcome! – Justus87 Apr 8 '14 at 21:24

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.