Bounded Arithmetic in Free Logic

TL;DR

This paper reformulates Buss' bounded arithmetic theories using free logic, showing they are easier to analyze and interpret, and explores their consistency and interpretability properties to address open questions about hierarchy collapse.

Contribution

It introduces a free logic-based reformulation of Buss' theories and demonstrates interpretability and consistency results, providing new tools to analyze the hierarchy of bounded arithmetic.

Findings

Buss' theories prove the consistency of certain induction-free fragments.

Theories in the new formulation can interpret Buss' hierarchy.

Investigation of G"odel sentences suggests hierarchy separation.

Abstract

One of the central open questions in bounded arithmetic is whether Buss' hierarchy of theories of bounded arithmetic collapses or not. In this paper, we reformulate Buss' theories using free logic and conjecture that such theories are easier to handle. To show this, we first prove that Buss' theories prove consistencies of induction-free fragments of our theories whose formulae have bounded complexity. Next, we prove that although our theories are based on an apparently weaker logic, we can interpret theories in Buss' hierarchy by our theories using a simple translation. Finally, we investigate finitistic G\"odel sentences in our systems in the hope of proving that a theory in a lower level of Buss' hierarchy cannot prove consistency of induction-free fragments of our theories whose formulae have higher complexity.