I'm pretty sure that I am misunderstanding something here, but I'm not sure what.
How can you make sense of "equinumerosity" in Hume's Principle in a logicist approach to math, without first having functions defined?
You want to be able to derive the natural numbers from principles of logic, and so you rely Hume's Principle as a type-lowering abstraction principle:
The "number" of things with property P is the same as the "number" of things with property Q if and only if the Ps and Qs are equinumerous.
I figure I just don't understand how "equinumerous" is being used here. Is it required that equinumerosity is witnessed by a bijection, and if so how can "function" be defined without ordered pairs?