Proofs in Nuprl are trees. The nodes of the tree consist of sequents and justifications. A sequent is a list of
formulas, called hypotheses, paired with a single formula called the
goal. The hypotheses are numbered .
These sequents, also called goals, are displayed as
The symbol, , called a turnstile, separates hypotheses
from conclusions. A sequent is provable iff we can prove the
goal G from the hypotheses
.
The justification component of a node gives a reason that the goal sequent follows from the subgoal sequents generated by the justification. Justifications are displayed as by justification text.
A sequent, its justification, and subgoals constitute an individual
inference in the proofs. Here is a schematic example:
no subgoals no subgoals
In general an inference can look like
where the
are lists of formulas and
are single formulas.
Nuprl provides various tree traversal operations to facilitate
``reading'' a proof tree and modifying it. These proof trees are
meant to be read with these tree walking operations. But we also want
to print the trees. There are various schemes for doing this. We write
vertical lines in the left margin to connect a subtree to its present
goal. Here is how the first example would be printed.
1.
2.
1.
2.