The significance of the so--called judgements lies in the fact that they constitute the claims of a proof. They are the units of assertion ; they are the objects of inference. The judgements of have the form

where are distinct variables
and 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* .

Before explaining the conditions which make a
sequent true
we shall define a relation , where **H** is a hypothesis list and
**l** is a list of terms,
and we shall define what it is for a sequent to be * true at*
a list of terms.

` :,,:` if and only if

*

*
&

*
if

We can also express this relation by saying that
every is a member of

and every is type --functional in , where means the set type

The sequent

is
true at if and only if

*
(

*
&

*
)

*
if ` :,,:`

*
&

Equivalently, we can say that
**s** is **S**--functional in
if

:,,: .
The sequent

is true if and only if

*
is
true at

The connection between functionality and the truth of sequents lies in the
fact that **S** is type--functional (or **s** is **S**--functional) in
if and only if **T** is a type and
for each member **t** of **T**, **S** is type--functional (**s** is **S**--functional)
in ` { x:T| x=t in T}`.
Therefore,

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, 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 what is anticipated to be the standard mode of use,
the user tries to prove that a certain type is inhabited without
regard to the identity of any member.
One expects that in this mode the user thinks of the type
(that is to be shown inhabited) as a proposition, and 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

Also, 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. It should be noted that in the current system proofs named in the user's library cannot be proofs of sequents with hypotheses.

Thu Sep 14 08:45:18 EDT 1995