Godel and forcing

Question

Are there any forcing based proofs of Godel's first and second incompleteness theorems?

Answer 1

On the one hand, the method of forcing has been one of the principal tools for showing independence results in set theory, and I suppose that any independence result can be viewed as an instance of the first incompeteness theorem. We know ZFC is incomplete, if consistent, because we can build forcing extensions satisfying $\text{ZFC}+\text{CH}$ and others with $\text{ZFC}+\neg\text{CH}$, and so CH is not settled by ZFC. And the same holds in hundreds or even thousands of other similar situations, where we show that a statement is independent of a particular set theory by forcing both it and its negation. In this sense, forcing has provided us with many instances of the first incompleteness theorem.

But on the other hand, we cannot seem to use forcing over a model of set theory to prove that an arithmetic theory is incomplete. The reason is that set-theoretic forcing simply does not affect arithmetic truth, since every statement of arithmetic is absolute between the ground model and the forcing extension. Indeed, even $\Sigma^1_2$ truth (and more, depending on one's large cardinals) is absolute.

Meanwhile, there are various uses of forcing with models of arithmetic, to show independence over very weak theories. Nevertheless, Ali Enayat's answer to a question of Timothy Chow explains a severe limitation of the method for showing independence results. I think probably that question and answer may be the topic in which you are actually interested.

Finally, one can view many priority arguments in computability theory as proceeding from a forcing perspective. That is, the constructions are often elaborate procedures that amount to builing a filter that meets certain dense sets (called requirements). And there are many proofs of the first incompleteness theorem that proceed from computability considerations. For example, there cannot be a true c.e. complete theory, since then we could solve the halting problem by searching for proofs either that the given program does halt or that it does not halt.