Cyclic and Inductive Calculi are equivalent

TL;DR

This paper proves the equivalence between cyclic and inductive calculi in first-order logic by showing that each inductive proof can be translated into a cyclic proof and vice versa, unifying two reasoning frameworks.

Contribution

It establishes the first formal proof that cyclic and inductive calculi are equivalent, complementing previous work that showed cyclic calculus is at least as powerful as inductive calculus.

Findings

Cyclic and inductive calculi are mutually translatable.

First-order cyclic calculus can simulate inductive proofs.

The equivalence unifies different reasoning approaches in logic.

Abstract

Brotherston and Simpson [citation] have formalized and investigated cyclic reasoning, reaching the important conclusion that it is at least as powerful as inductive reasoning (specifically, they showed that each inductive proof can be translated into a cyclic proof). We add to their investigation by proving the converse of this result, namely that each inductive proof can be translated into an inductive one. This, in effect, establishes the equivalence between first order cyclic and inductive calculi.