The starting point for my interest in constructive mathematics was a colloquium given at Stanford by Errett Bishop, well-known proponent of constructive mathematics. The discussions precipitated by this colloquium led Harvey Friedman to pose the question which was ultimately answered by my Ph. D. thesis [1]. Since this was the starting point of several years of research, I shall explain the question.
In constructive mathematics, an important idea is that functions constructively defined on the reals must be continuous. Intuitively, this is because one must be able to compute the answer from the input, and how can you compute a real number from a "given" real number except by some method based on using approximations to the input to get approximations to the answer? A step function which is 1 for non-negative input and 0 for negative input, for instance, is not constructively defined on all real numbers, but only on those real numbers whose sign can be computed.
One possible way in which you might use the "whole" real number at once without having to manipulate an infinite "object" is if the input is given by a program for generating approximations. An effective operation is a function on real numbers which works this way, taking as input indices of Turing machines for generating real numbers, and respecting equality in the sense that different indices for the same real number x give as answers different indices for the same real number f(x).
An amazing theorem TKLS, proved independently in Russian by Tseitin and in the West by Kreisel, LaCombe, and Shoenfield (Tseitin has priority), says that effective operations are continuous. But the proof of this theorem is not quite constructive, involving as it does an argument by contradiction. The argument by contradiction is used only to prove that a certain computation must halt. This limited use of argument by contradiction was considered admissible by the Russian constructivists, and it bears the name Markov's principle. The question posed by Friedman was whether this deviation from constructive principles could be eliminated, or not. In other words, is TKLS derivable in intuitionistic arithmetic (without Markov's principle)?
The main result of my thesis is that the use of Markov's principle in the proof of TKLS is indispensable: TKLS is unprovable in intuitionistic arithmetic. A similar underivability result was obtained for a variant of TKLS called Myhill-Shepherdson's theorem, which applies to partial functions. The method I used in the proof was a new variant of Kleene's "recursive realizability". The dissertation work was published in [2].
Actually, TKLS refers to functions defined on the space of functions from N to N, rather than on the reals. It is not hard to extend the proof to the more general setting of functions from one complete metric space to another, but an independence result is different for each specific case. For example, the theorem that effective operations on the reals are continuous does not immediately imply TKLS. My first paper after my thesis [3], extended the independence result to the case of effective operations on the reals. (I wrote this paper on a patio overlooking the San Lorenzo River, in Felton ,California, while employed at the University of California, Santa Cruz.)
My dissertation also contained the result that if a specific Turing machine can be proved in intuitionistic arithmetic to be an effective operation, then it can also be proved to be continuous. That is, although TKLS is not provable, it is only the implication that is unprovable: it isn't possible to exhibit a specific operation for which the hypothesis is provable and the conclusion not provable. This result was published in [4].
The next question was whether this independence result continues to hold relative to stronger constructive theories than inuiitionistic arithmetic. What if, for instance, we add sets of numbers (or "species") and axioms asserting the existence of sets defined by any formula in the second-order language? To settle this question, I had to extend my new notion of realizability to that theory and prove its soundness. This was done in [5].
At this point, Prof. Solomon Feferman began to develop his theories for "Explicit Mathematics". These theories at once struck my by their elegance and beauty, and also by the wide-open opportunities to study their metamathematics. Feferman had already shown how to extend Kleene's basic realizability to his new theories, but it fell into my lap to extend the other known metatmathematical tools to these new theories, including my own new realizability, and obtain some basic metamathematical results about them. While doing this, I realized that the principle that "constructively defined functions are continuous" could be extended to a more general principle, namely that constructive existence theorems imply that the constructed object depends locally continuously on parameters. This is more general because there can be regions of parameter values in which there is more than one dependent object, and no continuous function will always succeed in constructing such an object. At the time, Ralph Abraham was writing papers on catastrophe theory which impressed such situations upon me, and I had also been systematically giving a constructive treatment of my favorite subject in pure mathematics, minimal surfaces, in which such situations arise. In [6] I published some of these metamathematical results about Feferman's system, as well as the general formulation of the "principle of continuous choice". (The material in [6] is presented in a more coherent fashion, and at least one error is corrected, in my book Foundations of Mathematics which should now be read instead of [6].)
That still left the matter of the derived rules of inference: were provably defined functions in Feferman's systems also provably continuous? To settle that question for arithmetic, I had used the Gödel Dialectica interpretation. This depends heavily on the use of type theory, and it was not obvious whether it could be extended to a type-free theory like Feferman's. In [7] I gave such an extension and used it to show that the derived rules of inference related to continuity, as well as Markov's rule, are valid for Feferman's theories. Many years later, V. Plisko pointed out a technical oversight in the definition (and proof) which however is correctible, so the results are all correct as stated.
While living in Amsterdam in 1977, I reconsidered a theorem of Goodman, namely that the axioms of choice (AC) at all finite types could be conservatively added to intuitionistic arithmetic. While still a graduate student in 1971, I had tried to understand Goodman's proof, but I never could do more than check it line-by-line. The basic idea seemed elusive. I also tried unsuccessfully in 1971 to find my own, more comprehensible proof. Finally in 1977 I succeeded, by introducing forcing into the repertoire of metamathematical tools that could be used on constructive formal systems. Up until then, forcing had been applied only to non-constructive set theories. I was familiar with forcing, having studied it under Scott, Feferfman, Friedman, and Solovay while a graduate student, and once I got the idea to apply it to constructive theories, Goodman's theorem fell into place. I saw that his theorem could be proved by the application of first forcing, then realizability. Indeed it later seemed to me that his original proof, which had seemed so incomprehensible to me, could be understood as the composition of forcing and realizability. The new method immediately enabled me to extend Goodman's theorem to stronger theories, for example finite type theory with the axiom of extensionality, and I published the new method and results in [12].
Meantime, Myhill had developed IZR, an intuitionistic version of Zermelo-Fraenkel set theory, and these theories also begged for metamathematical work.. Friedman had extended Kleene's basic realizability to IZF, and in [12] I extended q-realizability to IZF, proving the "numerical existence property" for IZF. I also used forcing to obtain derived rules of inference about uniform continuity: provably defined functions on compact spaces are not only continuous, they are uniformly continuous.
The extension of the independence of TKLS to IZF had to await a collaboration with Andre Scedrov, which took place at a meeting in New Mexico in the summer of 1980. Late one night we sat at a table for some hours and checked the soundness of the extension to IZF of the necessary notion of realizability. This work was published in [21].
In October, 1980, I attended a series of lectures given by Per Martin-Löf in Munich, about his type theories. I still remember the extraordinary hospitality of my host, Prof. Scwhichtenberg, who introduced me to classifications of German wines I had not known existed. I finally managed to understand Martin-Löf's theories that week, and on the train back to the Netherlands, where I was living at the time, I worked out the definition of recursive realizability for Martin-Löf's theories and proved its soundness. Up until this time, the only proof of consistency of these theories was via the term model given by Martin-Löf. This work was published in [18]. The material can also be found in Chapter XI of Foundations of Constructive Mathematics.
An earlier piece of work, proving that the join axiom in Feferman's theories, in the presence of only weak induction, still has only the proof-theoretic strength of arithmetic, reached print only some years later in [25]. This was my first use of Gentzen's sequent calculus, which I later used in my work on automated deduction.
From 1980 to 1985, my efforts were all directed towards the publication of Foundations of Constructive Mathematics [23]. This book presents all the theories described above, and all the main metamathematical results about them, as well as a lengthy chapter containing the important results of recursive analysis.
During this period I was also beginning to teach computer science, and saw how Feferman's theories could be applied to proving the correctness of programs. I presented these ideas in [24], which also contained a definition of (and completeness proof for) the Logic of Partial Terms (LPT). LPT is a logic designed to allow the construction of terms that have no denotation, such as "The King of France", or the output of a non-terminating program.
After the book was published, I reflected on the subject, and thought that the essence of the problem all the above theories are trying to solve is to give a formal account of the use of both rules (algorithms) and sets in constructive mathematics. Since in the logical tradition there is a well-established theory of rules (lambda calculus) and a well-established theory of sets (ZF), why not just combine those two theories? I published this theory and a consistency proof in [27]. Nobody else has yet taken up the study of this system, although there is an interesting open problem concerning it.
The survey article [26], which appeared in a volume dedicated to Turing, chronicles the relationships between logic and computation. The tension between these two basic elements of mathematics is differently resolved in classical and constructive mathematics. It is also at the heart of automated deduction, which reduces logic to computation (proof search). Curiously, the programming language Prolog, based on this reduction, can in turn be used to reduce computation (programs) to logic! By this time, I was fully immersed in a software development effort, building programs to help students learn algebra, trig, and calculus. The machinery at the core of this project had to be able to do computations in algebra and calculus, but to keep computation rules from being incorrectly applied, there also had to be a powerful logical apparatus. Many months of intensive labor went into this, most of it the antithesis of theoretical in nature, but at one point I found that I could simplify the program a good bit, and make it run faster and better, by using non-standard analysis in the logical part of the program. The algorithm seemed to work, but it clearly needed a correctness proof, which I supplied in [36].
With the Mathpert software finished at last, I turned to the other extreme, writing a paper [41] on the basic philosophical issues of mathematical existence. In the years 1998-2000, my work in automated deduction was the focus of my attention. In my mind, this rather applied work was just another way of approaching the boundary between logic and computation. In 1998, this work led to a rather theoretical paper [42], presenting properties of a new unification algorithm.
Strangely enough the work on automated deduction led at the end of 2000 back to logic! Discussions with Larry Wos about automated deduction in propositional logic led to a theoretical question about deductions in Lukasiewicz's propositional logic, which I was able to answer, modulo many lemmas which Larry proved in Otter. There were also some lemmas that were proved in a specially compiled version of Otter by Robert Veroff, so the paper that resulted, namely [48], has three authors.