Carnegie Mellon University
Computability & Automated Proof Search

Computability & Automated Proof Search

The notion of computability plays a most important role in a department of philosophy for two reasons: (i) it is used in cognitive science and the philosophy of mind; (ii) it is needed for some of the most fundamental results in mathematical logic. Gödel's incompleteness theorems and the undecidability of predicate logic are among those results that prompted the concern with a precise mathematical characterization of computability.

Axioms for computability. Sieg analyzed the historical origins and the evolution of the notion starting in the late 1920s. It became clear that one key notion was being captured, namely, calculability in logical calculi; that is apparent from Gödel's and Church's relevant work and the analysis of "reckonable" functions carried out by Hilbert and Bernays. It was only in Turing's work, however, that restrictive finiteness and locality conditions were intrinsically motivated (through an appeal to the restricted sensory capacities of human beings operating in a mechanical fashion). Sieg formulated these conditions precisely and imposed them axiomatically on discrete dynamical systems; he proved then an appropriate representation theorem: computations of any model of these axioms are reducible to Turing computations. Refining work by Turing's student Robin Gandy, Sieg also formulated axiomatic principles for computations carried out by machines, i.e., discrete mechanical devices. It is the special feature of machines that they can carry out massively parallel computations. And yet, the computations of any model of the "machine axioms" are also reducible to Turing computations.

Semantics for computation. Theoretical Computer Science is of course an important area of research at Carnegie Mellon, with several very strong groups of researchers in different areas. The field of programming semantics is one such area, and Awodey often cooperates with CS colleagues in research, doctoral supervision, conference organization, refereeing, etc. Some of Awodey's research is devoted specifically to developing and investigating new mathematical structures as semantics for programming languages, involving functorial, topological, and algebraic methods. For instance, recent work on homotopy-theoretic semantics for intensional type theory provides a link between classical topology and a system of constructive type theory with wide-ranging computational applications -- and the first known abstract semantics for that theory.

Search and verification. The undecidability of the decision problem puts a limit on how far we can realize the Leibnizian idea of Calculemus, i.e. deciding mechanically any question that can be formulated in a "universal language." What can be done positively comes under the heading of fully or partially automated reasoning. There is considerable expertise and talent in that field at Carnegie Mellon, not only in this Department, but also of course in Computer Science (Clarke and Pfenning), not to speak of the venerable history through the early work on theorem proving by Allen Newell and Herbert A. Simon.

Sieg's work in proof theory has been focused recently on the investigation of systems of natural reasoning. Indeed, it was the need for finding ways of searching for proofs in such systems for first-order logic that motivated the proof theoretic work; that was quite successful in that it led to the implementation of efficient proof search algorithms. These algorithms are strategically guided, and the purely logical strategies can be extended quite directly to incorporate the use of definitions and of lemmata. If one exploits in addition particular subject-specific heuristics, then one has a dynamic framework in which one can search for mathematical theorems. That was accomplished for parts of meta-mathematics, i.e., Gödel's incompleteness theorems were found at an "abstract" level. Currently, elementary set theory is being investigated with the goal of finding a proof of the Cantor Bernstein theorem within the axiomatic framework formulated by Zermelo and Fraenkel.

"Formal verification" involves use of computational methods to verify correctness of mathematical arguments, as well as the correctness of hardware and software design with respect to a formal specification. Avigad has worked in the field of "Interactive theorem proving," which uses computational proof assistants to obtain formal axiomatic proofs of such claims. He obtained a landmark verification the Prime Number Theorem in Isabelle in 2004, and was a member of a team, led by Georges Gonthier, that completed a formal verification of the Feit-Thompson Odd Order Theorem in the Coq proof assistant in 2012. He has also contributed to homotopy type theory, developing a library for homotopy limits of diagrams over graphs with Krzysztof Kapulkin and Peter Lumsdaine.

Avigad has also developed decision procedures and algorithms to support such work. With Turing Award winner Edmund Clarke and their student Sicun Gao, he helped develop a new framework for the formal verification of hybrid systems, which combine discrete and analog components. He has developed, with Robert Lewis, a new method of verifying real-valued inequalities, drawing on his earlier work with Harvey Friedman on methods of combining decision procedures over the reals.

Awodey's collaboration with Voevodsky on Univalent Foundations for Mathematics has as a significant component the large-scale formalization of mathematics in the Coq proof assistant, as well as the development of new proof assistants for this purpose. During the special year at the Institute for Advanced Study in 2012-13 a large body of mathematics was formalized in this new system, including many results from classical homotopy theory such as computations of the homotopy groups of spheres. Awodey is currently supervising two dissertations related this work: one by Kristina Sojakova in CMU Computer Science Department (jointly advised with professor of Computer Science Frank Pfenning) and one by Chris Kapulkin in the University of Pittsburgh Mathematics Department (jointly advised with Pitt professor of Mathematics Thomas Hales).

Computable analysis. Avigad and his students have worked in computable analysis, providing computable versions of key theorems in ergodic theory and measure-theoretic probability. He has also contributed to algorithmic randomness, providing an analysis of the type of randomness implicit in a seminal theorem due to Weyl. With Vasco Brattka, he wrote a detailed survey of the history of computable and constructive analysis.