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

[Harvey Friedman]

On 3/30/06 1:26 PM, "Bas Spitters" <spitters at cs.ru.nl> wrote:

> There is now also an intuitionistic version, i.e. provable in Kleene-Vesley's
> FIM, by Veldman. 
> 
> http://webdoc.ubn.kun.nl/mono/v/veldman_w/intuprofk.ps
> (or Wim Veldman: An intuitionistic proof of Kruskal's theorem. Arch. Math.
> Log. 43(2): 215-264 (2004))
> This result was elicited by Coquand's result. Veldman's proof is predicative
> and can be translated into a Bishop-style constructive proof. There are many
> nice constructive results in this area (like the ones connected to open
> induction) that I do not want to go into now.

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 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,
and so once again Kruskal's theorem cannot be proved there either. Where in
Bishop do you see any substantial logical strength beyond that of HA?

Harvey Friedman