Shoenfield's approach to the metamathematics of forcing

174 Views Asked by At

Cohen's approach to the metamathematics of forcing (see Kunen IV.5.1, new edition) involves talking about unspecified finite subsets $\Omega, \Lambda \subset \text{ZFC}$. Apparently, this is not very "elegant". For this reason Kunen introduces Shoenfield's approach. It goes as follows:

Shoenfield's approach to the metamathematics of forcing as in Kunen IV.5.1, new edition

The meta-theoretical Theorem IV.5.1 is:

If $\text{ZFC} + \mathfrak{c} = \aleph_7 \vdash \Xi$, where $\Xi$ is an arithmetical statement, then $\text{ZFC} \vdash \Xi$.

I have several questions:

1) What is the use of introducing the symbol $F$? Can't we just add to $\Sigma$ the sentence "$C$ is countable"?

2) What is meant by "explicitly" (as underlined in red above)? How is this relevant to the argument?

3) Why is talking about unspecified finite subsets $\Omega, \Lambda \subset \text{ZFC}$ considered not "elegant"?

1

There are 1 best solutions below

10
On

The idea of adding this extra symbol is due to Feferman. You're right that we do not need $F$, in general, to claim that we have a countable transitive model.

However the goal is to give an explicit definition of a model, a forcing, and a generic filter, which ultimately gives us an explicit definition of a model satisfying the resulting theory. For this reason we introduce $F$ as well, so it will let us do any recursive construction canonically. Of course, we can overcome this by noting that since $M$ satisfies $V=L$, there is a canonical ordering that we can use. But since we've added symbols anyway, might as well add $F$ to simplify these arguments by a lot.

The explicit part can be seen as somehow a recursive process in which we produce this model from $M$.

Finally, the lack of elegance is quite subjective, but the idea is that instead of doing this meta-theoretic induction on arbitrarily large fragments of $\sf ZFC$, we have one concrete proof of that. Whether or not you find it "better" is your choice, but this is natural to agree with Kunen once you've used forcing a few times and wrote a few forcing proofs. Eventually you even forego the countable model, and just force over the universe. But until you've had some practice, it's hard to explain exactly why.