Frege's theorem and his logicism

As is well known, Frege gave an explicit definition of number (belonging to some concept) in §68 of his Die Grundlagen der Arithmetik (Frege 1884) as follows: the number (die Anzahl) which belongs to the concept F is the extension of the concept 'equinumerous to the concept F'. Here number is defined as an extension of some second-order concept. In other words, a number is a kind of object. After having defined individual numbers, in the following sections (§§74-83) Frege showed how to derive the main theorems of arithmetic. In those derivations, however, Frege did not use the explicit definition of number. Rather he used a kind of contextual definition of number which is now called 'Hume's Principle':

#F = # G ↔ F ≊ G

where '# F' means 'the number which belongs to the concept F', 'F ≊ G' means 'the concept F is equinumerous to the concept G' or 'there is a one-to-one correspondence between objects falling under the concept F and objects falling under the concept G'. Unlike in Frege's explicit definition, in this contextual definition the essence of number, that is, what number is, is not given, but only the criterion of identity of numbers.

According to Frege's later system of Grundgesetze der Arithmetik (Frege 1893-1903) the criterion of identity of the extensions of concepts is given by Axiom V as the coextension of those concepts: 'F = 'αGα ↔ ∀x(Fx ↔ Gx) (the extension of the concept F is the same as the extension of the concept G if and only if every object falling under the concept F falls under the concept G and vice versa). When the explicit definition of number: # F = 'X(F ≊ X) (the number belonging to the concept 'equinumerous to the concept F') is connected with the instance of (second-order) Axiom V : 'X(F ≊ X) = 'Y(G ≊ Y) ↔ ∀H(F ≊ H ↔ G ≊ H), there is the danger that a contradiction like Russell's paradox might arise. Therefore, in order to avoid contradiction, it is desirable to use a principle which is guaranteed consistency. Recently several researchers¹ have noticed that in the Grundlagen, Frege gave a basis sufficient to derive theorems of arithmetic (including Peano Arithmetic), but using only Hume's Principle-which is consistent. Boolos believes that this work of Frege is significant enough to deserve the title 'Frege's Theorem'.

The purpose of the present paper is, first, to confirm this claim of Boolos' by following his arguments that Frege's results, which he calls 'Frege's theorem', can be established, and second, to reconsider the significance of Frege's results for the logicist program. In section 1, in accordance with Boolos, we construct 'Frege arithmetic', a formal system which will serve as the foundation to prove Frege's theorem, and make the role of Hume's Principle in this system explicit. Then in section 2, we actually derive some theorems of arithmetic, including Peano's five axioms, by reconstructing Frege's arguments in §§74-83 of his Grundlagen. Lastly, in section 3, we consider the significance of Frege's theorem and locate it in his whole logistic programme. This suggests that, despite the discovery of inconsistency in the Grundgezetze, Frege's logicism can be seen in a new and more favourable light.