This article is cited in 1 paper

Fragments of arithmetic and cyclic proofs

L. D. Beklemishev^a, D. S. Shamkanov^a, I. N. Smirnov<sup>abc

a</sup> Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russia
^b Ivannikov Institute for System Programming of the Russian Academy of Science, Moscow, Russia
^c Moscow Institute of Physics and Technology, Dolgoprudny, Moscow Region, Russia

Abstract: We define a new cyclic proof system for Peano arithmetic that is simpler than the existing ones and can be adapted for analysis of formal inference and for automatizing inductive proof search. We show how various traditional subsystems of Peano arithmetic defined by restricted forms of induction can be represented as fragments of the proposed system.
Bibliography: 45 titles.

Keywords: cyclic proofs, Peano arithmetic, induction.

MSC: Primary 03F03, 03F30; Secondary 03F07

Received: 10.02.2025 and 26.03.2025

DOI: 10.4213/sm10276

 English version: Sbornik: Mathematics, 2025, 216:10, 1339–1362

Bibliographic databases:

• 
• 
• 
•