Some difficulties when trying to formalize forcing

Question

I'm new to forcing and im impressed by the results we can achive using it. there is some importent point that i fail to understand. Assuming the (unformal notion of) consistency of (the unformaliled) theory: $ZFC$ , i am (almost) convinced (after some reading of kunens book) that one will never succeed to prove $CH$ (the "almost" is because there is a small part that I didnt read + I need to rehearse). I want to formalize the independence results and I'm having difficulties. for exemple, I want to know how to formalize the fact that we cant prove $CH$. I found this post: https://mathoverflow.net/questions/88134/formal-proof-of-conzfc-conzfc-not-ch-in-zfc but I did not understand Goldstern (highly voted) answer including what his exact statements are. Here is what I got + some (probably bad) attempts to understand what the exact statements are.

but first of all here is some conventions: If $φ$ is some (meta)formula (i.e $∀x(x=x)$) then $'φ'$ will be the corresponding formalized object (i.e some set which is a finite function s.t ...) the set $'ZFC'$ is defined similarly. Now, $($$¬$$($$'ZFC'$ $⊢$ $'CH'$$)$$)$ is just a regular statement (which is a meta-formula) like (for example) Radon–Nikodym. I want to prove $($$¬$$($$'ZFC'$ $⊢$ $'CH'$$)$$)$ (proving this regular statement is the formalization im talking about)

I understand 1-4. the only way I found 6,5 to make sense is by assuming that $'ZFC'$ $⊢$ $($$'$$($$'ZFC'$ $⊢$ $'CH'$$)$$'$$)$, (call this assumption $@$) and now we may define: $J$ $:=$ {$x$$∣$ $x$ is a finite subset of $'ZFC'$} and we can explicitly define a well ordering of $J$ (fix one). now define $ZFC*$ $:=$ min{$x∈J$$∣$ $x⊢$ $'CH'$} and define $ZFC**$ as needed (Im 99% sure that i know how). now from $@$ the defenition of $ZFC*,ZFC**$ makes sense in every model of $'ZFC'$. now take some $M$ s.t $M$ $⊨$ $'ZFC'$ , from levy reflection principle there exists $x$ in $M$ s.t $M$ $⊨$ $'($$x$ is transitive and countable and $x ⊨ ZFC**$$)'$ (i am not convinced that this true ). we proved that $∀R$ if $R$ is countable transitive and $R$ $⊨$ $ZFC**$ then $∃Y$ s.t $Y$ $⊨$ $ZFC*$ $+$ $'¬CH'$ (i am not sure that this is accurate). let $φ$ denote this regular statement. now it is obvious that $'ZFC'$ $⊢$ $'φ'$. but now $M$ $⊨$ $'φ'$. but we now easily see that $M$ $⊨$ $'$($∃Y$ s.t $Y$ $⊨$ $ZFC*$ + $'¬CH'$)$'$ but then $M$ $⊨$ $'$$¬$$($$ZFC*$$⊢$$'CH'$$)$$'$, and this is a contradiction to $@$.

as you can see, Im not sure if the above statements are correct and if they are correct, i dont know how to prove them. for any help / correction of my mistakes / discussion, i would be grateful. Thanks (again), and sorry for the long question.

Answer 1

If you give me a finite list $S$ of some of the axioms of ZFC I can prove from ZFC that exists a c.t.m. (countable transitive model) $M$ such that $M\vDash \land S$ by using the Lowenheim-Skolem method and the Mostowski transitive collapse.

Suppose that you give me a proof that $\land S\implies CH$ where $S$ is the finite list of all of the axioms of ZFC that are used to prove $CH$. Then any c.t.m. $M$ for $\land S$ will satisfy $M\vDash CH.$

But I can take a finite list $T$ of some of the axioms of ZFC and take a c.t.m. $M$ with $M\vDash ((\land S \land (\land T)),$ and use Forcing to obtain a c.t.m. $M[G]$ with $M[G]\vDash ((\land S)\land \neg CH).$ This is a contradiction. So if there is such an $S$ then ZFC$\vdash (1=0).$

The list $T$ will include the axioms needed to define a certain Poset in $M$ and to derive some of its properties, and to prove the existence and some properties of $G,$ and to demonstrate that $M[G]\vDash \land S,$ and that $M[G]\vDash \neg CH.$ (You could say that $T$ is reverse-engineered from $S$ and $\neg CH$.)

In the meta-theory, we have Con(ZFC)$\implies$ (ZFC$\;\not \vdash CH$).

This also applies with $CH$ and $\neg CH$ interchanged, so Con(ZFC)$\implies $(ZFC$\;\not \vdash \neg CH).$

As Kunen writes, Forcing gives us a finitistic method of obtaining a contradiction in ZFC from any (explicitly demonstrated) proof, from any finite S, of $CH$ (or of $\neg CH$).

Answer 2

The proof of the independence of CH or other statements using forcing can be done in an arithmetical theory like PA or something way weaker. Of course any arithmetical statement (like Con(ZFC) $\rightarrow$ Con(ZFC + $\neg$ CH)) that PA proves can also be proved in ZFC.

In this answer I am using PA rather than ZFC (which would equally work) as a metatheory to avoid confusion between the 'metatheory ZFC' and the 'ZFC' of which we are proving independence.

So let's try to go through it step by step:

• We are trying prove from PA that Con(ZFC) $\rightarrow$ Con(ZFC + $\neg$ CH). So let's work in PA. Assume ZFC $\vdash$ CH. This does not mean we are assuming PA $\vdash$ $[$ZFC $\vdash$ CH$]$! (this corresponds to your assumption @) This assumption (that ZFC $\vdash$ CH) is just a shortcut for placing a '$($ZFC $\vdash$ CH$) \rightarrow$' before every statement we are making.

• The statement 'ZFC $\vdash$ CH' just means that there is a proof of CH from ZFC, i.e. there is some natural number $n$ that encodes a proof of CH (which also is coded by some number ...) from the axioms of ZFC (and 'being an axiom of ZFC' is definable). But this actually means (just by the definition of proof) that there is a number $m$ that codes a finite set of axioms of ZFC that prove CH.

• We know by the reflection principle (which is provable in PA), that for any such finite set of axioms $T$, ZFC $\vdash$ $[\exists M \models T$ and $M$ is a ctm $]$ (you can formally define T inside ZFC)

• But we also know that we can extend $T$ to a theory $T'$ which still only consists of axioms of ZFC so that ZFC $\vdash$ $[\exists M \models T'$ and $\exists M' \supseteq M (M' \models T + \neg$CH$)]$. In particular we know ZFC $\vdash$ $\exists M (M \models T + \neg$CH$)]$

• On the other hand we have a proof of CH from $T$. This proof can also (in the same way as T) be formalized in ZFC. So actually ZFC $\vdash$ [T $\vdash$ CH]. But then ZFC $\vdash$ $\exists M (M \models $CH$ + \neg$CH$)]$, which means ZFC $\vdash$ $\exists M (M \models $CH$ + \neg M \models $CH$)]$, which is a formal contradiction in ZFC.

• Thus $\neg$ Con(ZFC).

So we got that PA $\vdash$ $($ZFC $\vdash$ CH$) \rightarrow (\neg$ Con(ZFC)$)$, which of course is equivalent to PA $\vdash$ Con(ZFC) $\rightarrow$ Con(ZFC + $\neg$ CH).