Completeness

The terms, evaluation fragments, and rules for type membership are intended to formalize Naive Type Theory. The display notation and the informal semantics we have given suggest the connections between formal and informal accounts. I want to just mention some of the highlights by referring to the presentation in section 2.

Primitive Types

Nuprl has void for the empty type and takes the integers, int, as primitive. But N can be defined inductively or as a subset of int, e. g.

$$N=\{z:{\sf int} \vert 0\leq z\}$$

Compound Types

The display forms indicate the correspondence between the type constructors and Nuprl terms, for example the Cartesian product, $A \times B$, is product(A; B). The tags for discriminated unions are formalized as inr(b), inl(a). The informal function notation, $x\mapsto b$ is formalized as $\lambda$(x.b) of course.

The inductive type $\mu x.F(x)$ is formalized as rec(x.F(x)), and the recursor, $\mu\!-\!ind(a; f, z.b)$ is rec_ind(a; f, z.b).

Universes

The formal type theory must make some distinctions not seen in the naive version. In order for types to be values, they need to belong to a type. We might try adding a single new type, say Type, for this purpose. But then it must belong to a type. We might try attaining closure by postulating. $Type\in Type$.

But this causes many troubles. It allows us to inhabit every type [21] and permits non-terminating functions in the function spaces [28]. So following the traditions of predicative type theory [45,34,19,20], we introduce a hierarchy of types. Following [35] we call them universes. They are denoted ${\sf U_1, U_2, \ldots}$, and we have that

$${\sf U_i\in U_{i+1}}$$

Logic is introduced into type theory by taking propositions-as-types. This is well explained elsewhere, e. g. [12,13,17,23,34,35]. According to this principle,

$${\sf Prop_i=U_i.}$$