Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Cyclic Proofs for iGL via Corecursion

Borja Sierra Miranda

TL;DR

This work addresses the problem of relating a standard calculus for $\textup{i}\mathsf{GL}$ to a cyclic proof system, extending cyclic proof techniques to the intuitionistic Gödel–Löb setting. It adopts a coalgebraic, corecursive framework to construct translations from finitary proofs to non-wellfounded and cyclic proofs, and proves a precise equivalence between $\vdash_{\textup{i}\mathsf{GL}} S$ and $\vdash_{\textup{i}\mathsf{K4}_\circ} S$ via a two-way translation built from admissible rules like contraction and Löb. The main contributions are (i) an alternative corecursive translation-based proof of equivalence, (ii) a careful treatment of progress conditions ensuring soundness, and (iii) a structural bridge between finite acyclic and cyclic proofs for the $\textup{i}\mathsf{GL}$ calculus. This work enhances understanding of cyclic proof systems for logics with fixpoints and demonstrates a robust method to derive cyclic systems from standard calculi, with potential applicability to other intuitionistic modal logics.

Abstract

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.

Cyclic Proofs for iGL via Corecursion

TL;DR

This work addresses the problem of relating a standard calculus for to a cyclic proof system, extending cyclic proof techniques to the intuitionistic Gödel–Löb setting. It adopts a coalgebraic, corecursive framework to construct translations from finitary proofs to non-wellfounded and cyclic proofs, and proves a precise equivalence between and via a two-way translation built from admissible rules like contraction and Löb. The main contributions are (i) an alternative corecursive translation-based proof of equivalence, (ii) a careful treatment of progress conditions ensuring soundness, and (iii) a structural bridge between finite acyclic and cyclic proofs for the calculus. This work enhances understanding of cyclic proof systems for logics with fixpoints and demonstrates a robust method to derive cyclic systems from standard calculi, with potential applicability to other intuitionistic modal logics.

Abstract

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.
Paper Structure (7 sections, 6 theorems, 17 equations)

This paper contains 7 sections, 6 theorems, 17 equations.

Table of Contents

  1. Introduction
  2. Algebras and Coalgebras: (co)recursion
  3. Non-wellfounded and cyclic proofs
  4. On the need of progress
  5. Infinitary Proof Translation
  6. From finitary to cyclic, and vice versa
  7. Conclusion

Key Result

Lemma 7

$(\mathbb{T},\textsf{destruct})$ is the final coalgebra of $\mathcal{T}_L$ and $(\mathbb{T}^{<\omega},\textsf{construct})$ is the initial algebra of $\mathcal{T}_L$.

Theorems & Definitions (20)

  • Definition 1
  • Definition 2
  • Definition 3: Algebra/Coalgebra
  • Definition 4: Recursion/Corecursion
  • Definition 5: Tree endofunctor
  • Definition 6
  • Lemma 7
  • Definition 8
  • Definition 9
  • Definition 10
  • ...and 10 more