Dear Peter and Sy,
I would like to add a short comment about the move to . This concerns to what extent it can be formulated without consulting the hyper-universe is an essential way (which is the case for since can be so formulated). This issue has been raised several times in this thread.
Here is the relevant theorem which I think sharpens the issues.
Theorem. Suppose holds, Let be the set of all ctm such that satisfies . Then is not -definable over the hyperuniverse. (lightface).
Aside: is always definable modulo being #-generated and being #-generated is -definable. So X is always -definable. If one restricts to of the form for some real , then is -definable but still not -definable.
So it would seem that internalization to via some kind of vertical extension etc., might be problematic or might lead to a refined version of which like IMH has strong anti-large cardinal consequences.
I am not sure what if anything to make of this, but I thought I should point it out.