Differences in the Logic

The Nuprl proof rules naturally extend the Lambda--prl proof rules and as such are organized along roughly the same lines. However, the logic of Nuprl is considerably more powerful than that of Lambda--prl , and the rules are correspondingly more complex. The Nuprl rules are classified into three broad categories: introduction, elimination and equality; the equality rules are further broken down into computation rules and equality rules for each of the term constructors. The introduction and elimination rules are analogous to those in Lambda--prl ; the equality rules are a new feature of the Nuprl logic.

The differences between the logic of Lambda--prl and Nuprl can be briefly summarized as follows:

• Strengthening the type structure.
  The Lambda--prl logic is based on two primitive types, integers and lists of integers. The Nuprl logic extends this to a much richer type structure.
• Identifying propositions with types.
  In Lambda--prl propositions were specific syntactic entities. In Nuprl propositions are simply certain kinds of types. Demonstrating the truth of a proposition amounts to presenting an object of that type so that a proposition is treated as the type of its justifications.
• Well-formedness.
  In Lambda--prl well--formedness of propositions was checked by the system. The richness of the Nuprl type structure, however, precludes the possibility of automatically checking whether or not an expression is a type. By the identification of propositions with types this property extends to propositions as well.
• Explicit treatment of equality and simplification.
  In Lambda--prl equality and simplification were by and large taken care of by the arith rule, which handled simple arithmetic, substitutivity of equality and simplification of terms (such as hd[1,2]=1). The Nuprl logic, however, is sufficiently rich that such a treatment is no longer possible. Consequently there are rules for equality of terms and for computation.

• Introduction Rules
• Elimination Rules
• Equality and Simplification Rules