[FOM] An intuitionistic query

[Arnold Neumaier]

rgheck wrote:
> On 09/09/2009 10:12 AM, Arnold Neumaier wrote:

>> (*) is a special case of Dirichlet's pigeonhole principle.
>> Are there versions of the latter that are intuitionistically
>> undecidable? I found an infinite version in
>>      https://eprints.kfupm.edu.sa/60600/1/60600.pdf ,
>> but I am looking for a finite version.
>>    
> Each of the finite versions is certainly going to be provable by a 
> version of the argument you gave, and the uniformity of those arguments 
> is good intuitionistic reason to think the generalization holds. I.e, 
> the obvious argument by induction should work.

I am not so certain. I looked more deeply into the literature and
found that it apparently depends on the way the pigeonhole principle
is formulated.

For example, according to Theorem 4 in http://arxiv.org/pdf/math/9405204
the principle appears to be intuitionistically invalid when written in
a form generalizing
    (***) For every mapping f from {a,b,c} to {d,e},
    there are distinct x, y with  f(x)=f(y). 




Arnold Neumaier