Arithmetic with Limited Exponentiation

TL;DR

The paper explores a hierarchy of weak logical theories related to limited exponentiation, analyzing their properties and interpretability within bounded arithmetic, revealing insights into their computational and foundational strength.

Contribution

It introduces and analyzes a hierarchy of weak theories with limited exponentiation, showing their interpretability in bounded quantifier arithmetic and exploring their computational implications.

Findings

Theories include fixed k-fold exponential time computation.

Weak K"onig's Lemma is interpretable within these theories.

Theories encompass higher-level function types with extensionality and comprehension.

Abstract

We present and analyze a natural hierarchy of weak theories, develop analysis in them, and show that they are interpretable in bounded quantifier arithmetic $\text{I}\Delta_0$ (and hence in Robinson arithmetic Q). The strongest theories include computation corresponding to k-fold exponential (fixed k) time, Weak K\"onig's Lemma, and an arbitrary but fixed number of higher level function types with extensionality, recursive comprehension, and quantifier-free axiom of choice. We also explain why interpretability in $\text{I}\Delta_0$ is so rich, and how to get below it.