Synthetic Undecidability Proofs in Coq:
The Entscheidungsproblem, Trakhtenbrot’s Theorem, and First-Order Axiom Systems
Saarland University
Abstract:
In this talk, I give an overview of our growing Coq library of undecidability proofs, with a focus on decision problems concerned with first-order logic. The first part of the talk introduces our synthetic approach to undecidability proofs based on the fact that all functions definable in Coq’s constructive type theory are computable, hence avoiding reference to formal models of computation such as Turing machines. The second part demonstrates how this approach is applied to some standard problems in first-order logic included in the library: validity and provability (the original Entscheidungsproblem), finite satisfiability (Trakhtenbrot’s theorem), and entailment in first-order axiom systems such as PA and ZF.