Dear Sy,

Before we close this thread, it would be nice if you could state what the current version of is. This would at least leave me with something specific to think about.

Is it:

1) (SDF: Nov 5) M is weakly #-generated and for each phi, if
for each countable alpha, phi holds in an outer model of M which
is generated by an alpha-iterable presharp then phi holds in an inner model of M.

2) (SDF: Nov 8) M is weakly #-generated and for all : Suppose that whenever is a generator for M (iterable at least to the height of M), holds in an outer model M with a generator which is at least as iterable as . Then holds in an inner model of M.

or something else? Or perhaps it is now a work in progress?

Regards,
Hugh