README⤓ .txt 2026-07-17T121634.146 000000000000808 The metatheory of computation: what functions and sets are effectively computable, decidable, or enumerable, and how the undecidable problems are stratified by degree and hierarchy. It is the recursion-theoretic branch of mathematical logic, standing alongside model theory and proof theory.
Algorithmic Randomness⤓ .md 2026-07-15T230424.000 000000000031080 Per Martin-Löf, "The definition of random sequences" (1966), giving the first definition that survived. Levin and Chaitin gave the incompressibility characterization (1970s); Schnorr gave the martingale one (1971). Developed by Kučera, Solovay, Downey, Hirschfeldt, Nies. The subject is the recursion theory of what a random object is.
Arithmetical Hierarchy⤓ .md 2026-07-17T120407.600 000000000000928 Kleene, Mostowski (1940s). Classify sets of naturals by the number of alternating quantifiers over a recursive matrix. The analytical hierarchy extends this to second-order quantifiers.
Bishop-Style Constructive⤓ .md 2026-07-17T120407.600 000000000000944 Errett Bishop (1967). Foundations of Constructive Analysis. Minimal philosophy. Compatible with classical. Foundation of constructive analysis.
Choice Sequences⤓ .md 2026-07-15T072104.000 000000000014776 Brouwer (1920s). Intuitionist foundations. Sequences created by free choice. Not predetermined. Foundation for Brouwerian analysis.
Church-Turing Thesis⤓ .md 2026-07-17T120407.600 000000000000912 Church (1936), Turing (1936), Kleene. Identifies the informal notion of effective calculability with a formal model of computation. A thesis, not a theorem: it links intuition to mathematics.
Computability Theory⤓ .md 2026-07-17T120407.600 000000000000912 Gödel, Church, Turing, Kleene, Post (1930s). Formalize effective calculability. Several independently proposed models coincide. Foundation of the theory of the computable and the fourth branch of mathematical logic.
Computable Analysis⤓ .md 2026-07-15T235628.000 000000000017480 Turing's computable reals (1936); Grzegorczyk (1955) and Lacombe (1955) independently gave the computable real functions; Pour-El and Richards, Computability in Analysis and Physics (1989); Weihrauch, Computable Analysis (2000), which established TTE as the standard framework. Computability on reals. TTE (Type-2 Theory of Effectivity). Computable real functions. Foundation of exact real computation.
Halting Problem⤓ .md 2026-07-17T120407.600 000000000000872 Turing (1936). The first proved-undecidable problem. Established by diagonalization, it grounds undecidability throughout logic and computer science.
Higher Recursion Theory⤓ .md 2026-07-17T120407.600 000000000000936 Kleene, Kreisel, Sacks (1960s-70s). Generalizes computability beyond the finite: to recursive ordinals, admissible sets, and higher types. Recursion theory meets definability.
Kolmogorov Complexity⤓ .md 2026-07-17T120407.600 000000000000920 Solomonoff (1960), Kolmogorov (1965), Chaitin (1966). Algorithmic information theory. Measures the information content of an individual object by its shortest description.
Markov Principle⤓ .md 2026-07-17T120407.600 000000000000824 A.A. Markov (1950s). Russian constructive mathematics. Computable sequences. Church's thesis. Foundation of recursive mathematics.
Realizability⤓ .md 2026-07-15T055807.000 000000000022232 Kleene introduced realizability (1945) to interpret intuitionistic logic via computable functions. A formula is true if "realized" by a computation. Connects constructive logic to computability theory. Extended by Kreisel, Troelstra, and others. Foundation for program extraction from proofs.
Recursive Functions⤓ .md 2026-07-17T120407.600 000000000000904 Dedekind and Skolem formalized primitive recursion; Gödel, Herbrand, and Kleene defined the general recursive functions (1930s). A syntactic characterization of the computable number-theoretic functions.
Recursively Enumerable Sets⤓ .md 2026-07-17T120407.600 000000000000968 Kleene, Post (1944). The semi-decidable sets and their structure. Post's problem and the priority method (Friedberg, Muchnik, 1956) opened the study of r.e. degrees.
Rice's Theorem⤓ .md 2026-07-17T120407.600 000000000000864 Rice (1953). Sweeping undecidability result: every non-trivial semantic property of programs is undecidable. Generalizes the halting problem to all extensional properties.
Turing Degrees⤓ .md 2026-07-17T120407.600 000000000000864 Turing (1939) introduced oracle machines; Post, Kleene developed degrees of unsolvability. Structure of relative computability. Measures how uncomputable a set is.
Zero-One Laws⤓ .md 2026-07-16T001339.000 000000000035424 Glebskii, Kogan, Liogon'kii, and Talanov (1969) in the Soviet literature and Ronald Fagin, "Probabilities on finite models" (Journal of Symbolic Logic, 1976), independently. Compton, Kolaitis, and Vardi extended the subject through the 1980s and 90s; Shelah and Spencer (1988) settled the sparse random-graph case.
CRITERIA⤓ .txt 2026-07-17T120407.600 000000000000824 Required: At least one of the following: - A model or thesis of effective computation (recursive functions, Turing machines, Church-Turing) - A result about decidability or its failure (halting problem, Rice's theorem, r.e. sets) - A structure of the non-computable (Turing degrees, arithmetical hierarchy, higher recursion, Kolmogorov complexity)