When cardinals determine the power set: inner models and Härtig quantifier logic

We show that the predicate "x is the power set of y" is Σ₁(Card)‐definable, if V = L[E] is an extender model constructed from a coherent sequences of extenders, provided that there is no inner model with a Woodin cardinal. Here Card is a predicate true of just the infinite cardinals. From this we conclude: the validities of second order logic are reducible to V_I, the set of validities of the Härtig quantifier logic. Further we show that if no L[E] model has a cardinal strong up to one of its ℵ‐fixed points, and l_I, the Löwenheim number of this logic, is less than the least weakly inaccessible δ, then (i)l_I is a limit of measurable cardinals of K, and (ii) the Weak Covering Lemma holds at δ.