A Sample Theorem in Nuprl's Logic

We take as an example, the theorem:

$$\forall A:{\Bbb{P}}_{i}.\ \forall B:{\Bbb{P}}_{i}.\ \neg(A \wedge B) \Longleftrightarrow \neg A \vee \neg B.$$

This is one of the DeMorgan laws for propositional logic. The connectives $\neg,\ \wedge, \vee,\ \Longleftrightarrow$ are respectively the not, and, or, and iff connectives of propositional logic. Other logical connectives used in Nuprl are $\Rightarrow$ (implies), and $\Leftarrow$ (is implied by). We sometimes call $\Leftarrow$ rev_implies.

The universal quantifiers (the terms starting with $\forall$) and the ${\Bbb{P}}_{i}$ in the example perhaps require a little explanation. The expression $\forall x:T.\ P$ reads as ``for all x of type T , proposition P holds''. The Nuprllogic also has an existential quantifier; $\exists x:T.\ P$ reads as ``there exists an x of type T such that proposition P holds''.

It is common in logic books, when there is only one domain over which quantification ranges, to omit any specific mention of the domain. In Nuprl there are many domains or types over which quantifiers can range, so we always make the domain explicit. In the theorem above, the domain of quantification for both A and B is ${\Bbb{P}}_{i}$, read as ``propositional universe i'' or for short ``prop i''. ${\Bbb{P}}_{i}$ is a type of propositions. The need for the subscript i arises from a concern expounded by the philosopher Bertrand Russell in his Principia Mathematica. The concern is that of avoiding circularity of reference. Russell disliked considering the proposition $\forall A:{\Bbb{P}}.\ P$, where ${\Bbb{P}}$ is a type of all propositions, as a member of type ${\Bbb{P}}$. He argued that it is meaningless to define some new element of a type by quantifying over all members of that type, since the range of the quantification would have to already include that new element. He refered to this self-reference as a vicious circle.

The Nuprl logic follows in the type theoretic tradition established by Russell, and has an infinite series ${\Bbb{P}}_{1},{\Bbb{P}}_{2},{\Bbb{P}}_{3},\ldots$ of types of propositions. The subscripts are called levels. ${\Bbb{P}}_{2}$is the type of all propositions at level 2. The level of some proposition is 1 greater than the maximum of all the levels explicitly mentioned in the proposition. If no levels are mentioned, then the proposition is at level 1. The types ${\Bbb{P}}_{i}$ are cumulative in the sense that ${\Bbb{P}}_{i}$ contains not just the propositions with level i , but the propositions with levels from 1 upto i . In Nuprl, we avoid the question of what level to state a theorem at by replacing level numbers by variables, and consider the level variables to be implicitly (universally) quantified over. Hence the use of ${\Bbb{P}}_{i}$ as the type of A and B in the example theorem.