[POPLmark] Re: Meta-comment

[Randy Pollack]

Bob Harper writes:

| As to the issue of "trust", I am astonished that there could be any
| question here at all.  To believe in the consistency of, say, Coq or HOL
| is an enormous step that requires you to accept strong comprehension
| principles and that admits no simple inductive characterization to
| justify them semantically.

I'm not sure this point is terribly relevant to the poplmark
challenge, but I'm interested in it.  HOL requires impredicativity
(and also definite descriptions) to be useful, which I guess is what
Bob is referring to.  But dependent type theory does not require
impredicativity.  Most of what is done in Coq (in practice) could be
done predicatively.  E.g. I guess Jerome's de Bruijn poplmark solution
could be formalised in Martin-Lof type theory with inductive
definitions and a few universes.

What is the relative strength of Twelf vs Martin-Lof type theory with
inductive definitions and a few universes?

Randy