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 f ollows: the number (die Anzahl) which belongs to the concept F is the exten sion 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 arithmet ic. In those derivations, however, Frege did not use the explicit definitio n of number. Rather he used a kind of contextual definition of number which is now called 'Hume's Principle': # F = # G <--> F approximate to G where '#F' means 'the number which belongs to the concept F', 'F approximat e to 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 an d objects falling under the concept G'. Unlike in Frege's explicit definiti on, in this contextual definition the essence of number, that is, what numb er is, is not given, but only the criterion of identity of numbers. According to Frege's later system of Grundgesetze der Arithmetik (Frege 189 3-1903) the criterion of identity of the extensions of concepts is given by Axiom V as the coextension of those concepts: 'epsilonF epsilon = 'alphaG alpha <-> For Allx(Fx <-> Gx) (the extension of the concept F is the same a s 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 approximate to X) (the number belonging to the concept 'equinumerous to the concept F') is connected with the instance of (second-order) Axiom V: 'X(F approximate to X) =' Y(G approximate to Y) <-> For AllH(F approximate to H <-> G approximate to H), there is the dang er that a contradiction like Russell's paradox might arise. Therefore, in o rder to avoid contradiction, it is desirable to use a principle which is gu aranteed consistency. Recently several researchers(1) have noticed that in the Grundlagen, Frege gave a basis sufficient to derive theorems of arithme tic (including Peano Arithmetic), but using only Hume's Principle-which is consistent. Boolos believes that this work of Frege is significant enough t o 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 Pri nciple in this system explicit. Then in section 2, we actually derive some theorems of arithmetic, including Peano's five axioms, by reconstructing Fr ege's arguments in 74-83 of his Grundlagen. Lastly, in section 3, we consid er the significance of Frege's theorem and locate it in his whole logistic programme. This suggests that, despite the discovery of inconsistency in th e Grundgezetze, Frege's logicism can be seen in a new and more favourable l ight.