8 papers
Cyclic proofs in the equational version of Primitive recursive arithmetic
Daniyar Shamkanov
In this brief note, we present a cyclic proof system developed specifically for the equational version of Primitive recursive arithmetic and establish the equivalence of the two sy…
(Non-)well-founded derivations in the provability logic
Daniyar Shamkanov
We examine cyclic, non-well-founded and well-founded derivations in the provability logic . While allowing cyclic derivations does not change the system, the non-well…
Fragments of arithmetic and cyclic proofs
Lev D. Beklemishev, Daniyar S. Shamkanov, Ivan N. Smirnov
We present an alternative cyclic proof system for Peano arithmetic that could be simpler than the existing ones and well-adapted both for proof analysis and for automatizing induct…
A realization theorem for the modal logic of transitive closure
Daniyar Shamkanov
We present a justification logic corresponding to the modal logic of transitive closure and establish a normal realization theorem relating these two systems. The re…
On structural proof theory of the modal logic K+ extended with infinitary derivations
Daniyar Shamkanov
We consider an extension of the modal logic of transitive closure K+ with some inifinitary derivations and present a sequent calculus for this extension, which allows non-well-foun…
Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs
Yury Savateev, Daniyar Shamkanov
We present a sequent calculus for the weak Grzegorczyk logic Go allowing non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elim…