Among the great pioneers of logic, Gottlob Frege (1848-1925) should certainly be mentioned. His magnum opus, Begriffschrift (in English, "Concept Writing") introduced many basic ideas of modern logic that are also very important for the study of programming languages, including the idea of applying a function to an argument (as opposed to the classical Greek way of doing it with subject and object), propositional logic, quantification, and the modern idea of formal proof (i.e., proofs based on the form of what is to be proved, as opposed to the classical Greek proofs by syllogism).

Well founded induction for the Peano signature does require proving P(0): if we let x=0, then we get the implication true => P(0), which is equivalent to P(0), as our proof obligation for this case.

It is also worth mentioning that all of the rules of deduction for first order logic can be seen as part of a Post system.

Two assertions about initial algebras not proved in the book have short proofs, which are, however, quite abstract and algebraic. They rely on the characterizization of an initial algebra as a Sigma-algebra having exactly one Sigma-homomorphism to any other Sigma-algebra; this is called its universal property. Here are the two properties to be proved:

1. Any two initial Sigma-algebras are isomorphic.
    
2. An initial Sigma-algebras has no proper sub-Sigma-algebras.

If f: I -> I is a homomorphism from an initial algebra to itself, then f is the identity map on I .

This lemma follows from noticing that the identity map on I is a homomorphism on I , and that the universal property then implies it is the only one.

For the first assertion, let I, I' be initial algebras. Then there are homomorphisms f: I -> I' and g: I' -> I , and hence f;g: I -> I and g;f: I' -> I' are also homomorphisms. By the lemma, f;g and g;f must be identity maps, which implies that they are inverses, which means that I and I' are isomorphic.

For the second assertion, let I' be a subalgebra of an initial algebra I , and let f: I' -> I be the inclusion. The universal property implies there is also a homomorphism g: I -> I' , and the lemma implies g;f: I -> I is the identity, which in turn implies that f is surjective. Now since f is both surjective and injective (i.e. onto and one-to-one, in the older terminology), it is an isomorphism.

Everything above about initial algebras generalizes to the case where we consider not just Sigma-algebras, but Sigma-algebras that satisfy a given set E of equations. Here the pair (Sigma, E) defines an abstract data type, and its initial algebra (up to isomorphism) is a canonical model for the abstract type. (See the bottom of page 252 of Sethi.)