Induction rules in bounded arithmetic (Q2309507)

From MaRDI portal





scientific article; zbMATH DE number 7184243
Language Label Description Also known as
default for all languages
No label defined
    English
    Induction rules in bounded arithmetic
    scientific article; zbMATH DE number 7184243

      Statements

      Induction rules in bounded arithmetic (English)
      0 references
      0 references
      1 April 2020
      0 references
      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.
      0 references
      bounded arithmetic
      0 references
      parameter-free induction
      0 references
      induction rule
      0 references
      partial conservativity
      0 references
      reflection principle
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references

      Identifiers