Induction rules in bounded arithmetic

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

h a t P i_{i}^{b}

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_{2}^{i}

and

S_{2}^{i}

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.

Review text

The article is well organized and written. Two main results are presented, a conservation result, and a characterization of parameter-free induction axioms and rules involving an axiomatic extension of \(G_i\) proof system. The author purpose the study of a parameter-free version of Samuel Buss's theories proving that, for theories \(T\) of appropriate complexity, \(T + T^i_2 (T + S^i_2)\) is conservative over \(T + \hat\Sigma^b_i-(P)\mathrm{IND}^R \) and \( T + \hat\Pi^b_i-(P)\mathrm{IND}^R\) w.r.t. suitable classes of formulas, implying certain conservativity of \(T^i_2 (S^i_2)\) over \(\hat\Sigma^b_i-(P)\mathrm{IND}^-\) and \(\hat\Pi^b_i-(P)\mathrm{IND}^-\). Besides, considering the connection between bounded arithmetic and propositional proof system, the author present a characterization of parameter-free induction axioms and induction rules involving a \(G_i + \xi\) proof system, that is, using variants of reflection principles for fragments of quantified propositional calculi \(G_i\). Finally, some typos, on page 475, Observation 5.2, page 484, Theorem 5.20, and page 485, Corollary 5.23, the symbol \(\square\) does not correspond to the end of the paragraph.

Recommendations

Cites work

Cited in

(13)

This page was built for publication: Induction rules in bounded arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2309507)