Supplement to Frege's Theorem and Foundations for Arithmetic
Proof of the General Principle of Induction
Assume the antecedent of the principle, eliminating the defined notation for HerOn(F, aR+):
Pa & ∀x,y(R+(a,x) & R+(a,y) & Rxy → (Px → Py))
We want to show, for an arbitrary object b, that if R+(a,b) then Pb. So assume R+(a,b). To show Pb, we appeal to Fact (7) about R+ (in our subsection on the Weak Ancestral in §4):
Fx & R+(x,y) & Her(F,R) → Fy
Instantiate the variable F in this Fact to the property [λz R+(a,z) & Pz] (that there is such a property is guaranteed by the Comprehension Principle for Relations), and instantiate the variables x and y to the objects a and b, respectively. The result (after applying λ-Conversion) is therefore something that we have established as true:
R+(a,a) & Pa & R+(a,b) & Her([λz R+(a,z) & Pz], R) →
R+(a,b) & Pb
So if we can establish the antecedent of this fact, we establish Pb. But we know that the first conjunct is true, by the definition of R+. We know the second conjunct is true, by assumption. We know that the third conjunct is true, by further assumption. So if we can establish:
Her([λz R+(a,z) & Pz], R),
we are done. But, by the definition of heredity, this just means:
∀x,y[Rxy → ((R+(a,x) & Px) → (R+(a,y) & Py))].
To prove this claim, we assume Rxy and R+(a,x) & Px (to show: R+(a,y) & Py). But from the facts that R+(a,x) and Rxy, it follows from Fact (3) about R+ (in our subsection on the Weak Ancestral) that R*(a,y). This implies R+(a,y), by the definition of R+. But since we now have R+(a,x), R+(a,y), Rxy, and Px, it follows from the first assumption in the proof that Py.