4
$\begingroup$

Forcing is a method of "adding sets" to a model $M$ of ZF by making a new set $M^{(\mathbb{P})}$ consisting of every set of $M$, but you have the option to add certain sets out of $M^{(\mathbb{P})}$ as to guarantee you get a new model of ZF.

Intuitively, if you force with a bunch of functions from $\omega^M$ to $\omega_1^M$, then in the new model, what was once $\omega_1^M$ is now a countable ordinal. This is choosing to keep as many sets in $M^{(\mathcal{P})}$ which are "evidence that $|\omega_1^M|=\aleph_0$" as possible. (OVERSIMPLIFICATION)


The reason this is effective for CH is because it makes $\omega_1^M$ look smaller by adding enough such functions to the universe. The idea is that you add things which are "evidence of your axiom being true" and discard nearly everything else.

The question is this: could you also remove things which are "evidence of your axiom being false?"

Let's say there is this magical method of doing this called antiforcing. It would have some interesting applications:

  1. Perhaps, starting in a model of the axiom of determinacy, one could antiforce with winning strategies to make a model of ZF in which the axiom of determinacy fails.
  2. Starting in a model of the existence of a certain large cardinal, say, a measurable cardinal, it may be possible to antiforce with $\kappa$-complete nonprinciple ultrafilters, leaving $\kappa$ a non-measurable cardinal, but intuitively not "collapsing" anything; that is, the cardinals around it are undisturbed.
  3. Most importantly (and the real reason I was thinking of this), starting with a model of $V\neq K$ for some core model $K$, and a large cardinal $\kappa$ with $|(\kappa^+)^K|\neq\kappa^+$, one could antiforce with many surjections from $\kappa$ to $(\kappa^+)^K$, making a model of $K$ in which $(\kappa^+)^K=\kappa^+$.

You may be wondering why the last one is important; well, it's a way to "antiforce the sharp away" for a given core model. This could perhaps mean that, starting with the existence of a large cardinal $\kappa$ with cardinal property $P$, if this method of "antiforcing" preserves $P$, then the existence of a cardinal with $P$ doesn't imply the sharp exists; meaning that $K$ is an inner model for $P$.


Here's the question: Has this been thought of before (I assume it has)? What would be some good ways to go about doing it? (Of course, using an inner model would work, but I want a method more similar to 'undoing' forcing rather than just removing all non-constructable sets).

$\endgroup$
  • 3
    $\begingroup$ I may misunderstand, but "removing" sets was initially considered as easier, leading to proofs of the consistency of AC or CH (assuming that of ZF), much before Cohen introduced forcing to prove consistency of their negation. $\endgroup$ – YCor Sep 24 '18 at 18:49
  • 10
    $\begingroup$ You should probably read about set-theoretic geology and its inner model-theoretic version. $\endgroup$ – Andrés E. Caicedo Sep 24 '18 at 18:52
  • 2
    $\begingroup$ @KeithMillar Assuming we're talking about inner models with the same ordinals, shouldn't it be the case that it's possible to remove some set $A$ while preserving some set $B$ if and only if $A \notin L(B)$? $\endgroup$ – James Hanson Sep 24 '18 at 19:06
  • 7
    $\begingroup$ Keith, I didn't just say inner model theory, but rather inner model-theoretic geology. In any case, one of the key motivators of inner model theory is very close to what you are after. The evolution of covering lemmas illustrates this dramatically. $\endgroup$ – Andrés E. Caicedo Sep 24 '18 at 20:06
  • 3
    $\begingroup$ Your question is too vague to say much more than what Andrés already did by way of an answer. Concerning your item 3, though, which large cardinals $\kappa$ do you have in mind? $|(\kappa^{+})^K| = \kappa$ is plain false if $\kappa$ is weakly compact (or e.g. carries a precipitous ideal). $\endgroup$ – Ralf Schindler Sep 27 '18 at 8:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.