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

Thu Sep 14 08:45:18 EDT 1995