** Next:** Expressions Formed by
**Up:** Syntactic Issues
** Previous:** Syntactic Issues

In Nuprl
all theorems consist of goal statements, where a goal statement is
similar to sequents used in natural deduction style inference systems. The
form of a goal statement is ` `**H** >> **T**, where **H** is a hypothesis list and **T **
is a formula in the Nuprl
logic. The symbols ` >>` separate the
hypotheses from the conclusion
and thus correspond to the symbol
used in logic. Top--level goals must have empty hypothesis lists; this
prevents the user from introducing inconsistent hypotheses.
Theorems also cannot contain free variables; in the terminology of
chapter 2, this means that all top--level goals must contain closed terms to the right of the
` >>` symbol.

*Richard Eaton *

Thu Sep 14 08:45:18 EDT 1995