Research Areas
Computability & Automated Proof Search
Why should computability play any role in a Department of Philosophy?
The connection goes back to at least Leibniz: not only did he require that issues be formulated clearly in a universal language, but he also hoped that controversies could be decided by suitable mechanical means of calculation. The Leibnizian Calculemus insures radical intersubjectivity that is needed also for modern formal systems of logic and mathematics. Today, that notion is crucial to characterize formal systems and interpret the limitative theorems of Goedel, Church and Turing appropriately.
Frege saw himself directly in the tradition of Leibniz. In the 1920's Hilbert formulated the Entscheidungsproblem (the decision problem for predicate logic): Is there a mechanical procedure that allows us to decide (in finitely many steps), whether a particular statement in the language of predicate logic is logically provable or not?
Church and Turing solved the decision problem negatively in 1936. In order to obtain their solutions they introduced particular mathematical notions capturing precisely, so they argued, the informal concept of mechanical procedure. Turing gave the most convincing argument: he used the concept of computability by idealized machines and claimed that every effectively calculable number-theoretic function is actually computable by such a (Turing-) machine.
In support of this claim (thesis), Turing reasoned that all processes carried out by a human computor when effectively calculating the values of a number-theoretic function can be performed by his machines. Turing's analysis was adapted for characterizing machine computability; Turing's student Robin Gandy did that in 1980. Sieg turned this characterization into a truly abstract model for parallel (machine) computations.
The negative solution of the decision problem puts a limit on how far we can realize the Leibnizian idea of Calculemus! What can be done positively comes under the heading of automated theorem proving. There is considerable expertise and talent in automated reasoning at Carnegie Mellon, not only in this Department, but also in Mathematics (Peter Andrews) and Computer Science (Edmund Clarke and Frank Pfenning), not to speak of venerable history through the early work on theorem proving by Newell and Simon.
Sieg initiated a novel approach to automated theorem proving or, better, automated proof search. The idea is to use logically grounded strategies to search for proofs in natural deduction calculi representing the structure of informal argumentation faithfully. The theoretical work underlying the AProS proof engine emphasizes as a central theme the connection between restricted forms of natural deduction proofs and strategies for proof search: normal forms of proofs are obtained by constructing proofs that directly reflect proof-strategic considerations.
This idea has been extended, in a number of Masters and Ph.D. theses, also to intuitionistic sentential and predicate logic, but also to modal logics, for example S4. By now, the extensions cover not just logic, but particular (restricted) parts of mathematics and metamathematics. AProS has been able to prove, at an abstract level, Goedel's incompleteness theorems.
Avigad has used a mechanized proof assistant called Isabelle to formally verify the prime number theorem. This is one of the most complex mathematical theorems to be verified to date. He is currently developing proof-theoretic methods that can be used to support such verification efforts. For more information, see Avigad’s home page and the formalization project page.