 Wright sketched a derivation of the Dedekind-Peano axioms from Hume’s Principle. The deductions sketched would be carried out in standard second-order logic—‘standard’ in the sense that, in the presence of HP, all number-abstractive terms of the form #xΦ(x) can be proved to denote. Such a system is unfree with respect to its number-abstractive terms. This point holds even if the second-order logic in question is a free logic in the official sense of not being committed to the theorem-scheme ∃!t (i.e., ∃x x = t) for any well-formed singular term t. The proof of this point is short and easy, and is like the one given in  §1.2.3.  We shall given an informal version as follows. 