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

[Bas Spitters]

On Thursday 30 March 2006 21:43, Gabriel Stolzenberg wrote:
> On Thu, 30 Mar 2006, Bas Spitters wrote:
> > There is now also an intuitionistic version, i.e. provable in
> > Kleene-Vesley's FIM, by Veldman.
> >
> > (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.
>
>    As I recall, part of the story was that Harvey had proved that
> every proof of Kruskal's theorem requires impredicativity.  Obviously,
> I must be mistaken about this.  Is there some other result with which
> I may be confusing this?

There seem to be two issues here, Harvey can correct me if I am wrong. 
1. Veldman proved, intuitionistically, Kruskal's theorem (as in the `theorem 
proved by Kruskal'). Harvey showed that an extension of this theorem with a 
`gap condition' cannot be proved in a predicative system (in the sense of 
Feferman-Schutte).
I have the impression that Coquand indeed gave a constructive "impredicative" 
proof of the extended theorem, which can be carried out in a theory with 
enough inductive definitions.
2. "Predicativity" as used by Feferman-Schutte refers to a level of 
proof-theoretic strength. By type theorists the term is used for a kind of 
"non-circularity in definitions", as it was used originally by Russell. 
Martin-Löf's type theory  with enough inductive definitions is 
"impredicative" according to Feferman. In this sense one can say that there 
is a "predicative" (ie non-circular) proof of the extended Kruskal theorem.
(I was reminded of this offline by Jesper Carlström. In my opinion this was 
not the source of confusion, but it is good to state in any case. I wonder 
how this is connected to Weaver's definition of "predicative".)

>    Actually, I was thinking about efficiency.  I had the, possibly
> mistaken, impression that the use of impredicativity helped make
> for efficient type checking.

I have never heard this before, but that doesn't mean that it is not true.
In any case, the type checking of (the predicative) Coq is efficient, many 
people use it each day.

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