This section is included for technical completeness; the beginning reader
may wish to skip this section on a first reading.
Here we shall consider only briefly the
semantics.
The complete introduction appears in section 
.
The semantics of
are given in terms of a system of computation
and in terms of criteria for something being a type,
for equality of types,
for something being a member of a given type
and for equality between members in a given type.
The basic objects of are called terms. They are built using variables and operators, some of which bind variables in the usual sense. Each occurrence of a variable in a term is either free or bound. Examples of free and bound variables from other contexts are:
, 
)
are the binding operators. In 
the two occurrences of x are bound, and the occurrence
of y is free.
the occurrence of y is free, the first occurrence of x is free, and
the other two occurrences are bound.
function Q(y:integer):integer;all occurrences of x and y are bound, but in the declaration of P x is bound and y is free.
function P(x:integer):integer; begin P:=x+y end ;
begin Q:=P(y) end ;
By a closed term we mean a term in which no variables are free. Central to the definitions of computation in the system is a procedure for evaluating closed terms. For some terms this procedure will not halt, and for some it will halt without specifying a result. When evaluation of a term does specify a result, this value will be a closed term called a canonical term. Each closed term is either canonical or noncanonical, and each canonical term has itself as value.
Certain closed terms are designated as types; we may write ``T type''
to mean that T is a type.
Types always evaluate to canonical types.
Each type may have associated with it closed terms
which are called its members; we may write ``
'' to mean
that t is a member of T.
The members of a type are the (closed) terms that have as values the
canonical members of the type, so it is enough when specifiying the
membership of a type to specify its canonical members.
Also associated with each type is an equivalence relation on its
members called the equality in (or on) that type;
we write ``
'' to mean that t and s are members of T
which satisfy equality in T.
Members of a type are equal (in that type) if and only if their values
are equal (in that type).
There is also an equivalence relation T = S on types called type equality. Two types are equal if and only if they evaluate to equal types. Although equal types have the same membership and equality, in some unequal types also have the same membership and equality.
We shall want to have simultaneous substitution of terms, perhaps containing free variables, for free variables. The result of such a substitution is indicated thus:
where,
, 
are variables,
and 
are the terms substituted for them in t.
What follows describes inductively the type terms in Nuprl
and their
canonical members. We use typewriter font to signify actual
Nuprl
syntax.
The integers are the canonical members of the type int.
There are denumerably many atom constants (written as character strings
enclosed in quotes) which are the canonical members of the type atom.
The type void is empty. The type A|B is a disjoint union
of types A and B.
The terms inl(a) and inr(b) are canonical members of
A|B so long as
and 
. (The operator names inl and inr
are mnemonic for ``inject left'' and ``inject
right'' .)
The canonical members of the cartesian
product type A#B are the terms
<a,b> with 
and 
.
If x:A#B is a type then A is closed (all types are closed)
and only x is free in B.
The canonical members of a type x:A#B (``dependent product'')
are the terms <a,b> with 
and 
.
Note that the type from which the
second component is selected may depend on the first component.
The occurrences of x in B
become bound in x:A#B.
Any free variables of A, however, remain free in x:A#B.
The x in front of the colon is also bound, and indeed it is this position
in the term which determines which variable in B becomes bound.
The canonical members of the type A list represent lists of members of A.
The empty list is represented by nil,
while a nonempty list with head a and tail
b is
represented by a.b,
where b evaluates to a member of the type A list.
A term of the form t(a) is called an application
of t to a, and a is called its argument.
The members of type
A->B are called functions, and each
canonical member is a lambda term, \ x.b,
whose application to any member of A is a member of B.
The canonical members of a type x:A->B,
also called functions, are lambda terms
whose applications to any member a of A are members of 
.
In the term x:A->B the occurrences of x free in B become
bound, as does the x in front of the colon.
For these function types it is required that applications of a
member to equal members of A be equal in the appropriate type.
The significance of some constructors derives from the representation
of propositions as types, where the
proposition represented by a type is true if and only if the type
is inhabited.
The term a<b is a type if a and b are
members of int , and it is inhabited
if and only if the value of a is less than the value of b.
The term (a=b in A) is a type if a and b are members of A,
and it is inhabited if and only if 
.
The term (a=a in A) is also written (a in A);
this term is a type and is inhabited if and only if 
.
Types of form {A|B} or {x:A|B} are called set types.
The set constructor provides a
device for specifying subtypes; for example, {x:int|0<x} has just
the positive integers as canonical members.
The type {A|B} is inhabited if and only
if the types A and B are,
and if it is inhabited it has the same membership as A.
The members of a type {x:A|B} are the
members a of A such that 
is inhabited.
In {x:A|B}, the x before the colon and the free x's of B
become bound.
Terms of the form A//B and (x,y):A//B are
called quotient types.
A//B is a type only if B is inhabited, in which
case 
exactly when a and 
are members of A.
Now consider (x,y):A//B.
This term denotes a type exactly when A is a type,
is a type for a and 
in A,
and the relation 
is an equivalence relation
over A in a and 
.
If (x,y):A//B is a type then its members are the members of A;
the difference between this type and A only arises in the
equality between elements. Briefly, 
if and
only if a and 
are members of A and 
is inhabited. In (x,y):A//B the x and y before the colon and the free occurrences of x and y in B become bound.
Now consider equality on the types already discussed.
Members of int are equal
(in int) if and only if they have the same value. The same goes for type atom.
Canonical members of A|B, A#B,
x:A#B and A list are
equal if and only if they have the same outermost operator and their
corresponding immediate subterms are equal (in the corresponding types).
Members of A->B or x:A->B are equal if and only if
their applications to any member a of A are equal in 
.
The types a<b and (a=b in A) have
at most one canonical member, namely axiom, so equality is trivial.
Equality in {x:A|B} is just the
restriction of equality in A to {x:A|B}, as is the equality
for {A|B}.
Now consider the so--called universes, Uk (k positive). The members of Uk are types. The universes are cumulative; that is, if j is less than k then membership and equality in Uj are just restrictions of membership and equality in Uk. Uk is closed under all the type--forming operations except formation of Ui for i greater than or equal to k. Equality in Uk is the restriction of type equality to members of Uk.
With the type theory in hand we now turn to the Nuprl proof theory. The assertions that one tries to prove in the system are called judgements. They have the form
where,
are distinct variables
and 
and s are terms (n may be 0),
every free variable of 
is one of 
,
and every free variable of S or of s is one of 
.
The list
is called the
hypothesis list or assumption list, each 
:
is called a declaration
(of 
), each 
is called a hypothesis or assumption,
S is called the consequent or conclusion,
s the extract term (the reason will be seen later),
and the whole thing is called a sequent.
The criterion for a judgement being true
is to be found in the complete introduction to
the semantics.
Here we shall say a judgement
is almost true if and only if
*
*
if
That is, a sequent like the one above is almost true
exactly when substituting terms 
of type 
(where 
and 
may depend on 
and 
for j<i) for the
corrseponding free variables in s and S results in a true
membership relation between s and S.
It is not always necessary to declare a variable with every hypothesis in a hypothesis list. If a declared variable does not occur free in the conclusion, the extract term or any hypothesis, then the variable (and the colon following it) may be omitted.
In
it is not possible for the user to enter a complete
sequent directly; the extract term must be omitted.
In fact, a sequent is never displayed with its extract term.
The system has been designed so that upon completion of a proof,
the system automatically provides, or extracts, the extract term.
This is because in the standard mode of use
the user tries to prove that a certain type is inhabited without
regard to the identity of any member.
In this mode the user thinks of the type
(that is to be shown inhabited) as a proposition and assumes that it
is merely the truth of this proposition that the user wants to show.
When one does wish to show explicitly that 
or that 
,
one instead shows the type (a = b in A)
or the type (a in A) to be inhabited.
The system can often extract a term from an incomplete proof when the extraction is independent of the extract terms of any unproven claims within the proof body. Of course, such unproven claims may still contribute to the truth of the proof's main claim. For example, it is possible to provide an incomplete proof of the untrue sequent >> 1<1 [ext axiom], the extract term axiom being provided automatically.
Although the term extracted from a proof of a sequent is not displayed in the sequent, the term is accessible by other means through the name assigned to the proof in the user's library. In the current system proofs named in the user's library cannot be proofs of sequents with hypotheses.