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

[Bas Spitters]

On Wednesday 29 March 2006 07:07, Gabriel Stolzenberg wrote:
>    It's been over 15 years since I looked at them but, if I remember
> correctly, e.g., in Thierry Coquand's proof of Kruskal's theorem.
> (I'm talking about a version that I'm pretty sure he didn't publish.)

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.

> > ALF (or agda/alfa as it is now called) is predicative. Coq used to be
> > impredicative (based on Coquand/Huet's calculus of constructions), but
> > recently (v8.0) they changed the type system so that it is predicative.
> > (Well, the computational part of the system is predicative. The issue
> > is too technical to go into here.) Their motivation, as I understand
> > it was that the impredicative definitions were just too difficult to
> > understand for most users. They were contradicting set-theoretical
> > intuitions.
>
>    That's very interesting.  The impredicativity seemed so elegant.
> How do they now introduce the logcial constants?  

For some time already Coq is based on the calculus of inductive constructions 
(by Coquand and Paulin). In the presence of inductive definitions the logical 
constants, i.e. "exists", "or", "and" can be defined ... inductively.
The definitions are very close to the previous impredicative definitions (the 
smallest ... such that ...). The constants forall and -> are basic parts of 
the calculus, using props-as-types.

> Also, how does the 
> shift to predicativity effect type checking?

It is still decidable, if that was your question.

Bas