[FOM] induction and reducibility
Allen Hazen
allenph at unimelb.edu.au
Sun Oct 28 15:13:47 EDT 2007
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
More information about the FOM
mailing list