9
$\begingroup$

We are forced to use forcing for almost all "hard" independence results such as: $Con(ZFC)\longrightarrow Con (ZFC+\neg CH) $. The question simply is:

Primary Question: Is there any "forcing free" proof for $Con(ZFC)\longrightarrow Con (ZFC+\neg CH) $ or $Con(ZF)\longrightarrow Con (ZF+\neg AC) $ or any other "hard" independence results?

Secondary Question: Please list all "non simple" consistency results which have two proofs one by forcing and another without using it.

$\endgroup$
6
  • $\begingroup$ Related. $\endgroup$ Commented Aug 7, 2013 at 13:55
  • 1
    $\begingroup$ No, there are no forcing-free proofs of any of these results. It would be great to come upon such a new technique. There are, of course, a few independent results that do not rely on forcing, but I do not know i they are of the kind you are seeking. There is the consistency of Aczel's anti-doundation axiom, for example. See also here. $\endgroup$ Commented Aug 7, 2013 at 14:01
  • $\begingroup$ I thought I heard that Moschovakis has a proof of independence of V=L by omitting ordinals, rather than by forcing. $\endgroup$ Commented Aug 7, 2013 at 14:10
  • $\begingroup$ In Fraenkel atoms model AC fails. $\endgroup$
    – Eran
    Commented Aug 7, 2013 at 19:22
  • 1
    $\begingroup$ @Eran And we have atoms, so we do not have extensionality, and the underlying theory is not $\mathsf{ZF}$. $\endgroup$ Commented Aug 7, 2013 at 23:55

1 Answer 1

6
$\begingroup$

Krivine realizability can be used to obtain independence results over $\mathsf{ZF}$. For instance, in Krivine's paper Realizability algebras II : new models of ZF + DC, Logical Methods in Computer Science 8 (1:10) p. 1-28 (2012), he constructs a realizability model in which $\mathsf{AC}$ fails in a pretty strong way: there is an infinite sequence of infinite subsets of $\mathbb{R}$ strictly decreasing in cardinality.

$\endgroup$
2
  • 2
    $\begingroup$ This is nice! It is perhaps too soon to see whether we can get new results this way, but it has potential. Krivine says that forcing posets are a particular case of realizability algebras, and there are some similarities, but to me the flavor of this approach is different. $\endgroup$ Commented Aug 9, 2013 at 15:30
  • 2
    $\begingroup$ The fear is that this ends up as "sheaf forcing", as studied by Xavier Caicedo and his students, see here for an example. We also have here a more general framework than forcing and unfortunately no new independence results yet. $\endgroup$ Commented Aug 9, 2013 at 15:49

You must log in to answer this question.