# Foundations of Forcing in Kunen

In Kunen's Set Theory book, forcing is described as a finitistic procedure to get some relative consistency result $$Con(ZFC)\Rightarrow Con(T)$$, where $$T$$ is an extension of $$ZFC$$. Because we can't prove (from $$ZFC$$) the existence of a countable transitive set model of $$ZFC$$, Kunen describes the relative consistency proof using a countable set model $$M$$ of a finite fragment of $$ZFC$$ with enough strength to carry out the particular argument. Treating this $$M$$ as the ground model, we can use forcing to attain some $$N\supset M$$ that models $$T$$. From here, if we could derive a contradiction $$T\vdash\phi\wedge\neg\phi$$, then $$ZFC$$ would derive this contradiction relativized to $$N$$, i.e. $$ZFC\vdash\phi^N\wedge\neg\phi^N$$. Since we assume $$Con(ZFC)$$ in our relative consistency argument, this is a contradiction, so it cannot be the case that $$T$$ can prove any contradiction and we can conclude $$Con(T)$$. Kunen remarks that this proof is finitistic as we don't use any infinitistic methods in the metatheory to produce this argument.

I follow the argument, but I was unclear whether it is necessary that the ground model only models a finite fragment of $$ZFC$$. I know that the incompleteness theorems show that $$ZFC$$ can't prove the existence of a set model of the entirety of $$ZFC$$, but can't we assume the existence of one as a consequence of our $$Con(ZFC)$$ assumption in the relative consistency argument? Earlier in Kunen's book, he mentions that we can use Gödel numbering to define the satisfaction relation with set models and formally prove the completeness theorem as a theorem of $$ZFC$$. If we assume $$Con(ZFC)$$ in our proof, it seems like we can use this formal version of the completeness theorem to get the existence of a set model of all of $$ZFC$$, which we can then treat as the ground model for the forcing argument. I know that deciphering the Gödel numbering requires a metatheorem, but the statements $$Con(ZFC)$$ and $$Con(T)$$ are already expressed using Gödel numbering in Kunen's original argument, so invoking the Gödel numbered completeness theorem wouldn't seem to make this argument any less formal or finitistic. Am I misunderstanding something, or is my suggestion just another valid approach to the foundations of forcing?

Another example of this same question comes up when using class models to prove relative consistency results. Kunen provides a similar finitistic argument that the class $$L$$ can be used to prove $$Con(ZF)\Rightarrow Con(ZFC)$$, without appealing to the assumed existence of set models of $$ZF$$ or $$ZFC$$. In this case could we use the formalized completeness theorem to get a set model $$M$$ of $$ZF$$ from the assumption $$Con(ZF)$$, then use the defining formula for the class $$L$$ and separation to get a set model for $$ZFC$$ as a subset of $$M$$?

• In the case of $L$, yes the formalized completeness theorem approach works. In the case of forcing, Kunen's assumption that the model is transitive makes things more complicated and this is why the finite fragment argument is used... see here. Commented Jul 9, 2023 at 19:37
• I don't understand your point about how this wouldn't be less finitistic though... invoking the completeness theorem at the meta-level is pretty glaringly not finitistic. (Also on the above... though I go into it in the linked answer, worth noting here that it's perfectly possible to carry out the forcing proof using the completeness theorem. And even if we use transitive models and opt to look at finite fragments, if we really don't want to do things finitarily, we can just use the compactness theorem.) Commented Jul 9, 2023 at 19:53
• Well it's infinitary by nature just like the completeness theorem, in the sense that there's no way to really formalize it in PA or PRA (at least not in its full glory) since models are kind of inherently set-theoretic. But like the completeness theorem, it can be formalized in ZFC. So, for a ZFC proof of Con(ZFC) -> Con(T) you can show in ZFC that (assuming Con(ZFC)) every finite subtheory of $T$ has a model and invoke compactness. This takes a little thought to work out though, and isn't any less complicated or more elucidating than Kunen's finitary approach, IMO. Commented Jul 9, 2023 at 20:34
• ZFC doesn't prove "there are set models for each finite fragment of ZFC". Rather, ZFC proves "there are set models (of the fragment)" for each finite fragment of ZFC. The universal quantifier over finite fragments is in the metatheory. (And as for reflection, it's a theorem schema, not a single theorem, accordingly.) Commented Jul 9, 2023 at 22:20
• BTW, we can certainly talk about finiteness in ZFC... e.g. we can define natural numbers (say, as ordinals with no limit ordinal beneath), and say a set is finite if there's a bijection between it and a natural number. But there are subtleties with that notion capturing finiteness in models (e.g. not every set a model thinks is finite is necessarily actually externally finite), and thinking about this apparent paradox you highlighted in terms of models shows this must be the case for 'finite fragments of ZFC' according to models that think ZFC is inconsistent. Commented Jul 9, 2023 at 22:40

Cohen, in his initial publications, used Axiom SM, "There exists a standard model of ZF". (Standard models are all well-founded, of course.) It is known that Con(ZF) does not imply SM. The reason basically is that the minimal model doesn't satisfy SM, but if Con(ZF) is true, then it satisfies Con(ZF). That's because Con(ZF) is a $$\Pi_1$$ sentence.
Incidentally, Cohen eventually did look at non-well-founded models, in a paper on the independence of AC ("Automorphisms of Set Theory", Proceedings of the Tarski Symposium, 1971, pp.325-330). As he remarks in his book, there can be no true automorphism of a standard transitive model of ZF. Forcing proofs thus work with automorphisms of the notion of forcing. But Cohen constructed a true automorphism of a non-well-founded model of ZF and used that to prove the relative consistency of Con(ZF+$$\neg$$AC).