[FOM] induction and reducibility

[Allen Hazen]

Two remarks.

(1)  Poincaré’s comment was in the context of his 
debate with Russell: Russell claimed that 
mathematics was “logic,” where logical truths are 
provable in his formal system of (ramified) 
Higher-Order Logic(*), Poincaré on the other had 
claimed that mathematics depended on an 
irreducibly “intuitive” (no I can’t say what that 
means, but anyway the implication is that it 
doesn’t reduce to logic) principle of 
mathematical induction.  In this context the 
claim that Russell’s axiom of reducibility is a 
form of induction makes sense.  Suppose you want 
to reproduce a proof of some theorem of (for 
concreteness say) PA as a formal proof in 
Russell’s system.  The proof you want to 
reproduce involves an application of mathematical 
induction: ...0..., and for any n (...n... implies
....n+1...), so for every n (...n...).  Natural 
numbers are defined (essentially: I’m simplifying 
a bit) as items that satisfy every “propositional 
function” (of a certain type) that is satisfied 
by 0 and by successors of items that satisfy 
it.  (“Propositional function,” if you aren’t 
interested in the details of Russell’s 
metaphysical semantics, can be interpreted 
roughly as “property.”)  So the proof is 
immediate ... ***IF*** you can show that ...x... 
defines a “propositional function” of the right 
type.  But sometimes (always, if ...x... involves 
unbounded quantification over natural numbers: so 
for any arithmètic formula that isn’t Delta-0) 
the formula will define a propositional function 
at the wrong “ramification-level” in Russell’s 
Ramified type theory.  The axiom of reducibility 
(in essence it says, in the language of Ramified 
Type Theory, that the propositional functions of 
minimal “ramification level” form a model of 
Simple Type Theory) is needed to close the 
gap.  In the polemical context, therefore, 
Poincaré had some justification in saying that 
the Axiom of Reducibility was a “disguised” appeal to Induction.

(2)  Russell’s formalization of his type theory 
(as has been complained repeatedly by many 
authors) wasn’t up to modern standards of 
formality.  Still, it is by now pretty clear what 
the system was meant to be.  (Probably the 
clearest easily accessible description is in 
Church’s “Comparison” of Russell and Tarski, in 
JSL v. 41 (1976), pp. 747-760.)  What Myhill does 
in the article cited in earlier posts is to give 
a model-theoretic proof that this system, without 
the Axiom of Reducibility, cannot give 
mathematical induction (for non-Delta-0 
conditions).  Gödel probably didn’t need Myhill’s 
proof, as there is an easier one from the Second 
Incompleteness Theorem: Ramified Type Theory can 
be formulated as a Sequent Calculus, the 
Hauptsatz is finitistically provable for it, so 
(lots of boring detail skipped(**)) if PA were 
interpretable in Russell’s system it would prove 
its own consistency and be inconsistent.    ...     ...
                          ....       ...  What’s 
not clear is that Myhill’s result applies to 
Russell’s claim in the appendix to the 1925 
edition of “Principia Mathematica”: in the 
introduction to that edition Russell had 
described (in ways that aren’t up to modern 
standards of formalization, of course: intuitive 
semantics and a few examples written out in 
notation that doesn’t make ramification levels 
explicit) a form of type theory that properly 
extends “standard” Ramified Type Theory, and 
undoubtedly thought of the (inadequately 
formalized: level specifications missing on 
variables!) argument in the appendix as being 
given in this new system.  It is clear from his 
comments in “Russell’s Mathematical Logic” that 
Gödel was aware of Russell’s liberalization of 
the Ramified theory, but most later commentators 
­ including Myhill ­ seem to have overlooked it 
until Jen Davoren and I, and (independently) 
Gregory Landini pointed it out in the 1990s.  (At 
the risk of sounding conceited, I think Davoren 
and Hazen, “Russell’s 1925 logic,” in the 
“Australasian Journal of Philosophy,” vol. 78 
(2000), pp. 534-556, is the clearest published 
account of the revised system.)  It is clear (by 
the argument from the Second Incompleteness 
Theorem) that full PA is not interpretable in 
Russell’s “second edition” system, but it seems 
***[Note to ambitious students: open problem here 
that may not be TOO difficult] POSSIBLE*** that 
the system is mathematically more powerful than 
the “first edition” system (w/o 
reducibility).  In particular, J.P. Burgess has 
shown (Notre Dame Journal of Formal Logic, vol. 
39 (1998), pp. 1-17­ as coauthor I contributed 
only minor points and had achieved much less 
impressive results) that “first edition” Russell 
gets only a small fragment of Primitive Recursive 
Arithmetic (“elementary” or Kalmar arithmetic): I 
have not been able to derive more than this in 
the “second edition” system, but it seems 
possible that it COULD be made to yield a larger 
fragment of PRA, or even full PRA.

(*)  Another non-logical assumption in “Principia 
Mathematica” is an axiom of Infinity: there are 
infinitely many individuals.  Since this is a 
separate issue from the status of Reducibility, I ignore it here.
(**) A bit more detail on the argument in the 
Burgess and Hazen article cited below.

---

Allen Hazen
Philosophy Department
University of Melbourne