Project Page Index Table of Contents
    • Equivalence of Both Definitions
  • Arithmetical Hierarchy
    • Arithmetical Hierarchy in First-Order Arithmetic
  • Prenex Normal Form
  • Axioms for synthetic computability
    • Synthetic Church's thesis
  • Halting problems
    • Continuity
    • Constructions
  • Kleene trees
    • Omniscience principles as axioms on trees
    • WKL
    • WKL equivalences
  • CT in relation to other axioms
    • Provable choice axioms
    • Extensionality axioms
    • Classical logical axioms
    • Axioms of russian constructivism
    • Choice axioms
    • Brouwer's intuitionism
    • Arithmetical Hierarchy in Type Theory
  • Kleene-Post Theorem
  • Post's Theorem
  • Turing Jump
    • Enumerating Oracle Machines
    • Synthetic Turing Jump
    • Finite types
    • Infinite types and predicates
  • Decidability and Enumerability
    • Decidability
      • Discrete types
    • Enumerability
      • Enumerable types
    • List enumerability
    • Definitions
    • Pre-order properties
    • Semi-decidability
  • Reducibility
    • Many-one reducibility
    • One-one reducibility
    • Truth-table reducibility
    • Total Turing reducibility
    • Extensional dialogue trees
    • Oracle Functionals and Turing Reducibility
    • Lemmas about extensional dialogue trees
      • Interrogations with accumulator argument E
      • Stalling interrogations with silent steps
    • Trees give rise to partial functions
    • Closure properties of Oracle computability
    • Lemmas about Turing reducibility
    • Central results regarding Turing reducibility
Generated by coqdoc and improved with CoqdocJS