constructive mathematics, realizability, computability propositions as types, proofs as programs, computational trinitarianism topos, homotopy topos type theory, homotopy type theory canonical form, univalence Bishop set, h-set decidable equality, decidable subset, inhabited set, subsingleton The arithmetical hierarchy or arithmetic hierarchy or Kleene–Mostowski hierarchy is a hierarchy used in computability theory to classify certain subsets of the natural numbers based upon the complexity of the first-order formulas that define them. decidability, which correspond to in the arithmetical hierarchy semidecidability, which correspond to in the arithmetical hierarchy Takayuki Kihara, The Arithmetical Hierarchy: A Realizability-Theoretic Perspective [arXiv:2410.15795] Wikipedia, Arithmetical hierarchy