Very impressive! Thanks for the travel guide through the actualist class-theory literature! It seems to be a minefield out there, so the safest move for me is to try to develop a “wimpy HP” that only draws on classes which are first-order definable. I say “wimpy” because this move really takes the juice out of the theory and has the smell of fear in it (“Oh no, I can’t even imagine Tarski’s satisfaction relation for V, because it’s not definable! I’m scared that something awful might happen if we do that!”)
OK, so here is the WHP (Wimpy HP): Height maximality means nothing more than ZFC, i.e. first-order reflection (with set-parameters). (I already have tears in my eyes.) Width maximality means that if we take a wimpy-thickening of V we don’t discover new properties, where a wimpy-thickening of V (no quotes necessary!) is a V-definable structure V-thick (whose universe and relations are V-definable classes) together with a V-definable interpretation of (V,membership) into V-thick. (The “interpretation” should obey the usual good rules for interpretations; in particular any first-order property of (V, membership) translates faithfully into a first-order property of V-thick). So Wimpy-IMH says that if a first-order sentence holds in some wimpy-thickening of V then it holds in a definable inner model of V.
The classical example of a wimpy-thickening is the Scott-Solovay Boolean-valued universe where is a set-sized complete Boolean algebra. A more courageous example is where is a definable class-sized “tame” set-complete Boolean algebra (for the definition of “tame” see my book on class-forcing). At the moment no other natural example comes to mind. Note how “wimpy” this is: surely can have “thickenings” with superhuge cardinals but it can’t even have a wimpy-thickening with ! (On the other hand I have to confess that even Wimpy IMH has powerful consequences, like the nonexistence of inaccessibles).
I conjecture that if someone rejects the HP because it doesn’t sit well with height actualism and gets interested in the Wimpy HP, they will soon regret it and wish they had attended the Real Non-Wimpy HP party.
P.S. I thought I’d keep this out of the text above because it’s rather speculative. Earlier it was intimated that the actualist can’t interpret IMH in a satisfactory manner. I’m not sure I see this; there are plenty of ways of simulating a forcing extension of within . For example, Hamkins and Seabold (http://arxiv.org/abs/1206.6075) show how you can replace with an elementary extension ,
Whoops, how does a severe actualist pull that off? When you move to a (proper) elementary extension you are taking a model of a rather fancy, non-first-order definable theory. It seems you’ve already violated the promise that all classes are first-order definable if you want to think about that theory.
So probably you didn’t mean “fully elementary” but only “ elementary for some big “.
But more seriously: Note that your elementary extension may fail to be an end-extension! I.e., it may even have nonstandard natural numbers! If “thickenings” of are to be useful then they can’t change the ordinals. For this reason we’re forced into an infinitary logic where we can form a theory which ensures that the ordinals of don’t change (or are at least an initial segment of the ordinals of the “imaginary universe”, so we can take a simple “truncation” back to ). In fact we need to get all of the sets of “fixed” by that theory. To get such a logic we’re forced to my “slight lengthening” of to a model of KP with as an element, and if an actualist can accept that then she might as well let loose and buy the whole HP package, leaving her life as a wimp behind.
pick a -generic from , and simulate the forcing extension of with . Why not just do the same with IMH? For example, for the Weak Inner Model Hypothesis we could have:
[WIMH-V] If holds in an inner model of some appropriate elementary extension of , then already holds in an inner model of .
If you take to be an elementary extension and “inner model” to mean “definable inner model” then this will be true automatically; it has no strength.
The matter is complicated by the fact that the are quite often non-well-founded, but I don’t see that this would affect the results any. You could motivate such a version with exactly the same reasons as the original Weak Inner Model Hypothesis; should be as “wide” as possible in
the sense that it contains a very high density of inner models, we just require a deviant interpretation for some models to explain how this should be understood. I don’t see, therefore, that the width potentialism is a necessary part of motivating width maximality.
I’ll think about it a bit more, but as I said above I don’t think that it is useful to look at non well-founded “thickenings” of V. And for HP purposes it doesn’t change anything to consider well-founded “thickenings” that live in a non well-founded “imaginary universe”.
Many thanks for your comments!