Well-Formedness of Terms

This section explains why Nuprl's basic inference rules have well-formedness premisses (or subgoals, thinking of the way in which Nuprl uses the rules), and motivates the use of the Auto tactic for type-checking.

Nuprl takes an uncommon attitude towards the checking of the well-formedness of terms. A term is well-formed if it has been properly put together. Usually in the study of logic, well-formedness is characterized by a simple set of syntactic rules, and when building theorem provers, it is easy to check well-formedness automatically. Because Nuprl is intended for for general purpose mathematics, things are not quite as simple. For example consider the proposition

$$\forall j,k:{\Bbb{N}}.\ k \not= 0 \Rightarrow j \div k \le j$$

Here, it is not true that $j \div k$ is a meaningful expression for all j and k of type $\Bbb{N}$ ($\{0,1,2,3,\ldots\}$); it is meaningless when k = 0 . So to check the proposition's well-formedness properly, we need to take note of the $k \not= 0$ on the left-hand side of the implication. In general k might be replaced by some complicated expression, in which case it might take a fair amount of work to prove that the proposition is well-formed. For this reason, Nuprl's logical rules were designed such that well-formedness checking is done simultaneously with truth checking. The rules guarantee that if a proof of a theorem is completed, then the theorem is both well-formed and true.

The second subgoal, with ${\Bbb{P}}${i}$\in$ $\Bbb{U}${i'} as the conclusion, is a well-formedness subgoal, requesting that the well-formedness of ${\Bbb{P}}${i}be checked. Well-formedness checking is always phrased as type checking; Some expression is well formed if it is a member of some appropriate type. Types themselves are considered members of type universes or just universes for short. As with propositional universes discussed earlier, to avoid a vicious circle, we have an infinite series ${\Bbb{U}}_{1},{\Bbb{U}}_{2},{\Bbb{U}}_{3},\ldots$ of type universes, where the subscripts are levels. Similar rules apply for determining the level of any term; take the maximum of the levels occurring in the term and add 1. If no levels occur, then the level is 1. ${\Bbb{U}}_{i}$ contains as elements all types with levels from 1 to i . The prime on the i in $\Bbb{U}${i'} is shorthand for `successor', so $\Bbb{U}${i'} is the same as $\Bbb{U}${i+1}.