Cyclic proof theory studies proofs where cycles are allowed. This is useful for developing proof theory for logics with fixpoint operators: cycles can be used to represent the unfolding of a fixpoint. However, this cyclic character is not unique to such explicit fixpoints. For example, modal logics whose frames have a Noetherian (conversely wellfounded) condition, such as GL (Goedel-Loeb logic), S4Grz (Grzegorczyk logic) and K4Grz also have cyclic proof systems. Particularly, Shamkanov introduces a non-wellfounded and a cyclic sequent system GL. He proves the equivalence of these two systems with an acyclic finite system via proof translations. In order to go from the finite system to the non-wellfounded system he defines the translation by corecursion. Iemhoff generalized the work of Shamkanov studying when, for a given modal logic proof system, there exists another modal logic proof system such that proofs in the first are equivalent to cyclic proofs in the second. There, she shows that iGL, an intuitionistic version of GL, also has a natural cyclic proof system. We provide an alternative proof of the equivalence of a standard calculus for iGL and a cyclic one.

翻译：循环证明理论研究允许循环存在的证明。这对于发展带有不动点算子的逻辑证明理论非常有用：循环可用于表示不动点的展开。然而，这种循环特性并非此类显式不动点所独有。例如，框架满足诺特（逆良基）条件的模态逻辑，如GL（哥德尔-勒布逻辑）、S4Grz（格热戈尔奇克逻辑）和K4Grz，同样具有循环证明系统。特别地，沙姆卡诺夫为GL引入了一个非良基的循环相继式系统，并通过证明转换证明了这两个系统与一个非循环有限系统的等价性。为了从有限系统转换到非良基系统，他利用余递归定义了转换规则。伊姆霍夫推广了沙姆卡诺夫的工作，研究对于给定的模态逻辑证明系统，何时存在另一个模态逻辑证明系统，使得前者的证明等价于后者的循环证明。她指出，直觉主义版本的GL（即iGL）同样具有自然的循环证明系统。本文为标准iGL演算与循环证明系统的等价性提供了一个替代证明。