The logic of Nuprl is a constructive type theory, but its types include those of partial objects, so it is also a domain theory. Its primitives are rich enough to build a substantial set theory on top of the type theory, one equivalent in expressive power to ZFC. This section first looks back to the origins of type theory and then traces its development through domain theory and to Nuprl.
The first chapter of Aristotle's classical book on logic, the Organon (Logic), is Categories
In Nuprl terms, Aristotle is saying that if the underling types (genera) are
different, say A is not equal to B, then no subtype of A, say {x:A|B}, is the same as any subtype of B, say {y:B|Q}. He goes on to say in the next sentences that if
A is a subtype of B (subordinate genera of B), then we can predicate P of both A
and B objects.
Martin-Löf and the Nuprl designers followed Aristotle in first laying down some
properties of language; e.g., of terms, before stating the typing principles. So
Aristotle begins the Categories by talking about homonyms, synonyms, individuals,
compound expressions, predicates ("of a subject") and typings ("in a subject").
Aristotle's logic introduced many other fundamental ideas, e.g., the third section
of the Organon, called Prior Analytics, was a study of demonstration, including
various rules of inference (essentially what is now called the monadic predicate
calculus), but it did not deal with paradoxes such as that of Epimenides the Cretan who said that all Cretans are liars; one of their poets said so. This is
essentially the question of the truth of the statement that says: "This statement
is false". This is the
Eubulides paradox. This paradox was a challenge to common sense that everyone could understand, but it did not seem to affect the careful language of science and mathematics. Russell remarked that people considered it more of a joke than a problem. But in June of 1901 Bertrand Russell discovered his famous paradox lying at the heart of a logic that was intended to provide a basis for all of mathematical reasoning. Just before he and Whitehead started Principia Mathematica, he showed that it is contradictory to talk about the set of all sets that do not contain themselves; the discovery is called Russell's Paradox: Let R = { X| not X in X}. Then
is R in R? If it is, then it is not. If it is not, then it is.
We have a
formalized version of this
in Nuprl.
In June 1902, having spent a year trying to understand and resolve the paradox, Russell communicated it to Gottlob Frege because
it also revealed a contradiction in Frege's just completed foundational logic for
all of mathematics, his Grundgesetze der Arithmetik (Foundations of
Arithmetic). Now the Liar Paradox and others took on some urgency, and Bertrand
Russell devoted the next decade of his life to working on this problem. In his 1908 paper, Mathematical Logic as Based on the Theory of Types, Russell laid
out a careful theory to contain the paradoxes. It became the basis of the logic of Principia Mathematica that he and Alfred North Whitehead published in 1910. This paper opens with the sentence, Russell went on to enumerate seven paradoxes, starting with that of Epimenides: then
the one he discovered (in two forms); then Berry's paradox about the least number
not nameable; another about the least indefinable ordinal; then the Richard paradox; and finally the Burali-Forti one. Kleene's famous book Introduction to
Metamathematics also begins with an extensive discussion of these paradoxes. Russell's solution is to invoke a new basic principle of logic and apply it to
designing a type theory that enforces the principle. The key point for us is that
Nuprl basically adopts Russell's solution in its modern form. Here is how Russell
put the matter. ...thus "I am lying" becomes "It is not true of all propositions
that either I am not affirming them or they are true;" in other words, "It is not
true for all propositions p that if I affirm p, p is true." The
paradox results from regarding this statement as affirming a proposition, which
must therefore come within the scope of the statement. This, however, makes it
evident that the notion of "all propositions" is illegitimate; for otherwise, there
must be propositions (such as the above) which are about all propositions and yet cannot, without contradiction, be included among the propositions they are
about. This leads us to the rule: "Whatever involves all of a collection must not be one of the collection," or, conversely: "If, provided a certain collection had a total, it would have members only definable in terms of that total, then the said collection has no total."(1) A type
is defined as the range of significance of a propositional function, that is, as
the collection of arguments for which the said function has values. Whenever an
apparent variable occurs in a proposition, the range of values of the apparent
variable is a type, the type being fixed by the function of which "all values" are
concerned. The division of objects into types is necessitated by the reflexive
fallacies which otherwise arise. These fallacies, as we saw, are to be avoided by
what may be called the "vicious-circle principle," that is, "no totality can
contain members defined in terms of itself." This principle, in our technical
language, becomes: "Whatever contains an apparent variable must not be a possible variable of that variable." This whatever contains an apparent variable must be of a different type from the possible values of that variable; we will say that it is of a higher type. Thus the apparent variables contained in an expression are what determine its type. He introduces the notion of first-order, second-order and higher order logics in this way. ...We may define an individual as something destitute of
complexity; it is then obviously not a proposition, since propositions are
essentially complex. Hence in applying the process of generalization to individuals
we run no risk of incurring reflexive fallacies. Elementary propositions together with such as contain only individuals as
apparent variables we will call first-order propositions. We can thus form
new propositions in which first-order propositions occur as apparent
variables. These we will call second-order propositions; these form the
third logical type. Thus, for example, if Epimenides asserts "all first-order
propositions affirmed by me are false," he asserts a second-order proposition; he
may assert this truly, without asserting truly any first-order proposition, and
thus no contradiction arises. The above process can be continued indefinitely. The (n + 1)th logical
type will consist of propositions of order n, which will be such as contain
propositions of order n - 1, but of no higher order, as apparent
variables.... Martin-Löf type theory is based on Russell's insight, but instead of a Russell's complex
system (called ramified type theory) it is based on an open-ended sequence of
universes, U1, U2, U3, .... that stratify the concept of type. The Martin-Löf form
is called a predicative type theory - in contrast to the impredicative forms such as
full second order logic, either classical or constructive (called the theory of
species in the constructive case). Nuprl follows this line as well. One alternative to this Russellian stratification are systems that allow a single
universe of all types (or all sets). Russell would say that such an object is too
big, but a contrary view (held by Quine, for example) is that having a set of all
sets or a type of all types is legitimate as long as we do not permit forming all
subsets. If there is some restriction on which subsets can be formed, say by
requiring a stratified predicate to define the subset, then no contradictions will
result. Quine proposed a system called New Foundations, NF, based on this
idea. There are other such set theories, including one proposed by
Alonzo Church
in 1974. In the case of "pure logic," the idea of a single large type that violates Russell's
principle appears in the notion of second-order logic. It is possible to quantify
over the type of all propositions to form statements like: Forall P.P. This
sentence is a proposition, so it can be instantiated with itself, a clear violation
of the vicious circle principle and a clear case of an impredicative notion of
proposition. Alonzo Church proposed a classical type theory based on this impredicative notion of
proposition in his paper Formulation of the Simple Theory of Types, JSL, 5,
1940, 56-68. This is the logical basis of the HOL system. The theory is anything
but "simple" from a philosophical or foundational point of view. It is equivalent to Zermelo set theory, Z. The constructive version of second order type theory allows a fully impredicative
notion of proposition, which at first sight seems to violate the notion of
construction in that the propositions cannot be built up systematically from
simpler ones. This theory can be generalized to Intuitionistic Higher-Order Logic,
say IHOL. Type theory opened the door to another fundamental idea in logic - the notion that
propositions are types which, if true, are inhabited by proofs. This conception of
mathematical truth had been already articulated clearly by
L.E.J. Brouwer in
1908. According to Brouwer's Intuitionist philosophy, a proposition is only true if
we can prove that it is. His notion of proof was not that of a logician's formal
proof, but once
Heyting formalized the notion of Intuitionistic Logic, it became
a challenge to also provide a precise sense in which there is a mathematical object
that proves a true formula.
Gödel and
Kleene approached this problem at nearly the same time. Kleene discovered
the concept of realizability in terms of recursive functions. Gödel
used the notion of primitive recursive functions in all finite types, his system T,
to provide a semantics for Intuitionistically true formulas. Other notions of realizability were later discovered.
Haskell Curry noticed in 1954
that propositional formulas could be realized by composition of his S, K and I
combinators. Bill Howard generalized this idea to the predicate calculus in
1968. At about the same time, N. G. deBruijn described his Automath project and
series of languages which used the lambda calculus to code proofs and provide
realizers. Lauchli also sought a semantics for Intuitionistic logic and was led to
realizers. Per Martin-Löf understood from Howard and Dana Scott understood from deBruijn that
these realizability concepts were central to a semantics for Intuitionistic
mathematics and that this semantics should drive the design of formal systems. They
each proposed foundational systems in the early 70s, but Scott had second thoughts
which he expressed in his paper. At essentially the same time, Jean Yves Girard discovered a class of typed lambda terms
that served as realizers for the "Theory of Species," a formalism he called system
F. He proved a remarkable theorem that his typed lambda terms were strongly
normalizable. This provided a consistency proof for the Theory of Species. The same
class of lambda terms was independently discovered by John Reynolds as a model of
typed programming languages. The theories of Martin-Löf and Girard used only total functions in their
semantics. But in computer science, the notion of a partial function was basic. The
standard universal programming languages like Algol and Lisp allowed these partial
functions. Indeed Lisp could be seen as a programming language based on the untyped
lambda calculus with its unrestricted use of the Y combinator. In the early 70s
Dana Scott set out to provide a mathematical semantics for this class of
functions. Basically he started with the realizers and tried to find a type
theory. His approach is now known as Domain Theory and is a flourishing branch of
mathematics and computer science. Nuprl draws heavily on the semantic theories of Per Martin-Löf which were inspired
by the Curry-Howard correspondence. We showed how to apply these ideas to a very
rich type theory, one adequate as the foundations of computer science, and we
showed how to use the full power of the lambda calculus as realizers by allowing
the Y combinator as a realizer. In this setting we were also able to provide types
for partial functions in the manner of Dana Scott. This allowed us to reconcile
Domain Theory and type theory as we felt was necessary to provide a foundation for
computer science.
The differentia of genera which are different and not subordinate one to the other are themselves different in kind. For example, animal and knowledge:
footed, winged, aquatic, two-footed, are differentia of animal, but none of
these is a differentia of knowledge.
The following theory of symbolic logic recommends itself
to me in the first instance by its ability to solve certain contradictions, of
which the one best known to mathematicians is Burali-Forti's concerning the
greatest ordinal.
.... Whatever we suppose to be the totality of propositions, statements
about this totality generate new propositions which, on pain of contradiction, must
lie outside the totality. It is useless to enlarge the totality, for that equally
enlarges the scope of statements about the totality. Hence there must be no
totality of propositions, and "all propositions" must be a meaningless
phrase.
The hierarchy of types
Alternatives
Propositions as Types and Realizability of Propositions
Domain Theory
Technical Contributions