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:
- 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.
- 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.
- 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).
