FOM: Neo-Fregean reverse mathematics

[Alasdair Urquhart]

Roger Jones's posting of 14 March on the Arche
project (of which he is rather critical) got me thinking
about some questions, both philosophical and logical.

First, I quite agree with the silliness of naming the
cardinality principle "Hume's Principle" -- but I've little to
add to what Bill Tait already said on this.  The passage in
Hume that is taken to justify this nomenclature (Treatise,
Book I, Part iii, Section 1) seems in fact to amount to the
idea that you can determine when two positive integers are 
the same by writing them out as N = 1 + 1 + 1 + ... + 1 and
then comparing units.  This has little or nothing to do
with Cantor's general cardinality principle.  Admittedly, this misreading
of Hume goes back to Frege (Grundlagen, Section 63), but 
I don't see why we should perpetuate this misreading.

All this is just terminology, and hardly serious.  But a more
serious problem in the "Neo-Fregean" literature is the persistence
with which people refer to "Hume's Principle" as a 
"contextual definition."  Boolos (who certainly knew better) 
refers repeatedly to the principle as a contextual definition
in the papers reprinted in "Logic, Logic, and Logic."
The Arche web site also refers to the axiom in this way.
But how can it be a "contextual definition" when it has
the axiom of infinity as a direct logical consequence?
How can it be a definition of any kind at all?

This brings me to my logical question.  Does anyone know
what is the exact proof-theoretical strength of the
cardinality principle?  That is to say, starting from
the conventional first-order language of set theory,
can we find a system that is in some sense equivalent to (some form of)
higher order logic + the cardinality principle?  A result
along this line would clarify the status of the cardinality
principle.

Alasdair Urquhart