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.
Regards,
Hugh