[FOM] on Bas Spitters on "constructive impredicativity?"
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
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