next up previous contents index
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