Finitude and Hume's principle (Q1372939)

Let FA be the extension of second-order logic with the so-called Hume's principle HP, i.e. the claim that the number of a concept \(F\) is equal to the number of a concept \(G\) iff \(F\) and \(G\) are equinumerous (i.e. there is a bijection between the collection of objects falling under \(F\) and those falling under \(G\)). Of course, HP requires that the usual second-order language is expanded by a second-order term forming operator \(Nx:Fx\), to be read as ``the number of \(F\)s''. ``Frege's theorem'' is the statement that the Dedekind-Peano axioms of second-order arithmetic are derivable in FA. The main result of this paper is that Frege's theorem can actually be proved in a strictly weaker system FAF, where HP is restricted to \textit{finite} concepts (`finite' being defined according to Frege). Actually, the author proves more: FAF is equivalent to the Dedekind-Peano system PAF, extended with the axiom ``the predecessor of a natural number is a natural number''. The paper is relevant to the philosophical problem whether some form of logicism can be supported on the basis of HP. Against \textit{C. Wright} [\textit{Frege's conception of numbers as objects} (1983; Zbl 0524.03005)], the author argues that HP cannot be the `basic analytic law' underlying arithmetic; instead, he cautiously presents some reasons to believe that HPF could be a better candidate. The paper is well-written and informative, also as a tool for interpreting (parts of) Frege's \textit{Grundgesetze der Arithmetk}.