[FOM] Primitive Recursive Pigeons

[A.P. Hazen]

    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