Computability theory

Computability theory is the branch of mathematical logic that studies what can and cannot be computed by mechanical procedures — a field that exists because of the questions Alan Turing and Alonzo Church posed in 1936. Its central object is not the computer but the computable function: the class of functions for which there exists an algorithm that, given any input, will eventually halt and produce the correct output.

The field's foundational result is the existence of the non-computable. Turing's halting problem — the question of whether an arbitrary program will eventually halt or run forever — is itself undecidable: no algorithm can answer it for all possible inputs. This is not a technological limitation. It is a mathematical fact about the structure of formal systems, one that implies profound constraints on what automated reasoning can achieve. The undecidability of the halting problem extends to a vast landscape of undecidable questions in mathematics, logic, and formal verification.

Computability theory distinguishes sharply between decidability (a question can be answered by an algorithm that always halts), semidecidability (a correct answer can be verified when it exists, but incorrect cases may run forever), and undecidability (no algorithm suffices). These distinctions are not merely technical. They determine the boundary of what can be automated in theorem proving, program verification, and automated reasoning — fields that repeatedly rediscover the limits Turing established.

The modern significance of computability theory lies in its application to complexity theory — the study not of what is computable in principle but of what is computable in practice, given constraints on time and memory. The boundary between computability and complexity is the boundary between mathematical possibility and physical realizability. A function that is computable but requires more time than the age of the universe is computable in theory and impossible in practice.