It has long been known that in the context of axiomatic second-order logic (SOL), Hume’s Principle (HP) is mutually interpretable with “the universe is Dedekind infinite” (DI). In this paper, we offer a more fine-grained analysis of the logical strength of HP, measured by deductive implications rather than interpretability. Our main result is that HP is not deductively conservative over SOL + DI. That is, SOL + HP proves additional theorems in the language of pure second-order logic that are not (...) provable from SOL + DI alone. Arguably, then, HP is not just a pure axiom of infinity, but rather it carries additional logical content. On the other hand, we show that HP is $$\Pi ^1_1$$ conservative over SOL + DI, and that HP is conservative over SOL + DI + “the universe is well ordered” (WO). Next, we show that SOL + HP does not prove any of the simplest and most natural versions of the axiom of choice, including WO and weaker principles. Lastly, we discuss other axioms of infinity. We show that HP does not prove the Splitting or Pairing principles (axioms of infinity stronger than DI). (shrink)