Supplement to Frege's Logic, Theorem, and Foundations for Arithmetic
Proof of Lemma Concerning Zero
Let P be an arbitrarily chosen concept. We want to show #P = 0 ≡ ¬∃xPx.
(→) Assume #P = 0. Then, by definition of 0, #P = #[λz z≠z]. So by Hume's Principle, P is equinumerous to [λz z≠z]. So, by the definition of equinumerosity, there is an R that maps every object falling under P to a unique object falling under [λz z≠z] and vice versa. Suppose, for reductio, that ∃xPx, say Pa. Then there is an object, say b, such that Rab and [λz z≠z]b. But, then, by λ-Conversion, b is not self-identical, which contradicts the laws of identity.
(←) Suppose ¬∃xPx. Now as we have seen, the laws of identity guarantee that no object falls under the concept [λz z≠z]. But then any relation you please bears witness to the fact that P is equinumerous with [λz z≠z]. For let R be some arbitrary relation. Then (a) every object falling under P bears R to a unique object falling under [λz z≠z] (since there are no objects falling under P), and (b) every object falling under [λz z≠z] is such that there is a unique object falling under P that bears R to it (since there are no objects exemplifying [λz z≠z]). Since P is therefore equinumerous with [λz z≠z], it follows by Hume's Principle, that #[λz z≠z] = #P. But, then, by definition, 0 = #P.