[FOM] foundations of the pigeonhole principle

[Robert Tragesser]

Speculating that the considerations in the neighborhood of Simpson 
SUBSYTEMS OF SECOND ORDER ARITHMETIC p.72, II.3 Primitive Recursion, 
especially Lemma II.3.7) provide the means to a foundations of the 
pigeonhole principle, I am finding some questions that are hard for me 
to answer...

There are such a number of ways of formalizing the pigeonhole 
principle. I'm inclined to view it as a fundamental principle.

Or is it best to view it as a special case of a more general principle? 
  Does it suffice to formulate it for natural numbers (sets of natural 
numbers)
?
Maybe it is conceptually/foundationally best to think of it as 
characterizing finite sets (not necessarily finite sets of natural 
numbers)?  In that case, wouldn't formulating the pigeonhole principle 
for sets of natural numbers make it too easy, because it's too easy to 
say what a finite set of natural numbers is?  I suppose we'd have to be 
convinced that the very idea of a finite set is founded on the idea of 
a finite set of natural numbers (as I am, but should I be)?

Allowing that it's foundationally sound/adequate to say that it 
suffices to formulate the pigeonhole principle over natural numbers, is 
it right to say that it is equivalent to (the proposition in Simpson 
Lemma II.3.7... but not restricting phi to Sigma1,2):   "Either there 
exists a finite set X such that (n)(n el X iff phi(n)), or there exists 
a 1-1 function f from N to N such that every n such that phi(n) is the 
image under f of an m of N).  Then the foundations of the pigeonhole 
principle are relativized to conditions of phi ?


Robert Tragesser

845-358-4515 (Ph)
26 DePew Avenue #1
Nyack, NY 10960-3839