[FOM] on Bas Spitters on "constructive impredicativity?"
spitters at cs.ru.nl
Fri Mar 31 07:31:15 EST 2006
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
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).
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
More information about the FOM