The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

AFAIK, Nuprl avoids these problems by defining only the universe of
types and their corresponding PERs recursively, but showing that this
definition is well-founded requires a surprisingly powerful fixed
point principle (at least, it surprised me).

Using Allen's method [5] one can define n universes of Nuprl in n+1 predicative universes of Coq [1, sec. 6.1].

It is just too ugly because of duplications of definitions at each level.

I think we can formalize n universes of the predicative fragment of Coq in n+1 universes of Nuprl.

If so, I don't understand why you seem to assert

that Allen's method of "defining only the universe of

types and their corresponding PERs recursively"

inherently needs a more powerful meta-theory.

In particular, if you look at Bob Harper's *Constructing Type Systems ....

(Martin Escardo and Paul Taylor tell me that Dito Pataraia showed that
this fixed point theorem also holds in intuitionistic set theory, but
to my knowledge there isn't a predicative version of it.)

I've not fully understood Bob Harper's construction, but

in [1, Fig.6], we showed how one can define all the universes of Nuprl in the first universe of Agda using induction-recursion.

Inductive-recursive [2,3] definitions are considered predicative, isn't it?

I don't know a very precise definition of predicativity, but I don't see any circularity in inductive-recursive definitions.

(the quote below is from the top of the original email.)

If you try to formulate the typing rules in the obvious way --- by
giving mutually-recursive judgements for context well-formedness, type
and term well-formedness, and equality --- then the definition of the
type system is clearly structural. However, you will not be able to do
induction on derivations to prove that weakening is sound, which in
turn prevents you from being able to show the soundness of
substitution in any easy way.

In the "obvious" way mentioned in the above quote,

I'm curious how powerful meta-theory is required to prove some of the

desired meta-theoretic properties like consistency, type preservation e.t.c. ?

In any case, I want to understand this method better. Is there a reference I can read?

Thanks,

Abhishek

[1] Anand, A., and Rahli, V. . Towards a Formally Verified Proof Assistant. ITP 2014 

http://www.nuprl.org/documents/Anand/TowardsAFormallyVerifiedProofAssistant.pdf

[2] Dybjer, P. (2000). A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. J. Symb. Log. 65, 525–549.

[3] Dybjer, P., and Setzer, A. (1999). A finite axiomatization of inductive-recursive definitions. In Typed Lambda Calculi and Applications, (Springer), pp. 129–146.

[4] http://sneezy.cs.nott.ac.uk/epilogue/?p=1098

[5] Allen, S.F. (1987). A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis. Cornell University.  http://www.cs.cornell.edu/Info/Projects/NuPRL/documents/allen/NonTypeTheoreticSemantics.ps