Computability theory or recursion theory studies formal models of effective computation and the limits of algorithmic solvability. Its classical core includes enumerability, machine computation, recursive definitions, undecidability, and recursively enumerable sets. It also interacts closely with mathematical logic, especially through arithmetization, incompleteness, and realizability.
Abstract
The subject begins with concrete models of computation such as Turing machines and register or abacus machines, and with function-theoretic notions such as primitive recursion and minimization. It then studies negative results such as the Halting Problem and broader undecidability phenomena, before moving outward toward definability in arithmetic, incompleteness, degree theory, and categorical semantics.
Realizability gives one of the main bridges from classical computability to logic and type theory. Through partial combinatory algebras, assemblies, triposes, and the effective topos, computability theory also becomes part of categorical logic.
Texts
- cutland1980-computability
- boolos2007-computability-and-logic
- enderton2010-computability
- rogers1987-recursive-functions-and-effective-computability
- odifreddi1989-classical-recursion-theory
- soare1987-recursively-enumerable-sets-and-degrees
- cooper2004-computability-theory
- vanoosten2008-realizability
- longley2015-higher-order-computability
- troelstra1988-constructivism
Outline
Classical computability theory
- Enumerability and effective listings
- Diagonalization arguments
- Turing computability
- Uncomputability, including the Halting Problem and productivity arguments
- Abacus or register-machine computability
- Recursive functions, especially primitive recursion and minimization
- Recursive sets, recursive relations, and recursively enumerable sets
- Equivalent definitions of computability, including coding computations and universal machines
Computability in logic
- Syntax and semantics of first-order logic
- The Undecidability of first-order logic
- Arithmetization and Godel numbering
- Representability of recursive functions in arithmetic
- Incompleteness, indefinability, and consistency results
Further directions
- Normal forms, interpolation, and definability
- Second-order logic and arithmetical definability
- Nonstandard models of arithmetic
- Ramsey-theoretic and proof-theoretic applications
- Degree structures, forcing, and priority methods
Realizability and categorical semantics
- Partial combinatory algebras
- Assemblies and applicative morphisms
- Triposes and the tripos-to-topos construction
- The effective topos
- Synthetic computability and synthetic domain theory
- Variants such as modified, function, and relative realizability