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

Gabriel Stolzenberg gstolzen at math.bu.edu
Thu Mar 30 14:43:47 EST 2006

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?
> For some time already Coq is based on the calculus of inductive
> constructions (by Coquand and Paulin).

   I'm aware of the pun.  I like Huet's sense of humor.
> > Also, how does the shift to predicativity effect type checking?
> It is still decidable, if that was your question.

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

   Thanks for the information.


More information about the FOM mailing list