Extending Primitive Recursion to Advanced Type Systems

What is it about?

Primitive recursion is the baseline of computability. We show that a collection of advanced type theories, in which not every function is primitive recursive, can be restricted in a straight-forward way to produce only primitive recursive functions using modern topos-theoretic techniques. This enables simplified approaches to reverse mathematics and formal verification.

Featured Image

Why is it important?

Knowing the strength of fragments of a logical system allows one to keep track of the minimal assumptions one needs to make in order to prove a theorem. The system whose fragments we consider is implemented in popular proof assistants such as Agda, and the proposed restriction is technically simple. This means that we lay the foundation for formally verified reverse mathematics. Furthermore, the proof of our result showcases a new way of using the modern technique known as synthetic Tait computability, hopefully inspiring further creative applications thereof.

Perspectives