Computational Flows in Arithmetic

TL;DR

This paper develops a theory of computational flows to interpret bounded arithmetic theories and extract computational content from proofs, extending to unbounded theories and capturing their NP search problems.

Contribution

It introduces a formal framework for computational flows and applies it to decompose proofs in bounded and unbounded arithmetic theories, linking them to computational problems.

Findings

Decomposition of proofs into computational reductions

Interpretation of bounded theories via computational flows

Extension to unbounded theories and NP search problems

Abstract

A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this paper we will develop a theory for these computational flows and we will use it to make a sound and complete interpretation for bounded theories of arithmetic. This property helps us to decompose a first order arithmetical proof to a sequence of computational reductions by which we can extract the computational content of low complexity statements in some bounded theories of arithmetic such as $I\Delta_0$, $T^k_n$, $I\Delta_0+EXP$ and $PRA$. In the last section, by generalizing term-length flows to ordinal-length flows, we will extend our investigation from bounded theories to strong unbounded ones such as $I\Sigma_n$ and $PA+TI(\alpha)$ and we will capture their total $NP$ search problems as a consequence.