Pure second-order logic is second-order logic without functional or first-order
variables. In "Pure Second-Order Logic," Denyer shows that pure second-order
logic is compact and that its notion of logical truth is decidable. However, his
argument does not extend to pure second-order logic with second-order identity.
We give a more general argument, based on elimination of quantifiers, which
shows that any formula of pure second-order logic with second-order identity is
equivalent to a member of a circumscribed class of formulas. As a corollary,
pure second-order logic with second-order identity is compact, its notion of
logical truth is decidable, and it satisfies a pure second-order analogue of
model completeness. We end by mentioning an extension to nth-order pure
logics.