Induction rules in bounded arithmetic

TL;DR

This paper investigates parameter-free induction schemes in bounded arithmetic, focusing on $\hat\Pi^b_i$ schemes, and explores their logical relationships, conservation properties, and separations.

Contribution

It introduces new results on the relationships and separations of parameter-free bounded arithmetic systems, especially $\hat\Pi^b_i$ schemes, including a novel witnessing theorem.

Findings

Inclusions and conservation results between systems

A new witnessing theorem for $T^i_2$ and $S^i_2$

Connections to reflection principles and system separations

Abstract

We study variants of Buss's theories of bounded arithmetic axiomatized by induction schemes disallowing the use of parameters, and closely related induction inference rules. We put particular emphasis on $\hat\Pi^b_i$ induction schemes, which were so far neglected in the literature. We present inclusions and conservation results between the systems (including a witnessing theorem for $T^i_2$ and $S^i_2$ of a new form), results on numbers of instances of the axioms or rules, connections to reflection principles for quantified propositional calculi, and separations between the systems.