Frege's Theorem says that it is possible to prove Peano's Axioms from Hume's Principle in the context of second-order logic. Recall that second-order logic uses two types of letters, which cannot be mixed: little--for things--and big--for classes or predicates. It also benefits from unrestricted comprehension. Recall also that Hume's Principle (HP) is:

(P)(Q)(#P = #Q <=> P == Q)

#P means "the number of P"
P == Q means "there is a 1-1 functional relationship from P onto Q"

(P)[n] Mn,P
(P)(Q)(n) ( Mn,P => (P == Q <=> Mn,Q) )
(P)(n)(m) (Mn,P & Mm,P => n = m)

(P) means "for all P"
[n] means "there exists n"
Mn,P means "P numbers n"

Frege's Theorem goes through, of course, only if one is allowed to define zero, the successor function and the natural numbers. These definitions--it is better to call them axioms--are:

M0,{x : ~x = x}
(m)(n) (Sm,n <=> [P][a] (~Pa & Mm,P & Mn,{x : Px V x = a}))
(n) (Nn <=> n = 0 V (P) [ (a)(b) ( [(a = 0 V Pa) & Sa,b] => Pb) => Pn ]

0 means "zero"
Sm,n means "n succeeds m"
Nn means "n is a natural number"

Now Frege's Theorem is a big thing, and at least a few think it is important. It is therefore germane to point out that the axioms--that is, unrestricted comprehension plus HP plus three implicit mathematical axioms--can be weakened significantly.

The "Dedekind's Proof" posting considers the following system:

F1 (x)({x : phi}x <=> phi) where phi does not contain any bound variables or free x in the predicate position
F2 (x)(y)({x,y : phi}x,y <=> phi) where phi does not contain any bound variables or free x or y in the predicate position
F3 (n)(m)(P) ( Nn & Mn,P & Mm,P => n = m)
F4 (P) (M0,P <=> (x) ~Px)
F5 (n)(m)(P)(Q)(a) ( Nn & Sn,m & ~Pa & (x)(Qx <=> Px V x = a) => (Mn,P <=> Mm,Q) )
F6(rule of induction: phi any formula, (x\y) means x substituted for free instances of y, supposing that x does not become bound in any of these occurences)

phi(0\n)
(n)(m) ( Nn & Sn,m & phi => phi (m\n) )
-------------------------------------------------
(n) ( Nn => phi )

In "Dedekind's Proof", it is proven that there are an infinite number of things in this system, i.e.

(n)(Nn => [P][a] Mn,P & ~Pa) (POTINF)

However, there is nothing in these axioms which ensures that there are natural numbers at all, so two additional axioms are needed:

F7 N0
F8 (P)(a)(n)(Nn & Mn,P & ~Pa => [m] (Nm & Mm,{x : Px V x = a}))

Peano's Axioms (pre-addition) are:

PA1 N0
PA2 (n)(Nn & Sn,m => Nm)
PA3 (n)(Nn => [m] Sn,m)
PA4 (n)(m)(m')(Nn & Sn,m & Sn,m' => m = m')
PA5 (n)(m)(n')(Nn & Nn' & Sn,m & Sn',m => n = n')
PA6 (n) (Nn => ~Sn,0)
PA7 Induction

They can be proved as follows:

R1 N0 (PA1)
Pf: This is axiom F7.

R2 (n)(m)(Nn & Sn,m => Nm) (PA2)
Pf: Let Nn & Sn,m. By POTINF, Mn,P & ~Pa for some P,a. By F5, Mm,{x : Px V x = a}. By F8, Nm' & Mm' & Mm',{x : Px V x = a}, for some m'. By F3, m = m'. So Nm.