Synthetic computability without choice

In synthetic computability, pioneered by Richman, Bridges, and Bauer, one develops computability theory without an explicit model of computation. This is enabled by assuming an axiom equivalent to postulating a function φ to be universal for the space N→N (CTφ , a consequence of the constructivist axiom CT), Markov’s principle, and at least the axiom of countable choice. Assuming CT and countable choice invalidates the law of excluded middle, thereby also invalidating classical intuitions prevalent in textbooks on computability. On the other hand, results like Rice’s theorem are not provable without a form of choice.

In contrast to existing work, we base our investigations in constructive type theory with a separate, impredicative universe of propositions where countable choice does not hold and thus a priori CTφ and the law of excluded middle seem to be consistent. We introduce various parametric strengthenings of CTφ , which are equivalent to assuming CTφ and an Snm operator for φ like in the Snm theorem. The strengthened axioms allow developing synthetic computability theory without choice. I will discuss 3 applications of the axioms: Rice's theorem, Post's construction of simple and hypersimple predicates, and an uncomputability proof Kolmogorov complexity.

Notably, the proposed parametric axioms seem to be not in conflict with classical intuitions since they are consequences of the traditional analytic form of CT.

hosted by