 Another indication of the dependence of second-order logic on set theory as the metatheory is the result of Barwise to the effect that the existence of the Hanf number of second-order logic is not provable in set theory without a highly complex use of the Replacement Axiom (for details, see Barwise 1972b).