Sy Friedman's "Inner Model Hypothesis" (IMH) asserts that every first-order
parameter-free sentence in the language of arithmetic that holds in some outer
model of V already holds in some definable inner model. In collaboration with
Philip Welch and Hugh Woodin, he has shown that the IMH is consistent from a
Woodin cardinal with an inaccessible above and has consistency strength at
least that of measurable cardinals of arbitrarily high Mitchell order.

The IMH itself is incompatible with large cardinals and implies that the
universe is minimal: By a theorem of Beller and Jensen, there exists a real x
in any model of the IMH such that
L_alpha[x] does not satisfy ZFC, for all alpha. For this same reason
the IMH cannot be extended to sentences with arbitrary real parameters.
(Consider "omega_1 of L[x] is countable".)

We consider a variant of the IMH that is compatible with large cardinals,
allows real parameters, and does not imply that the universe is minimal.
Indeed, if the universe is sufficiently non-minimal, then this variant has a
first-order formulation.