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 Σ 1 ( 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 ℓ I , the Löwenheim number of this logic, is less than the least weakly inaccessible δ, then (i) ℓ I is a limit of measurable cardinals of K, and (ii) the Weak Covering Lemma holds at δ.