A Case against Stephen Kleene’s Incomputability

In Mathematical Logic (1967), Stephen Kleene addresses a central activity of software engineering through his introduction of tally-based Turing machines. Yet in doing so, he inadvertently builds a subtle form of impredicativity into his theory: he implicitly defines the semantics of Turing computability by appealing to the very construct—the Turing machine—whose legitimacy is simultaneously under examination. Stewart Shapiro, in Acceptable Notation, draws attention to this tension by uncovering the non-mathematical assumptions that tend to enter Kleene-style computability proofs, ultimately grounding his critique in what he terms "an extended version of Church's thesis." In this paper, we revisit Shapiro's concerns but shift the focus to incomputability. We argue that Kleene's framework relies on a latent assumption that complicates the contemporary presentation of the Halting Problem. Specifically, Kleene begins with a notation-dependent foundation: his tally-based Turing machines provide genuine evidence of a limitation internal to that particular representational system. However, he then moves rapidly from this narrow result to a broad, notation-independent claim of incomputability. Our critique is that Kleene's account lacks the necessary conceptual transition from notation-dependent reasoning to notation-independent conclusions. Once this gap is made explicit, what remains is not a universal incomputability theorem but an incomputability claim relative to a specific representational choice. This reframing invites a more careful reconsideration of how the Halting Problem—and, more generally, the notion of incomputability—should be understood within the contemporary sciences.