COMPUTER SCIENCE AND MATHEMATICAL LOGIC

Abstract

Computer science has strong connections with numerous aspects of mathematical logic, but those aspects are
sometimes different from those traditionally studied for pure mathematical purposes. This paper is a survey of some
of those interactions. Its main themes are (1) logic’s clarification of computational concepts and (2) computation’s
infusion of new concepts and questions into logic.
Section 2 mentions some of the earliest interactions. They involve what would now be called computability theory
or recursion theory, rather than computer science, as they do not involve any resource limitations. Nevertheless, I
consider them worth pointing out, to emphasize the contribution of mathematical logic to a broad topic arising in
diverse fields of mathematics.
Section 3 concerns first-order logic, especially the notion of structure at the basis of the semantics of first-order
logic, pointing out that this same notion of structure is well-suited for many roles in computer science. I also describe
here a computational view of the expressive power of first-order logic.
Section 4 concerns logical systems obtained by adding to first-order logic the central non-first-order concept
involved in computation, namely the notion of iteration. The logical incarnation of iteration is
given by fixed-point operators, which are involved in the logical characterizations of various complexity classes.
Fixed-point operators play a role in all the subsequent sections of this paper.
Section 5 begins with a very general conjecture of Yuri Gurevich that polynomial-time computation, on general
finite structures, cannot be exactly captured by any logic (in a very broad sense of “logic”). I include a description
of a logic, “choiceless polynomial time,” that comes surprisingly close to capturing PTime, and I discuss the
possibility that it might actually be a counterexample to Gurevich’s conjecture.
Section 6 is devoted to a logic of a rather different sort, obtained from first-order logic by not only adding a fixed-
point operator but also removing part of the machinery of first-order logic, namely the universal quantifier. This
existential fixed-point logic turns out to have strong connections to computation as well as a certain mathematical
elegance.
Fixed-point logics do not admit a complete deductive system in the usual sense, but it is not difficult to write
down a reasonable system of axioms and rules governing the behavior of a fixed-point operator. The question then
arises whether the unavoidable incompleteness of such a system affects only complicated, Gödel-style sentences or
whether very simple truths might be unprovable. In Section 7, I describe the system that I have in mind and conclude
with an open question about a simple truth that might be unprovable.