[FOM] on Bas Spitters on "constructive impredicativity?"

[Bas Spitters]

On Friday 31 March 2006 02:25, Harvey Friedman wrote:
> There is no predicative proof of Kruskal's theorem, under the classical
> Feferman/Schutte elucidation. So if you say that Veldman's proof is
> predicative, then you must be referring to some nonstandard analysis of
> predicativity. Which nonstandard form?

I hope I have cleared this up in my response to Gabriel Stolzenberg.

> I always viewed Bishop style constructivity as entirely predicative under
> the Feferman/Schutte elucidation. In fact, I always viewed Bishop style
> constructivity as living comfortably within a conservative extension of HA.

I largely agree with you, in fact, I referred to Feng Ye a couple of weeks ago 
on the FOM-list. He made this claim precise: most of Bishop and Bridges can 
be carried out in a conservative extension of  HA (even of PRA).

> Where in
> Bishop do you see any substantial logical strength beyond that of HA?

I came across two instances where Bishop seems to be "impredicative". To be 
precise, I mean where he uses the power set in an essential way.
* The Bishop-Cheng measure theory. He uses the space of all partial functions. 
This can be "fixed" in a quite straight-forward way. See eg Feng Ye.
* The completion of a uniform space. It is in ex25 on p124 of Bishop and 
Bridges. It seems that the answer Bishop has in mind is to use a construction 
similar to the completion of metirc spaces, but instead of using Cauchy 
*sequences* one would use all Cauchy *filters*. It is a priori not clear how 
to carry out such a construction in, say, a predicative type theory or set 
theory.

I am not sure what this means: Does Bishop "allow" the use of the powerset or 
was he just being careless (if I may use that word).

Bas

-- 
-------------------------------------------------------
Research Group Foundations/ Institute for Computing and Information Sciences
Radboud University Nijmegen www.cs.ru.nl/~spitters/
P.O.box 9010, NL-6500 GL Nijmegen, The Netherlands.
spitters at cs.ru.nl Ph:+31-24-3652631 F:+31-24-3652525 Room: A5024