[FOM] on Bas Spitters on "constructive impredicativity?"
spitters at cs.ru.nl
Fri Mar 31 04:00:01 EST 2006
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
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.
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
More information about the FOM