I have to say that after the two last posts by Timothy Chow on Forcing I got so intrigued that I am trying to rethink the little I know about this formidable chapter of mathematics.
I have also to add that, although aware of the new field of set-theoretic geology, I am far from having a full grasp of it, so pre-emptive apologies to experts if I ask something that is either trivial or false.
Onto the point. Suppose I start from a transitive model of set theory $M$, and, rather than trying to expand it, I would rather do something opposite, namely the following: given an element $G$ of the model, try to "yank it out", to remove it surgically so that what remains is still a transitive model $M_0$.
In other words, try to establish $M= M_0[G]$.
Of course things are not so easy: I want to eliminate $G$ from $M$, but obviously I have to get rid of a lot of other sets in $M$ which are associated to $G$, for instance other sets which would imply its existence. Moreover, I have to choose judiciously whether or not $G$ is removable in such a way that after its removal (and of its "peers" ) the remaining set is still a model of $ZF$ of the same ordinal height.
I would call this operation selective erosion (if there is a canonical name for this operation please supply it) .
I understand that this may not be possible in some scenarios: for instance if $M$ is the minimal model, it is too "skinny" to allow for removals. But, unless intuition fails me, there should be plenty of "fat" models which should be liable to erosion.
MOTIVE
The way I look at this scenario is kind of the reciprocal of forcing: I would like to yank out some specific $G$ which codes some specific truths in $M$, for instance get rid of some map which collapses some cardinals.
QUESTION:
Are there methods that can be employed to do the surgery I sketched ? Notice that I do not ask whether a model is liable to erosion, rather whether some specific sets can be removed, and if so how.
NOTE: if I already know that $M$ is a forcing extension by $G$, then the problem is already trivially solved. Rather, suppose I only know that $M$ is a transitive model and someone comes along and gives me a $G$ in the model, and asks: is $G$ removable? I want to answer yes or no. Again, in some particular case the negative answer is obvious (example if G is an ordinal in $M$). But what about less trivial cases?
ADDENDUM: After the comments of Asaf, and especially after the great first answer by Jonas, time to take stock: The first thing that comes to my mind is that there are at least TWO candidate strategies to tackle this problem (and perhaps neither of them is the good one). You can call them BOTTOM-UP, which is the one I have sketched very loosely in my "debate" with Asaf, and the one which I would call TOP-DOWN which is the one advocated by Jonas.
Let us briefly recap them:
- BOTTOM UP. Start from a minimal model $W_0$ such that $A\notin W$ (for instance the constructibles in $M$) , and look at the set of extensions $W$ of the bottom $W_0$ such that $W[A] \neq M$, ordered by inclusion, then try to take the colimit of this ordered set (in other words, you hope that the sup of all of them is a model and does not contain A, but adding A you get M) . Is such a beast exists you found your A-eroded M
- TOP DOWN See Jonas's answer (I would call it the "take the limit " method).
Notice that both could be considered a form of selective geology:
1 is like growing the "earth", from some core, till a layer where A is present is reached.
2 is actually more in line with erosion, getting rid of as much as you can, as so aptly Jonas said.
So, either going from non A-grounds and looking for their union, or from A-grounds and looking for their intersection
PROBLEM: Both methods rely on looking at a certain ordered set of models of ZF in the "universe' M, and on certain lattice operations which can be performed. I have absolutely no clue whether such operations (taking sups or infs) are admitted in all cases (my gut feeling is no).
The story continues....