 ...Logic,

is version ``nu'' of our Proof Refinement Logics. Earlier
versions were ``micro'' and ``lambda'' [
Staff 83].
 ...space.
 In the discussion which follows we will use typewriter font
to signify actual Nuprl
text and mathematical font for metavariables.
 ...[#ML##1#].
 This is one result of a joint Cornell/Edinburgh study of programming logics
and automated reasoning begun in
198182 and continuing with joint studies of type theory and polymorphism.
 ...type.''
 Actually 97#97 reads as ``A is a type
in universe 98#98.''
We discuss universes later.
 ...expression.
 In full Nuprl
the distinction between types and other objects is
dropped.
 ...devices.
 In Nuprl
the goal 117#117
would
be expressed initially as 118#118.
A rule of introduction would then create the context 119#119.
 ...true.
 A better term to use here might be the token ``yes'',
which can be thought of as a summary of the proof.
The term axiom suggests that the facts are somehow
basic or atomic, but in fact they may require
considerable work to prove.
 ...h.
 In chapter 12 we introduce a concept of partial function
that will allow us to define 346#346 such that
347#347 using an unbounded search. The search is
guaranteed to terminate because of the information about f.
 ...semantics.

Section , page .
 ...inhabited.

Recall that the term (a = b in A)
is a type whenever 416#416 and 417#417 and is inhabited just when
418#418.
As a special case the term (a in A), which is
shorthand for (a = a in A), is a type and is inhabited
just when 419#419.
 ...windows
 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.
 ...system.
 Other commands needed for proving
theorems, evaluating terms, etc., will be discussed in later chapters.
 ...number.
 The keyword scroll can be abbreviated by scr.
 ...follows.
 The keyword create can be
abbreviated by cr.
 ...name.
 The keyword view can be abbreviated by v.
 ...#afterthm#2189>.
 The new
window is dependent on the
first window, so the first window cannot be
deleted until the text editor window is closed.
The first window can, however, be moved off the screen by using the
windowmoving commands. Thus windows can be temporarily hidden.
 ...turnstile,
 The notation >> is used instead of the more usual
turnstile 437#437 since the former is available
on most
terminals.
 ...clicked.
 Actually one can select the endpoints in
either order.
 ....
 One must not be in mouse mode
while doing this.
 ...are
 Other type constructors are being actively investigated. Some
of these will be discussed in chapter 12.
 ...assumptions.''

Although >> must be present in every theorem,
the system does not generate
it because we want to allow the possibility of stating theorems with
hypotheses, theorems such as x in int >> x+1 in int.
 ...void,

This is not a mathematical fact but a fact about Nuprl
, so we would not
expect
to be able to prove in Nuprl a theorem of the form ``if A is an atomic type,
then
A = atom or A = void''.
 ....
 The notation 461#461 is used in general
discussion about the logic of Nuprl
, whereas the notation Ui is
used in discussing text used by Nuprl
.
 ...proofs.
 The proofs we
are referring to in this discussion are not formal Nuprl
proofs but
abstract proofs.
 ...explicitly.
 Every object can be
constructed in two ways, either explicitly as in the example above or
implicitly.
Every proof
builds an object implicitly. We will see in chapter 4 how to
prove implicitly that the integers are an object in 468#468.
 ...#cldefs#2462>

It is important to enclose the right side of the definition in
parentheses to guarantee proper precedence and scope.
Also, it is important not to include a carriage return in the definition.
The carriage return will sometimes be read as a bad character when parsing
the right side, but it will not be visible on the screen.
 ...not.
 We will see other definitions later which will take account of
the structure of A.
 ...``or''.
 The usual sign for classical or is 498#498, which abbreviates the Latin
vel, meaning or.
We have chosen not to use the word ``or'' at all among the logical operators
because it has so many meanings in natural language.
 ...definition.
 If the symbol < is being used in a definition to mean
``less than'' then it
must be preceded by a backslash; otherwise, the system will try to interpret
it as the start of a new parameter.
 ...definition:
 The space after the ``514#514''
in the definition is to prevent the parser from thinking that the
following < is being quoted.
 ...of
 The definitions
of the logical connectives, which were presented in the preceding
chapter, are used here.
 ...mouse.
 In general, any action involving the
cursor and SEL
key can also can be done using the mouse pointer and
a leftclick.
 ...type
 Recall
that we think of the proof tree as lying on its side.
 ....
 It might seem
natural to be more general and say that P and Q belong to any
549#549
whatsoever. This is something that we will be able to do in Nuprl
shortly, but we do not want to discuss such matters at this point.
 ...them.
 Soon the system will
allow the user to suppress the display of any hypotheses he
is not interested in.
 ...evaluate
 Evaluation in Nuprl
will be discussed in
the next chapter.
 ...term
 A closed term is a term containing no
free variables.
 ...redex.
 This corresponds
to head reductions, normal order evaluation or call byname parameter
passing semantics.
 ...strategy.
 One might
complain that for certain terms this strategy would cause more work
than necessary to be performed.
For instance, consider the term (587#587
x.(x+x))(t), where t is very
expensive to evaluate.
Under the strategy described above, the value of t would be computed twice.
As the language we are dealing with is functional we know that this
is unnecessary, and
under the actual implementation of the evaluator it would in fact
be evaluated only once.
In general, for any substitution 588#588 in the rules above,
589#589 will be evaluated at most once and will be evaluated only if there is
a free occurrence of x in t.
 ...term.
 The
evaluator will try to reduce this term and in doing so will run until
something intervenes, such as exhausting available memory.
 ...proof.
 A
tactic may fail to produce any proof at all, but it will not produce
an invalid proof.
 ...}
 If the cursor is within an edit window COMMAND
