[FOM] An intuitionistic query

[rgheck]

On 09/17/2009 08:57 AM, Arnold Neumaier wrote:
> 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.
>
>    
This would not be surprising. I meant only to be commenting upon the 
generalization of the standard version, involving mappings onto initial 
segments of N.

> 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).
>
>    
You don't even need to generalize it. That alone fails.

Here's the proof, which reveals what is going on. Let a,b <> 0 be such 
that it is undecided if a=b. We shall exhibit a map from {a,b,0} to 
{a,b} such that it is not provable that (Ex)(Ey)(fx = fy & x<>y). Here 
is the map: f0 = b, fa = a, fb = a. This is a function, since, even if 
a=b, fa = fb. One can easily see that, if a=b, then x,y can be 0,a; if 
a<>b, then x,y can be a,b. But we do not know which case holds, and so 
we cannot produce the x,y in question.

Note that this reasoning does show that, under the hypotheses, 
~~(Ex)(Ey)(fx = fy & x<>y).

Note also that it is critical that the identity of items in the range is 
undecided. That is why the version involving maps onto segments of N is OK.

Richard