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

[Gabriel Stolzenberg]

   Here I make a brief response to Bas Spitters' reply to my message,
"constructive impredicativity?"

> On Monday 27 March 2006, Gabriel Stolzenberg wrote:
>
> > That was then.  Now, I am very comfortable with impredicative
> > definitions.  In fact, I think some of them are marvelous.
>
> Which ones do you have in mind?

   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.)

>
> My impression is that such a (constructive) impredicative definitions is
> usually an invitation to find an inductive definition. This inductive
> definition is usually easier to understand (for me).

   Agreed.

> 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?  Also, how does the
shift to predicativity effect type checking?

   Gabriel