Supplement to Frege's Theorem and Foundations for Arithmetic
Proof of Hume's Principle from Basic Law V — Grundgesetze-Style
[Note: We use εF to denote the extension of the concept F.]
Let P,Q be arbitrarily chosen concepts. We want to show:
#P = #Q ≡ P ≈ Q
(→) Assume #P = #Q (to show: P ≈ Q). Note that since P ≈ P (this is Fact 2 in the subsection on Equinumerosity), we know by the previous Lemma that εP ∈ #P. But then, by identity substitution, εP ∈ #Q. So, by our previous Lemma, P ≈ Q.
(←) Assume P ≈ Q (to show: #P = #Q). By definition of #, we have to show εP≈ = εQ≈. So, by Basic Law V, we have to show ∀x(P≈x ≡ Q≈x). We pick an arbitrary object b (to show: P≈b ≡ Q≈b).
(→) Assume P≈b. Then, by definition of P≈ and λ-Conversion, ∃H(b = εH & H ≈ P). Let R be an arbitrary such concept; so b = εR & R ≈ P. From the second conjunct and our initial hypothesis, it follows (by the transitivity of equinumerosity) that R ≈ Q. So, reassembling what we know, it follows that b = εR & R ≈ Q. By existential generalization, it follows that ∃H(b = εH & H ≈ Q). So by λ-Conversion,[λx ∃H(x = εH & H ≈ Q)]b
It follows from this, by definition, that Q≈b.