Skip to main content
PRL Project

The Book

Implementing Mathematics with The Nuprl Proof Development System

Statements and Definitions in Nuprl

This chapter will explain how to write definitions and statements with the Nuprl system, and in doing so it will introduce a minimal set of system commands to the beginning user and explain how the type theory introduced in chapter 2 can be used to express mathematical propositions. The first four sections of the chapter concentrate on discussing the system commands and some relevant syntactic features of the Nuprl logic. The rest of the chapter describes the conceptual issues involved in using type theory as a general-purpose language for expressing mathematics. These conceptual issues are discussed via examples drawn from four areas of mathematics: logic (both constructive and classical), number theory, algebra and set theory. (Chapter 11 contains a summary of definitions and theorems from other areas of mathematics.) It is intended that this chapter be read while experimenting with the system. Throughout this chapter the typewriter font represents text that is actually used in the Nuprl system, while the $mathematical$ $f\! ont$ is used in general discussions.

Overview of the Nuprl Environment

The Nuprl system provides an interactive medium which is accessed via a screen divided into various windows3.1and a keyboard/mouse which allows communication with the system. The windows represent regions of the system with specialized roles in the interactive process; the different kinds of windows are listed in figure 3.1.

Figure 3.1: Windows Used in the Nuprl System
\item The Command Window
\item The Li...
...r\index{text editor}{} (ted)
The terminal is used to enter definitions, commands, proof steps and so forth into the appropriate window of the system. Commands that allow movement between windows and modification of the view of the environment consist of control sequences or mouse commands. In this section these features are described in as much detail as is needed for the purposes of this chapter. Chapter 7 contains a comprehensive discussion of system features.


The windows are part of Nuprl and are not part of the window mechanism that may come with the machine on which Nuprl is implemented.