In Nuprl's type theory, types are grouped together into universes
.
Types built from the base types such as 
or Atom
using the various type constructors are in universe 
.
The subscript 1 is the level of the universe. Types built from
universe terms with level at most i, are in universe
. Universe membership is cumulative; each universe
also includes all the types in lower universes.
Since propositions are encoded as types, propositions reside in
universes too. In keeping with the propositions-as-types encoding
, we
define a family of propositional universe abstractions
, which unfold to the
corresponding primitive type universe terms 
.
If one is only allowed to use constant levels for universes, one often has to choose arbitrarily levels for theorems. One would then find that one needed theorems which were stated at a higher level, and would have to reprove those theorems. This was the case in Nuprl V3.
Nuprl V4 allows one to prove theorems which are implicitly quantified over universe levels. Quantification is achieved by parameterizing universe terms by level expressions rather than natural number constants. The syntax of level expressions is given by the grammar:
The v are level-expression variables. v can be any alphanumeric
string
. These variables are implicitly quantified over all positive
integer levels. the k are level expression constants. k can be
any positive integer. The i are level expression increments
. i can
be any non-negative integer. The expression 
is interpreted as
standing for levels L + i. 
is an abbreviation for 
.
The expression 
is
interpreted as being the maximum of expressions 
.
Usually when stating theorems, only level expressions of the form v
and 
need be used. Other expressions get automatically created
by tactics. Further, it is normally sufficient to use a single level-expression
variable throughout a theorem statement. For example, we normally prove
the theorem:
rather than
