[FOM] Primitive Recursive Pigeons
A.P. Hazen
a.hazen at philosophy.unimelb.edu.au
Sun Jul 25 05:37:05 EDT 2004
About three years ago, I remember hearing that someone had shown
that the PIGEON-HOLE PRINCIPLE, over some very basic theory, yielded
primitive recursion (and so was a sufficient supplement to the very
basic theory to bring it up to the power of PRA). Does someone have
references? or details? I've been thinking about it again in the
context of thinking about "predicative" [see "Refs" at bottom of this
post] foundations of arithmetic. Next section is a proof-sketch, then
Refs (with an explanation of why I'm interested).
---
Does the proof go like this? Suppose that, for some "vector"
of n parametric variables, v, we have an n-ary function g(v) and an
(n+2)-ary function h(x,y,v). We want to prove the existence of an
(n+1)-ary function f(x,v) defined from them by primitive recursion.
We'll define f(n,v) = y to mean that there is a finite function
f'(x,v) defined on the numbers up to and including n
<<<<<COMMENT: This assumes that our very basic system can
handle quantification over finite functions; the systems I
most interested in (see "Refs") can. They also have classical
logic and can talk about 0 and successor and less-than.>>>>>
with f'(0,v) = g(v) and f'(s(m),v), where defined, equal to
h(m,f(m,v),v).
Clearly f(0,v) is defined, and f satisfies the recursion
equations as far as it goes. What we have to prove is that f(n,v)
exists for every natural number n.
So suppose for some n that f(n,v) is not defined (i.e. there
is no appropriate f' with domain extending up to n). We know that n
must be a successor, s(m). We now define an injection (one-one
function), i, from the segment of the numbers [0,s(m)] into the
segment [0,m]:
If f(x,v) is defined, let i(x) = x,
if f(x,v) isn't, let i(x) = p(x) (the predecssor
of x).
PROOF (?) that i, so defined, is an injection: Note first that,
since f(0,v) is definitely defined, the second clause will only come
into play if there IS a predecssor, so that's o.k. The identity and
(for numbers greater than 0) predecessor functions are both one-one,
so the restrictions of i to the f(z,v)-defined and f(z,v)-undefined
parts of the segment [0,s(m)] are both one-one. The only thing that
could go wrong would be a "collision": if the first clause forced us
to set i(j)=j for some j with f(j,v) defined, AND the second clause
set i(k)=j for some k with f(k,v) undefined. But in that case j=p(k)
-- in other words, k=s(j) -- so this can't happen: since there is an
appropriate
f'(z,v) with domain ending at j, and since h is assumed to be a total
total function, there will, contrary to supposition, be an
appropriate f'(z,v) for k as well. (Just add one more ordered pair
to the f' that works for j; getting finite sets by adding single
elements to given finite sets is part of very, VERY, basic theories
of finite sets.)
But this contradicts the PIGEON-HOLE PRINCIPLE in the form
"There is no injection from a segment [0,s(n)] to the segment [0,n]."
So the primitive-recursively defined function f is total.
---
Refs: Examples of very basic theories in which it is
possible to reason about finite functions (and in which recursive
functions are defined in the way outlined) include the PDA
(=Predicative Dedekind Arithmetic) of Burgess & co-author,
"Predicative logic and formal arithmetic," NDJoFL 39 (1998), pp.
1-17, and the EFSC (Elementary theory of Finite Sets and Classes) of
Feferman & Hellman, "Predicative foundations of arithmetic,"
J.o.Philosophical Logic 24 (1995), pp. 1-17, also discussed in their
paper in G. Sher and R. Tieszen, eds., "Between Logic and Intuition:
essays in honor of Charles Parsons" (Cambridge U.P., 2000), pp.
317-338. PDA doesn't admit definition of functions by primitive
recursion in general (though it does allow definition by BOUNDED
primitive recursion); the proof sketched -- if correct -- would be in
PDA + some form of pigeon-hole. Feferman and Hellman prove that
primitive recursion is available in EFSC (and, indeed, that it
interprets full PA); the interest here would be for a version that
drops or weakens their axiom "Sep." ... My own interest is in the
"Alternative History" question, what could Russell have done if he
had had something more like Brouwer's personality and had been
willing to jettison large parts of core mathematics because of
philosophical scruples? In particular, how much mathematics would be
obtainable in "Principia Mathematica" with the Axiom of Infinity but
WITHOUT the Axiom of Reducibility?
PDA was designed as a streamlined modern version of the
system ("Ramified Type Theory") of FIRST-EDITION "Principia", so
Burgess's result (viz., Grzegorczyk Arithmetic with exponentiation
but without the higher primitive recursive functions of the
Grzegorczyk Hierarchy) is probably the answer for 1910 Russell. In
the SECOND edition, Russell proposed a stronger version of ramified
type theory (one allowing a certain number of definitions that would
have been stigmatized as "impredicative" in the logic of the first
ed.): cf. Hazen & Davoren, "Russell's 1925 logic," Australasian J. of
Philosophy 78 (2000), pp. 534-556 (or the longer version to be
published in two weeks in the proceedings volume of the 2001 "Russell
01" conference in Munich).
By the standards of either edition of PM, the primitive
recursive definition of f, and certainly the definition of the
injection i, are "impredicative". (Note that the conditions in the
definition of i refer to the definèdness of f, and so involve
quantification over natural numbers.) In either edition's logic it
is, I think, possible to prove the pigeon-hole principle for
PREDICATIVELY-DEFINED injections. The second-edition logic, however,
allows us (***I think***) to prove that ANY function with a finite
domain (and so the injection i) is co-extensive with a "predicative"
one, and so that the pigeon-hole principle (as stated above) holds in
full generality.
If all the details work, in other words, 1925 Russell could
have gotten full PRA. Which would have made a nice reply to Skolem's
1923 paper!
---
Allen Hazen
Philosophy Department
University of Melbourne
More information about the FOM
mailing list