The axiom of infinity excludes and all smaller stages, so the cardinal is uncountable. Full semantics for second-order logic is decisive: every externally specified functional relation whose ordered pairs lie in is an allowed class parameter, even if the relation itself is not an element of .
If , choose an external cofinal function . Its graph is an allowed class parameter: each input, output and ordered pair has rank of a set below the infinite cardinal , which is a limit ordinal. The domain belongs to . The second-order form of Axiom schema of replacement would give its range as an element of . But a cofinal subset of has rank of a set and cannot belong to . Therefore .
If for a cardinal , choice supplies an external surjection . The domain belongs to and the ordered pairs of its graph have ranks below . Applying Axiom schema of replacement to this external functional class would put its range, the ordinal , in , again impossible. Hence for every .
Consequently
These are exactly the defining conditions for a strongly inaccessible cardinal. This full second-order replacement rank obstruction would not follow from Henkin semantics, where the available class relations may exclude the external functions just used.