We write a sequent as
where C is the conclusion of the sequent, and , the ith hypothesis
is either an assumption 
or a type declaration
, and 
. A type declaration 
is considered to bind
free occurrences
of x in terms to the right;
that is in 
and C. Sometimes we refer
collectively to the hypotheses and the conclusion of the sequent as
sequent clauses
or just clauses
. In the older Nuprl
\
literature, >> instead of the turnstile symbol 
is used
to seperate the hypothesis list from the conclusion. The word
goal
is sometimes used either to refer to a whole sequent or to just
the conclusion. Which should be clear from context.
Usually Nuprl displays sequents vertically and explicitly numbers the
hypotheses, so the sequent 
is displayed as:
A sequent can be considered as either a conjecture or a proved truth. As a conjecture one understands the sequent as expressing the as yet unproved conjecture that the conclusion of the sequent is deducible from the assumptions and declarations of the sequent. As a proved truth , one understands the sequent as expressing that that conclusion of the sequent has been proved true, given the assumptions and declarations of the sequent.
There are a few details left out of the above account that we now describe.
Logic is encoded into Nuprl's type theory using the propositions-as-types analogy, so all clauses of sequents are really types. Clauses are made to appear like propositions by using abstractions. All hypotheses declare variables , but the system currently hides the display of any variable whose name starts with a % character. We sometimes refer to such variables invisible variables . When sketching sequents in this document, we suppress variables that would normally be invisible.
.