Computability Theory

Pathway

Pages are grouped by how many dependency steps into this group they sit. Everything a page needs from this group appears above it.

1. Level 0

   2 pages
   • level 0Expander Graphs and Constraint Graphs31 results

     Normalized adjacency connects graph expansion with spectral estimates and walk probabilities.

     8 definitions, 14 lemmas, 2 propositions, 4 theorems, 2 corollaries, 1 false statementExamples & counterexamples →
   • level 0Formal Languages, Encodings, and Decision Problems18 results

     This page fixes the pre-machine vocabulary for the computability theory track: finite words over an alphabet, languages and their basic operations, reversal and induced…

     9 definitions, 6 lemmas, 1 proposition, 2 false statementsExamples & counterexamples →

2. Level 1

   4 pages
   • level 1Context-Free Grammars and Normal Forms20 results

     This page develops context-free grammars from derivations and parse trees through ambiguity, grammar simplification, Chomsky and Greibach normal forms, and the core closure constructions.

     9 definitions, 2 lemmas, 7 theorems, 2 false statementsExamples & counterexamples →
   • level 1Deterministic Finite Automata and Regular Languages16 results

     This page fixes deterministic finite automata as total machines over a fixed alphabet, proves the basic recursion law for the extended transition function, and then uses…

     5 definitions, 2 lemmas, 2 propositions, 4 theorems, 1 corollary, 2 false statementsExamples & counterexamples →
   • level 1Turing Machines, Configurations, and Computation16 results

     This page fixes the core Turing-machine semantics for the computability theory track: the deterministic one-tape model, right-infinite finite-support tapes, configurations…

     11 definitions, 2 lemmas, 1 proposition, 2 false statementsExamples & counterexamples →
   • level 1Turing-Machine Configuration Boundary Interface1 result

     This page fixes a raw Turing-machine tuple and its boundary conventions: finite-support tapes on natural-number cells, initial head position zero, and machine-relative accepting and rejecting states.

     1 definitionExamples & counterexamples →

3. Level 2

   5 pages
   • level 2Finite-Automata Transition and Determinisation Interfaces3 results

     Epsilon transitions can change the available states without consuming a letter.

     1 definition, 1 proposition, 1 theoremExamples & counterexamples →
   • level 2Myhill--Nerode Theory and DFA Minimization16 results

     This page develops the Myhill--Nerode point of view in two parallel forms.

     4 definitions, 4 lemmas, 4 theorems, 2 corollaries, 2 false statementsExamples & counterexamples →
   • level 2One-Tape Simulation Normal Forms3 results

     This page fixes a stay-put extension of the right-infinite, clamped-left-boundary machine model and proves its reduction to ordinary left/right machines.

     1 definition, 1 lemma, 1 theoremExamples & counterexamples →
   • level 2Pushdown Automata and Context-Free Languages17 results

     This page defines PDA runs and the two standard acceptance modes, proves the two machine-translation theorems connecting PDA's and context-free grammars, and then isolates…

     6 definitions, 2 lemmas, 3 propositions, 4 theorems, 2 false statementsExamples & counterexamples →
   • level 2Robust Machine Models and Universal Computation16 results

     This page records the standard robustness results around Turing computability.

     4 definitions, 3 lemmas, 6 theorems, 1 corollary, 1 false statement, 1 remarkExamples & counterexamples →

4. Level 3

   6 pages
   • level 3Context-Free Pumping, Ogden's Lemma, and Parsing16 results

     This page records the two standard pumping obstructions for context-free languages, uses them to isolate nonclosure phenomena, and then turns to parsing and decision…

     3 definitions, 2 lemmas, 6 theorems, 2 corollaries, 3 false statementsExamples & counterexamples →
   • level 3Decidable, Recognizable, and Enumerable Languages15 results

     This page separates three notions that are often conflated on first exposure: computability of total functions, recognizability of languages by machines that may diverge on…

     4 definitions, 1 lemma, 1 proposition, 7 theorems, 2 false statementsExamples & counterexamples →
   • level 3Effective Numberings, Reductions, Resources, and Randomness19 results

     This page fixes the interfaces needed to pass from literal finite programs to numerical computability and from finite random computations to complexity classes.

     11 definitions, 3 lemmas, 5 theoremsExamples & counterexamples →
   • level 3Nondeterministic Finite Automata and Subset Construction15 results

     This page develops epsilon-NFAs from their state-set semantics through the subset construction, then isolates three standard consequences: epsilon-moves can be eliminated…

     5 definitions, 2 lemmas, 2 propositions, 3 theorems, 1 corollary, 2 false statementsExamples & counterexamples →
   • level 3Primitive Recursive and Partial Computable Functions16 results

     This page develops the classical ladder from primitive recursion to partial recursion and then to machine computability.

     7 definitions, 1 lemma, 2 propositions, 4 theorems, 2 false statementsExamples & counterexamples →
   • level 3Resource Bounds and Machine Invariance14 results

     This page fixes the standard quantitative conventions of complexity theory: worst-case time and space, asymptotic comparison, constructible bounds, and the basic deterministic and nondeterministic resource classes.

     4 definitions, 3 lemmas, 2 propositions, 3 theorems, 2 false statementsExamples & counterexamples →

