Explaining the undecidability of first-order logic

Abstract

Turing proved the unsolvability of the decision problem for first-order logic (Entscheidungsproblem) in his famous paper On Computable Numbers, with an Application to the Entscheidungsproblem. From this proof it follows that attempts to specify a solution for the Entscheidungsproblem through pattern detection in automated theorem proving (ATP) must fail. Turing’s proof, however, merely predicts the non-existence of such solutions; it does not construct concrete examples that explain why specific attempts to solve the decision problem by pattern detection fail. ATP-search often runs in infinite loops in the case of unprovable, i.e. not refutable, formulas and one can ask why finite patterns of repeated inference steps cannot serve as criteria for unprovability. We answer this question by constructing pairs of formulas (ϕ,ϕ′) such that ϕ is provable (refutable) and ϕ′ is unprovable (satisfiable in an infinite domain) but all but the last proof step of the ATP-search for ϕ is a proper part of the endless ATP-search for ϕ′. We generate such pairs of formulas by mimicking computable sequences for a certain kind of universal Turing machine, namely, splitting Turing machines (STMs), via sequences of inference steps in ATP. In contrast to Turing’s and the textbooks’ method to formalize Turing machines, our method does not rely on further axioms and allows us to transfer the straightforward insight that the halting problem cannot be solved through pattern detection to the case of the Entscheidungsproblem. Our method is a constructive alternative to general undecidability proofs that explains why a scientific problem, namely the Entscheidungsproblem, is unsolvable in a specific way. This explanation provides a better understanding of the failure of pattern detection, which is of interest to: (i) the programmer, who is concerned with prospects and limits of pattern detection, (ii) the logician, who is interested in identifying logical properties by properties of an ideal notation, and (iii) the philosopher, who is interested in proof methods.