# 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 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 windows^{3.1}and 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.

*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.