5. Level 4

   7 pages
   • level 4Acceptable Numberings, the s-m-n Theorem, and Recursion16 results

     This page fixes the standard numbering viewpoint on partial computable functions, isolates the single hard-wiring operation that makes a numbering acceptable, and then derives the full s mⁿ family from it.

     5 definitions, 1 lemma, 2 propositions, 5 theorems, 1 corollary, 2 false statementsExamples & counterexamples →
   • level 4Diagonalization and the Halting Problem15 results

     This page isolates the first sharp gap between recognition and decision.

     3 definitions, 1 lemma, 7 theorems, 2 corollaries, 2 false statementsExamples & counterexamples →
   • level 4Nondeterministic Recursive Padding and Time Separation7 results

     The distinction between shortest accepting time and all-branch running time matters throughout this page.

     1 definition, 5 lemmas, 1 theoremExamples & counterexamples →
   • level 4P, NP, coNP, and Polynomial Reductions17 results

     This page fixes the basic complexity classes and the reduction language that later completeness proofs rely on.

     8 definitions, 1 lemma, 3 propositions, 3 theorems, 2 false statementsExamples & counterexamples →
   • level 4Randomized Complexity and Amplification20 results

     This page fixes the standard probabilistic complexity classes and then separates three different amplification stories that are often blurred together: BPP majority…

     4 definitions, 3 lemmas, 7 theorems, 1 corollary, 2 examples, 1 counterexample, 2 false statementsExamples & counterexamples →
   • level 4Regular Expressions and Kleene's Theorem16 results

     This page separates regular-expression syntax from its language denotation, builds the two automata-conversion directions behind Kleene's theorem, and then packages three…

     5 definitions, 2 lemmas, 7 theorems, 2 false statementsExamples & counterexamples →
   • level 4SAT Tableaux and Quantified-Space Completeness9 results

     This page builds SAT completeness from a fixed binary formula parser and a local computation tableau.

     3 definitions, 3 lemmas, 3 theoremsExamples & counterexamples →

6. Level 5

   6 pages
   • level 5Computable Reductions and Rice's Theorem16 results

     This page introduces computable many-one reducibility as the basic comparison tool for undecidable problems, proves its first transfer theorems, and places A TM as the canonical c.e.-complete language.

     4 definitions, 3 lemmas, 2 propositions, 4 theorems, 1 corollary, 2 false statementsExamples & counterexamples →
   • level 5Interactive Proof Systems and Public Coins16 results

     Polynomially bounded interaction gives the verifier random access to evidence without imposing any resource bound on the prover.

     6 definitions, 4 lemmas, 1 proposition, 3 theorems, 2 false statementsExamples & counterexamples →
   • level 5Kolmogorov Complexity and Algorithmic Randomness23 results

     Complexity depends on a chosen optimal machine up to an additive constant.

     9 definitions, 4 lemmas, 8 theorems, 2 false statementsExamples & counterexamples →
   • level 5Space Complexity, Savitch's Theorem, and TQBF20 results

     This page isolates the space-bounded side of complexity theory.

     6 definitions, 4 lemmas, 1 proposition, 4 theorems, 1 corollary, 2 examples, 1 counterexample, 1 false statementExamples & counterexamples →
   • level 5The Arithmetical Hierarchy and Post's Theorem18 results

     This page relates finite alternations of arithmetic quantifiers to finite iterations of oracle computation.

     5 definitions, 4 lemmas, 6 theorems, 1 corollary, 2 false statementsExamples & counterexamples →
   • level 5The Cook--Levin Theorem16 results

     This page localizes SAT and then proves the Cook-Levin theorem by encoding one polynomially bounded nondeterministic computation branch as a bounded tableau.

     4 definitions, 7 lemmas, 1 proposition, 2 theorems, 2 false statementsExamples & counterexamples →

