Cyclic Proofs for iGL via Corecursion
Borja Sierra Miranda (Logic and Theory Group, University of Bern)
循环证明理论研究允许循环的证明。 这对于开发具有固定点运算符的逻辑的证明理论很有用:循环可以用来表示固定点的展开。 然而,这种循环字符并不是这种显式固定点独有的。 例如,帧具有Noetherian(相反有充分理由)条件的模态逻辑,例如GL(Goedel-Loeb逻辑),S4Grz(Grzegorczyk逻辑)和K4Grz也有循环证明系统。 特别是,Shamkanov引入了一个非良好和循环序列系统GL。 他通过证明翻译证明了这两个系统的等价性与一个循环有限系统。 为了从有限系统到非有根据的系统,他通过corecursion定义了翻译。 Iemhoff概括了Shamkanov的研究,当对于给定的模态逻辑证明系统,存在另一个模态逻辑证明系统,使得第一个中的证明相当于第二个中的循环证明。 在那里,她表明iGL,一个直觉版的GL,也有一个自然的循环证明系统。 我们提供iGL和循环式计算等效性的替代证明。
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 introduce...
