To accommodate the top--down style of the Nuprl system the rules of the logic are presented in the following refinement style.
H >> T ext t by rule
*
>> 
ext 
*
*
>> 
ext 
The goal is shown at the top, and each subgoal is shown indented underneath. The rules are defined so that if every subgoal is true then one can show the truth of the goal, where the truth of a judgement is to be understood as defined in section 8.1. If there are no subgoals (k=0) then the truth of the goal is axiomatic.
One of the features of the proof editor is that the extraction terms are not displayed and indeed are not immediately available. The idea is that one can judge a term T to be a type and T to be inhabited without explicitly presenting the inhabiting object. When one is viewing T as a proposition this is convenient, as a proposition is true if it is inhabited. If T is being viewed as a specification this allows one to implicitly build a program which is guaranteed to be correct for the specification. The extraction term for a goal is built as a function of the extraction terms of the subgoals and thus in general cannot be built until each of the subgoals have been proved. If one has a specific term, t, in mind as the inhabiting object and wants it displayed, one can use the explicit intro rule and then show that the type t in T is inhabited. The rules have the property that each subgoal can be constructed from the information in the rule and from the goal, exclusive of the extraction term. As a result some of the more complicated rules require certain terms as parameters.
Implicit in showing a judgement to be true is showing that the conclusion of
the judgement is in fact a type.
We cannot directly judge a term to be a type; rather, we show that it
inhabits a universe.
An examination of the semantic definition will reveal that this is
sufficient for our purposes.
Due to the rich type structure of the system it is not possible in general
to decide algorithmically if a given term denotes an element of a universe,
so this is something which will require proof.
The logic has been arranged so the proof that the conclusion of a goal
is a type can be conducted simultaneously with the proof that the type is
inhabited.
In many cases this causes no great overhead,
but some rules have subgoals whose only purpose is to establish that the
goal is a type, that is, that it is well--formed .
These subgoals all have the form H >> T in 
and are referred
to as well--formedness subgoals.