[FOM] The necessity of forcing

[Ilya Tsindlekht]

On Thu, May 10, 2007 at 12:29:36PM -0400, joeshipman at aol.com wrote:
>  From private responses to my previous post, I satisfied myself that 
> forcing is useful for proving results about weaker systems than ZF, but 
> does not appear to be necessary for these. On the other hand, no one 
> responded to my last 2 queries, so I will restate them in a more 
> provocative form:
> 
> 
> CLAIM: There is no important result (provable in ZFC) of the form
> 
> If ZFC is consistent, then neither A nor ~A is a theorem of ZFC
> 
> which has been proven without using forcing in at least one of the two 
> halves of the result.
> 
The only ways of proving A is not a theorem of ZFC that I am aware of
are 1) proving that ~A can be forced and 2) proving that ~A is theorem
of ZF + V=L. The latter cannot work for both A and ~A, so I am inclined
to think your claim is true.

There is a proof that Axiom of Choice is not a theorem of the version of
ZF which allows atoms (elementary objects not being sets) which does not
use forcing. (AC is a theorem of ZF + V=L so you can prove without 
forcing that both AC and ~AC are consistent with ZF with atoms.)