How can you make sense of "equinumerosity" in Hume's Principle in a logicist approach to math, without first having functions defined?

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?

Thank you!

See Frege's Theorem: Equinumerosity: the "bijection" is not defined set-theoretically, and thus there is no need of the ordered pair notion.

F and G are equinumerous just in case there is a relation R such that: (1) every object falling under F is R-related to a unique object falling under G, and (2) every object falling under G is such that there is a unique object falling under F which is R-related to it.

In symbols:

F ≈ G = (def) ∃R [∀x(Fx → ∃!y(Gy & Rxy)) & ∀x(Gx → ∃!y(Fy & Ryx)]

• Cool, thank you very much. That should've been obvious to me since concepts are not defined set-theoretically, and you want to avoid Basic Law V and extensions.
– user
Commented Feb 23, 2021 at 16:17
• @user - recall that Frege's Logic was independent from set theory (at that time: the Cantor's version) and amounts to modern High-Order Logic. Commented Feb 23, 2021 at 16:19
• LOL it's tough for me. I'm a recovering mathematician. I hear "course of values" and "extension" and I automagically think set of ordered pairs and set comprehension. It's hard thinking to change.
– user
Commented Feb 23, 2021 at 16:55