Stanford Encyclopedia of Philosophy

Supplement to Frege's Logic, 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 → (PxPy))

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.