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 (Fact 2, subsection on Equinumerosity), we know by the Lemma for Hume's Principle that ϵP∈#P. But then, by identity substitution, ϵP∈#Q. So, again by the Lemma for Hume's Principle, 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 of Q≈, that Q≈b.
(←) (Exercise)
