A note on the logic of Turing's halting paradox

Abstract

Projects directed at a universal logic (notably, Brady's [Brady 2006]) have long struggled with paradoxes. In just the domain of computability, Hilbert's call for a general decision procedure was scuttled by Turing, using a diagonal argument. Indeed, Turing's halting problem can be straightforwardly viewed as a paradox, of the same type as others like the Liar and Curry's. This is confirmed here by reconstructing a halting predicate in a sequent calculus setting, thereby fitting a ``recipe' for paradox in [Ahmad, AJL 2022]. The usual range of possible solutions then apply, including especially substructural approaches. Bringing this work as a response to Brady's ``"Starting the Dismantling of Classical Mathematics" [Brady, AJL 2018], then, we assess his proposals to drop the law of excluded middle and other logical principles---asking whether this strategy avoids all versions of the halting paradox. Brady has well begun, in his idiom, the re-construction of mathematics; there is more yet to do.