Editing Forcing (mathematics) (section)

== Logical explanation ==

By [[Gödel's second incompleteness theorem]], one cannot prove the consistency of any sufficiently strong formal theory, such as <math> \mathsf{ZFC} </math>, using only the axioms of the theory itself, unless the theory is inconsistent. Consequently, mathematicians do not attempt to prove the consistency of <math> \mathsf{ZFC} </math> using only the axioms of <math> \mathsf{ZFC} </math>, or to prove that <math> \mathsf{ZFC} + H </math> is consistent for any hypothesis <math> H </math> using only <math> \mathsf{ZFC} + H </math>. For this reason, the aim of a consistency proof is to prove the consistency of <math> \mathsf{ZFC} + H </math> relative to the consistency of <math> \mathsf{ZFC} </math>. Such problems are known as problems of '''relative consistency''', one of which proves
{{NumBlk||<math display="block"> \mathsf{ZFC} \vdash \operatorname{Con}(\mathsf{ZFC}) \rightarrow \operatorname{Con}(\mathsf{ZFC} + H). </math>|{{EquationRef|⁎}}}}

The general schema of relative consistency proofs follows. As any proof is finite, it uses only a finite number of axioms:

: <math> \mathsf{ZFC} + \lnot \operatorname{Con}(\mathsf{ZFC} + H) \vdash (\exists T)(\operatorname{Fin}(T) \land T \subseteq \mathsf{ZFC} \land (T \vdash \lnot H)). </math>

For any given proof, <math> \mathsf{ZFC} </math> can verify the validity of this proof. This is provable by induction on the length of the proof.

: <math> \mathsf{ZFC} \vdash (\forall T)((T \vdash \lnot H) \rightarrow (\mathsf{ZFC} \vdash (T \vdash \lnot H))). </math>

Then resolve

: <math> \mathsf{ZFC} + \lnot \operatorname{Con}(\mathsf{ZFC} + H) \vdash (\exists T)(\operatorname{Fin}(T) \land T \subseteq \mathsf{ZFC} \land (\mathsf{ZFC} \vdash (T \vdash \lnot H))). </math>

By proving the following
{{NumBlk|| <math display="block"> \mathsf{ZFC} \vdash (\forall T)(\operatorname{Fin}(T) \land T \subseteq \mathsf{ZFC} \rightarrow (\mathsf{ZFC} \vdash \operatorname{Con}(T + H))), </math>|{{EquationRef|⁎⁎}}}}

it can be concluded that

: <math> \mathsf{ZFC} + \lnot \operatorname{Con}(\mathsf{ZFC} + H) \vdash (\exists T)(\operatorname{Fin}(T) \land T \subseteq \mathsf{ZFC} \land (\mathsf{ZFC} \vdash (T \vdash \lnot H)) \land (\mathsf{ZFC} \vdash \operatorname{Con}(T + H))), </math>

which is equivalent to

: <math> \mathsf{ZFC} + \lnot \operatorname{Con}(\mathsf{ZFC} + H) \vdash \lnot \operatorname{Con}(\mathsf{ZFC}), </math>

which gives (*). The core of the relative consistency proof is proving (**). A <math> \mathsf{ZFC} </math> proof of <math> \operatorname{Con}(T + H) </math> can be constructed for any given finite subset <math> T </math> of the <math> \mathsf{ZFC} </math> axioms (by <math> \mathsf{ZFC} </math> instruments of course). (No universal proof of <math> \operatorname{Con}(T + H) </math> of course.)

In <math> \mathsf{ZFC} </math>, it is provable that for any condition <math> p </math>, the set of formulas (evaluated by names) forced by <math> p </math> is deductively closed. Furthermore, for any <math> \mathsf{ZFC} </math> axiom, <math> \mathsf{ZFC} </math> proves that this axiom is forced by <math> \mathbf{1} </math>. Then it suffices to prove that there is at least one condition that forces <math> H </math>.

In the case of Boolean-valued forcing, the procedure is similar: proving that the Boolean value of <math> H </math> is not <math> \mathbf{0} </math>.

Another approach uses the Reflection Theorem. For any given finite set of <math> \mathsf{ZFC} </math> axioms, there is a <math> \mathsf{ZFC} </math> proof that this set of axioms has a countable transitive model. For any given finite set <math> T </math> of <math> \mathsf{ZFC} </math> axioms, there is a finite set <math> T' </math> of <math> \mathsf{ZFC} </math> axioms such that <math> \mathsf{ZFC} </math> proves that if a countable transitive model <math> M </math> satisfies <math> T' </math>, then <math> M[G] </math> satisfies <math> T </math>. By proving that there is finite set <math> T'' </math> of <math> \mathsf{ZFC} </math> axioms such that if a countable transitive model <math> M </math> satisfies <math> T'' </math>, then <math> M[G] </math> satisfies the hypothesis <math> H </math>. Then, for any given finite set <math> T </math> of <math> \mathsf{ZFC} </math> axioms, <math> \mathsf{ZFC} </math> proves <math> \operatorname{Con}(T + H) </math>.

Sometimes in (**), a stronger theory <math> S </math> than <math> \mathsf{ZFC} </math> is used for proving <math> \operatorname{Con}(T + H) </math>. Then we have proof of the consistency of <math> \mathsf{ZFC} + H </math> relative to the consistency of <math> S </math>. Note that <math> \mathsf{ZFC} \vdash \operatorname{Con}(\mathsf{ZFC}) \leftrightarrow \operatorname{Con}(\mathsf{ZFL}) </math>, where <math> \mathsf{ZFL} </math> is <math> \mathsf{ZF} + V = L </math> (the axiom of constructibility).