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.
Texts
- cutland1980-computability
- https://www.cl.cam.ac.uk/teaching/1112/CompTheory/comt-notes.pdf
- 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
General terms
- Algorithm (aka. effective procedure)
- Computation (execution of a series of instructions)
- Enumerability and effective listings
- Diagonalization arguments
- Uncomputability, including the Halting Problem and productivity arguments
- 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
- Decidability
Turing machines
Register machines
- Abacus machines
- Register machines
- Unlimited register machine (URM)
- URM-computable functions
- Unbounded minimization
- Partial recursive functions
- Primitive Recursion
- Kleene’s Normal Form Theorem
Lambda calculus
- Lambda calculus
- Lambda definability
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