One of the atomic types available in Nuprl
is the type integer, called
` int`.
The availability of integers as an atomic type allows one to express a
great deal of
elementary number theory without
much effort. The type ` int` comes equipped with an
* induction form*
so that one can inductively define functions from integers to integers. In
this section we illustrate how some number--theoretic predicates and functions
can be defined in Nuprl
and how number--theoretic theorems are stated.

We begin this section with an example of a simple theorem which will be proved
in chapter 4; we use this theorem to review how one enters theorems in the
system. The theorem asserts that for every pair of integers one can
find an integer whose value is 0 if the first of the original pair of
integers is less than the second and whose value is 1 if the first of the
original pair of integers is not less that the second. In this statement
there are a pair of quantifiers; the first is universal and the second is
existential. Accordingly we need the definitions for universal quantifiers
and existential quantifiers from figure . To state the theorm
in Nuprl
, one would first
create a name and place for the theorem using the commands discussed in
section 3.2. Then the theorem would be viewed and finally the text editor
would be invoked by clicking R on the mouse in ` <main proof goal>`.
Once in the text editor the first symbols typed would be ` >>`; after
this the text of the theorem can be typed. At this stage the definition
` all2` is needed. We use it by first typing
; this will put
the cursor in the command window with the ` I>` prompt. Now one
types ` all2` followed by a carriage return. The definition will be
instantiated in the text editor. The appearance of the definition template
will be ` all <var>,<var>:<type>.<prop>`. The variables ` x`
and ` y` can now
be entered as the first two parameters, and ` int` can be entered as the
third parameter. The body of this universally quantified statement is
an existentially quantified statement. The last parameter, ` <prop>`, in
the definition is instantiated by invoking the definition for ` some`.
The first two arguments of this quantifier can be filled in as before.
The body of the inner quantified statement is a conjunction of the two
conditions appearing in the statement of the theorem and can be expressed
using the built--in relation ` <` between integers and the definitions for
conjunction and negation. The final appearance of the theorem is as follows.

>>all x,y:int. some z:int. (x<y => z=0) & (~x<y => z= 1)This is a theorem whose proof will embody some computational content; the existence proof will involve a procedure which computes

The following definitions suggest
what some standard number theory looks like in Nuprl
.
We first define the predicate * divides* using
the (built--in) mod function.

divides(<n>:int,<m>:int) == ( <m> mod <n> = 0 in int)The next definition defines the predicate

prime(<n:int>) == (1 < <n>) & all k:int. ( (0 < k) & (<n> mod k = 0 in int) ) => (k=1 in int) | (k=<n> in int)Now these number--theoretic predicates can be used in conjunction with the logic definitions to state theorems in number theory in the following fashion.

>> all n:int. prime(n) | ~prime(n) >> all n:int. some p:int. n<p & prime(p)In stating number--theoretic propositions we come across our first examples of Nuprl theorems that have manifestly interesting computational content. The Nuprl system can extract the procedure from the proof. If we call the theorem

\n.(term_of(t)(n))is a function which takes a natural number to a prime which is greater than it, where the function

Another interesting theorem one can state in Nuprl is the remainder theorem :

>>all x:int. all y: int. some q:int. some r:int. (y = (q*x + r) in int) & (0 <= r < x).We assume that the term

Thu Sep 14 08:45:18 EDT 1995