must
be pressed to get the `` P>'' prompt.
 ...objects.
 Note: This has not been fully implemented.
 ...below.
 Note that if the command window is hidden from view, one can
enter mouse mode unwittingly.
If this happens it will appear as though
is not responding to any
input except for the arrow keys.
 ...relation:
 A note for experienced 638#638 users: no backslashes are required
in this def.
 ...return.
 Carriage returns are significant only as delimiters.
 ...text.
 Unlike, for example, the Unix program nroff
does not strip off
backslashes when evaluating macros.
They are stripped off only when text is actually parsed.
 ...T.
 There is a similarity between a type
and Bishop's notion of set. Bishop [Bishop 67] says that to give a set,
one gives a way to construct its members and gives an equivalence
relation, called the equality on that set, on the members.
 ...variables.

An identifier is any string of letters, digits, underscores or
atsigns that starts with a letter.
The only identifiers which cannot be used for variables are
term_of and those which serve as operator names, such as
int or spread.
 ...x:A.
 In the
formation of these as members of 766#766, B must be
767#767functional in x:A.
 ...constructor.
 modulo the difference between
A#B and x:A#B, etc.
 ...(x:A#B).

If the reader finds this a bit difficult to follow, perhaps it would help
to consider first the case in which x is not free in B and z is not free in T and then the more general cases afterward.
 ...integers.

This is defined by primitive recursion with 0 as the
base case and an induction step for each direction out
(positive and negative). Of course, in a higherorder system such as
, where functions can take functions as arguments and
have functions as values, one can define by primitive recursion
functions in int>int which are not primitive recursive.
 ...true.

If we were to give a similar semantic account of the judgements of
[MartinLöf 82], the plainest difference between the truth conditions for those
judgements and
judgements would be that the truth of the former
requires typefunctionality of each assumption in all its variables.
 ...inhabited.

Recall that the term (a = b in A)
is a type whenever 886#886 and 887#887 and is inhabited just when
888#888.
As a special case, the term (a in A) is a type and is inhabited
just when 889#889.
 ...system.

It turns out that these predicates will hold only for closed terms.
 ...theorem.
 This rule introduces very strong interproof dependencies.
A proof using this rule depends not only on C but also on the way
C is proved.
 ...variable.
 The system
actually uses sequences of asterisks rather than Greek letters.
 ...operators
 The notation for the
logical ``or'' is or and for ``and'' is &.
 ...is
 This is a
specialization of the LCF [Gordon, Milner, & Wadsworth 79] concept of tactic in that both
goal and event are taken as partial proofs.
 ...substitution,
 This is
usually how substitution takes place throughout the Nuprl
system.
 ...subgoal.
 For example, doing
intro's on a universally quantified formula generates
as many subgoals of this form as there are
quantified variables.
 ...nontrivial.
 Proving
that a type of the form t in T
is wellformed, for instance, requires proving that
t is a member of T, and this can be a Nuprl
\
statement that a program meets its specifications.
 ...principle.
 This principle
states that any function mapping a finite set into a smaller finite set
must map some pair of elements in the domain to the same element
in the codomain.
 ...forms.
 This will ensure that
the definitions of relations 2041#2041 and 2042#2042 are sensible.
A more liberal (and complex) restriction is given in [Constable & Mendler 85].
 ...refs.
 See chapter 7 for more on the eval command.
 ...functions.
 The variable _y_ contains underscores because
we want a name unlikely to appear in the surrounding text.