View this page in Polish courtesy of Valeria Aleksandrova
All my life, since I first became aware of logic and mathematics, I have been fascinated by the relationship between logic and computation. Therefore in the early 1980's, when I began to teach computer science, I took to Prolog like a fish to water. I was fascinated by the duality of Prolog: computations were based on logic, which was in turn implemented using computations. Moreover one could use Prolog computations to implement logical systems, so one then had logic (Peano arithmetic) implemented in computation (a Prolog program) implemented in logic (Prolog) implemented in computation (machine language). Ever since Bertrand Russell's time, the question whether logic is part of mathematics, or mathematics is part of logic, or neither, has been discussed, and I confess that I still do not know the answer.
As exercised in Prolog programming and logic, I implemented a number of different logics in Prolog. The most interesting approach seemed to me to be the one using Gentzen's sequent calculus. The backtracking, variable-instantiating nature of Prolog made it possible to simply write down the rules of Gentzen's calculus, and then use this description as a theorem-prover. Of course, the uncontrolled nature of the backtracking gives an inefficient search procedure so that many simple theorems cannot be derived. But the interesting thing about this search procedure is that, restricted to Horn clauses, backtracking search in the Gentzen sequent calculus duplicates the search procedure used by Prolog itself. I then saw that Gentzen's primary proof-theoretical result about his systems, namely the cut-elimination theorem, could be used to reprove the fundamental logical result about Prolog, namely completeness: any valid formula in Horn-clause form can be proved using only Horn-clause logic, that is, Prolog. This is essentially just a special case of Gentzen's cut-elimination theorem. Working out the details of this, I found that I needed some detailed proof-theoretical lemmas, which had luckily already been worked out in an old paper of S.C. Kleene. With the aid of Kleene's lemmas, the proof was easy to finish, and appeared in [32], whose publication date is some years later than the actual work. Moreover, the same method shows that with respect to non-deterministic search, the prover is complete for the whole first-order predicate calculus, not just for Horn clauses.
Of course I was not the first to implement a theorem-prover by backwards search in the Gentzen calculus. N. Shankar did it in LISP at about the same time I did it in Prolog, and according to G. Mints, various Russian researchers did it decades ago on primitive machines in assembly language. Experimenting with my prover, I soon discovered that it could not prove various theorems in practice, in spite of the theoretical completeness result for non-deterministic search. Instead, the prover would get stuck in a fruitless infinite regress. Of course, the undecidability of predicate calculus means that any sound prover must sometimes go into infinite regress. But by breaking up the Gentzen rules into sub-cases and properly arranging the order in which these rules were to be tried, I was able to improve the performance of the prover to the point where it could, for example, solve the well-known example known as "the steamroller". This work also appeared in [32].
Starting in 1985, I began to develop Mathpert, a computerized environment for learning algebra, trigonometry, and calculus. I soon realized that the question of the relationship of logic to computation would be fundamental to this effort. The usual "symbolic computation" programs ignore logic entirely, performing computations as if logic were irrelevant. This leads to two-line contradictions: Start with the equation x=0. Divide both sides by x. All the usual symbolic computation programs will reduce x/x to 1 and 0/x to 0, so we get 1=0 as the answer.
How do you feel about flying in a plane whose jet engines have been designed using software that permits a two-line deduction of 1=0? Whatever the answer to that question, it surely won't do for software to be used by students for learning mathematics. Some other research groups worked on building educational software based on these existing computation programs, but I felt certain it would never work correctly, so I set out to design and build an integrated logic-and-computation system. By 1989 the result was ready for public demonstration, and I demonstrated it at the conference on Computers and Mathematics that summer at MIT, as well as at a conference on AI and Education in Amsterdam. The emphasis in the former lecture [31] was on the connections between logic and computation. Two years later, I had another chance to explain my ideas on that subject, including some new developments related to the connection between inference in limit problems and second-order logic, in [34]. This is the proceedings of a conference held in Russia in 1992. The conference took place on a cruise ship belonging to the Russian Academy of Sciences.
The article [26] is a survey article, intended for the non-specialist. It discusses the relationship between logic and computation and surveys several lines of research that bear on the question.
One of the most difficult areas for the relationship between logic and ordinary mathematics arises in the treatment of bound variables. These arise in calculus in connection with limit problems and definite integrals. The case of definite integrals is fairly easy to handle: when integrating from a to b with respect to x, just make the assumption that x is between a and b. This assumption should be in force when doing computation on the integrand, but only then. It isn't so obvious what to do in the case of limits--what assumption should we make about x when analyzing a limt as x approaches 0? In [34] I had given a solution of these problems using second-order logic--essentially you want to consider propositions "in a neighborhood of the limit point".But this seemed inelegant to me, and more important, it was many thousand lines of C code that were never completely debugged. In the process of rewriting Mathpert entirely in C, which I began to do in 1990, I got the idea to replace all this code with some much simpler code based on non-standard analysis. What do we want to assume about x in a limit as x approaches 0 ? Of course, that x is infinitesimal. I wrote some hundreds of lines of C code that replaced thousands of lines based on second-order logic, and it worked faster and better and more reliably. But I began to wonder whether it would in every case be correct. The semantics of the algorithm were not entirely clear, and it involved some replacements which were not strict logical equivalents, and I worried about it. Eventually I worried about it enough to try to produce a rigourous proof of correctness of the algorithm. This turned out not to be quite trivial, and both the C code and the correctness proof had to be revised to make it work. The eventual result was published in [36].
Sometime in the early 1990's, I rewrote my Gentzen-calculus based prover in C. When in the summer of 1994 I converted Mathpert to Windows, the logic and computation engines of Mathpert were placed in dynamic link libraries (DLLs), which meant that other programs could use them. It became easy to connect the Gentzen-based prover to the Mathpert engines. As a test case, I tried to use the resulting prover to do epsilon-delta proofs in calculus, for example, to prove the continuity of f(x) = x^3. This it did after a bit of tinkering. The difficult part is a chain of inequality reasoning involving some upper bounds. After having done this, I tried to find out who had done it before, and to my surprise I found that I was the first! Although Bledsoe's group at UT had a prover that has proved that the sum of continuous functions is continuous, it could prove that any specific non-linear function is continuous, because its computational facilities were too limited.