Cross-links between Nuprl and Constructive Mathematics


Constructive mathematics is pertinent to the PRL project because all of our logics have had a constructive core. This means that they can make distinctions that are critical in expressing computational mathematics. For example, it is trivial to express the notion that a problem is decidable; using the constructive "or" logical operator and letting P name the problem, we say P or not P. Our logics also express classical reasoning. In some cases this is accomplished by defining the classical logical operators in terms of the constructive ones. In other cases we have shown that it is consistent to add classical axioms as a way to produce subtheories of the constructive logic (subtheories in the sense of subtyping).

For many centuries there has been a strong computational theme in mathematics. Prominent points have been the Greek interest in ruler and compass constructions, the Arab interest in algorithms and the algebra of solving equations, and the European development of the eighteenth and nineteenth century theory of functions.

A noncomputational tradition has also enjoyed great success. This is often associated with set theory and pure existence proofs and the like. Nowadays this is called "classical mathematics" even though its distinct existence dates from the 1800s. Its modern expression was brought into focus by Cantor and Hilbert, who referred to it as "ideal" mathematics. One might also use the term "existential" for it.

Even when this view was gaining popularity, many of the leading mathematicians expressed the need to keep track of computational meaning. We read of this concern in the writing of Kronecker, van der Waerden, Weyl and Gentzen in Germany; from the French school of Poincaré and Borel, Baire, Lebesgue, Lusin and Herbrand; from the Dutch, Brouwer and Heyting; from the Scandinavians like Skolem; the Russians Kolmogorov and Markov and so forth.

In the early twentieth century these two traditions came into conflict as part of what is called the crisis in the foundations of mathematics. In the nineteenth century, the paradoxes of calculus provoked an effort to create a firm foundation for the calculus based on type theory and logic or on set theory. The paradoxes in type theory and set theory - such as Russell's paradox or the Burali-Forti paradox - were considered by some to constitute a crisis in foundations. Brouwer's response to the crisis was to say that the problems arose from the nature of "ideal" or "existential" mathematics and did not arise in the computational tradition. This opinion was put in a confrontational and provocative way. Hilbert responded with a program to "save" ideal mathematics. That program is still known as Hilbert's Program. He cast it in opposition to Brouwer, although Kolmogorov and Gödel later showed that there need not be incompatibility. Hilbert's rallying cry was that "mathematicians would not be driven out of the paradise" that Cantor's set theory provided.

Now that the dust has settled and the controversy dimmed by the passing of the main protagonists, we can see that there remain these two traditions: the old computational and the modern (so called "classical" or "ideal"). The computational tradition has received renewed attention because of the advent of modern digital computers. Fields like numerical analysis, symbolic algebra, computational geometry, computational number theory, and automated deduction have arisen fresh in the last fifty years to employ large numbers of mathematicians, many of whom are not working in mathematics departments. These fields have become vital to modern science and industry. Some of them are part of the subject of computer science.

As we discuss in the section on Logic, modern computational mathematics has revealed some new foundational problems. We have written about this in Formalizing Automata II: Decidable Properties. Our group has also contributed directly to the computational mathematical tradition as we outline next.

Technical Contributions

One of the most celebrated formalizations we have done was Chet Murthy's formalization of Higman's Lemma in a classical extension of Nuprl 3. He was able to automatically translate this to a constructive proof using Harvey Friedman's theorem on so-called A-translations. Further work on this problem was carried out in Coq by Hugo Herbelin.

We have carried out more of Bishop's approach to constructive analysis by formalizing parts of his account of the calculus and proving the Intermediate Value Theorem. Citations.

The most extensive piece of new constructive mathematics done to date is Paul Jackson's development of constructive algebra up to the definition of polynomials in order to provide a foundation for computer algebra systems. (Citations.)

We have also developed parts of basic recursive function theory constructively.(Citations.)

Recently we have formalized results from Hopcroft and Ullman's book Formal Languages and Their Relation to Automata. (Citations.)

Here are the on-line libraries which are described in Formalizing Automata Theory I: Finite Automata and Formalizing Automata II: Decidable Properties and as published.

We are also creating an extensive library of elementary discrete mathematics on-line. This can be read either classically or constructively, a style advocated by Bishop in his book.

Constructive Logic

Judith Underwood gave a constructive proof of the completeness of Intuitionistic Propositional Calculus with respect to Kripke models in a paper and her thesis. Jim Caldwell has formalized this argument in Nuprl, and the algorithm extracted from the proof is a decision procedure for provability.

At Chalmers University in Gothenburg, Sweden, Coquant and Smith proved an abstract constructive completeness theorem for the Intuitionistic Predicate Calculus with respect to formal topology models. This proof was formalized in the Alf system by Henrik Persson based on a proof by Jan Cederquist.