7. Level 6

   6 pages
   • level 6Arithmetization and the Sum-Check Protocol24 results

     Formula gates turn Boolean values into field polynomials. Boolean-cube interpolation then supplies multilinear extensions and explicit full-table evaluators. Sum-check…

     6 definitions, 10 lemmas, 1 proposition, 4 theorems, 1 corollary, 1 false statement, 1 remarkExamples & counterexamples →
   • level 6Classical NP-Completeness Reductions19 results

     This page records the standard web of classical polynomial-time reductions that propagates NP-completeness outward from 3-SAT.

     6 definitions, 8 theorems, 3 corollaries, 2 false statementsExamples & counterexamples →
   • level 6Counting Complexity and Sharp-P17 results

     This draft page develops the assigned conventions and keeps every resource, type, and quantifier explicit.

     6 definitions, 1 lemma, 4 propositions, 3 theorems, 1 corollary, 2 false statementsExamples & counterexamples →
   • level 6Oracle Computability, the Jump, and Turing Degrees23 results

     An oracle is queried one bit at a time, but it changes which sets a fixed finite program can decide.

     8 definitions, 5 lemmas, 1 proposition, 6 theorems, 1 corollary, 2 false statementsExamples & counterexamples →
   • level 6Post Correspondence and Language Undecidability15 results

     This page follows the standard undecidability spine through Post correspondence.

     3 definitions, 2 lemmas, 1 proposition, 7 theorems, 2 false statementsExamples & counterexamples →
   • level 6Time and Space Hierarchy Theorems20 results

     The hierarchy theorems are quantitative diagonal arguments: clocks reserve universal-simulation overhead, while a configuration cap forces a space diagonalizer to halt.

     3 definitions, 8 lemmas, 1 proposition, 5 theorems, 2 corollaries, 1 false statementExamples & counterexamples →

8. Level 7

   2 pages
   • level 7Logarithmic Space, NL, and Reachability19 results

     This page fixes the uncharged read-only-input convention for logarithmic work space, develops configuration-graph reductions and directed reachability, and then proves the two central closure results.

     7 definitions, 5 lemmas, 5 theorems, 1 corollary, 1 false statementExamples & counterexamples →
   • level 7The IP = PSPACE Theorem20 results

     This page proves IP=PSPACE by arithmetizing quantified Boolean formulas.

     3 definitions, 10 lemmas, 4 theorems, 1 corollary, 2 false statementsExamples & counterexamples →

9. Level 8

   1 page
   • level 8Boolean Circuits and Nonuniform Complexity16 results

     This draft page develops the assigned conventions and keeps every resource, type, and quantifier explicit.

     6 definitions, 1 lemma, 1 proposition, 6 theorems, 2 false statementsExamples & counterexamples →

10. Level 9

    2 pages
    • level 9Gap Amplification and Assignment Testing31 results

      This page proves the constraint-graph gap-amplification step and develops the code and tester ingredients needed for assignment testing.

      9 definitions, 17 lemmas, 4 theorems, 1 false statementExamples & counterexamples →
    • level 9The Polynomial Hierarchy and Relativization25 results

      Polynomially bounded quantifiers give a hierarchy of decision classes.

      6 definitions, 7 lemmas, 3 propositions, 5 theorems, 2 corollaries, 1 false statement, 1 remarkExamples & counterexamples →

11. Level 10

    1 page
    • level 10Alphabet Reduction and the PCP Theorem34 results

      The PCP theorem gives an alternative way to verify an NP certificate: a polynomial-time verifier reads a fixed proof string at only a constant number of locations chosen with O(log n) random bits.

      8 definitions, 18 lemmas, 6 theorems, 2 false statementsExamples & counterexamples →

12. Level 11

    1 page
    • level 11Approximation Algorithms and Gap Reductions22 results

      This page develops the finite-instance model of optimization problems and the value-inequality definition of an approximation ratio, together with the PTAS, FPTAS and locally defined APX classes.

      8 definitions, 6 lemmas, 7 theorems, 1 false statementExamples & counterexamples →