The discussion so far has focused on the mechanics of using Nuprl . The rest of this chapter will concentrate on the conceptual issues that arise when one uses Nuprl to express formal mathematics. The discussion will continue to make reference to the mechanics of using Nuprl so that interested readers can take the opportunity to experiment with the system while familiarizing themselves with the logic of Nuprl . No attempt will be made to discuss proof techniques in this chapter; these will be covered in chapter 4.
All theorems in Nuprl have the form `` >> term'', where
>>
separates assumptions from the goal.
One can read >>int in U1 as ``prove that type int is in 
from no assumptions.''
In the next chapter we will see how various rules generate assumptions.
The most important aspect of the Nuprl system is the constructive nature of the type theory that underlies the system. A beginner should therefore be careful to make certain that the theorems being expressed are indeed constructively true. Even if a particular theorem is constructively true, the reader should remember that the proof will involve carrying out the actual constructions needed to exhibit the truth of the theorem. Thus several classically trivial theorems (or axioms) become relatively difficult. The benefit of the constructive viewpoint, of course, is that the resulting proofs become computationally significant. The heart of the constructive interpretation is contained in the propositions--as--types principle, which is discussed later in this section. It should be noted here that the constructive nature of the Nuprl type system in no way inhibits the possibility of modeling classical logic, and in fact we do so in the next section. The use of a constructive type theory for the Nuprl system is in sharp contrast to other systems for theory development, notably the LCF system.