Circular Proofs

Origin. Brotherston and Simpson (2007, 2011) gave the systematic treatment: CLKID^ω, a cyclic calculus for first-order logic with inductive definitions, set against LKID, the same logic with explicit induction rules. The technique has older roots — Niwiński and Walukiewicz (1996) used tableaux with a trace condition for the μ-calculus, and Santocanale (2002) gave circular proofs a categorical semantics. The governing idea is Fermat's infinite descent: a cycle is admissible when traversing it forever would force an infinite decrease.

Models. A proof is a finite graph rather than a tree, some of whose leaves are back-links to sequents occurring earlier on the same branch. The graph denotes its infinite unfolding, and validity is a condition on that unfolding rather than on any single step. Local correctness of every rule is necessary and not sufficient: soundness is global.

Formalism.

Pre-proof: Finite directed graph of sequents. Leaves: axioms or back-links. Back-link: edge to earlier sequent.

Derivation tree unfolding: Infinite tree by unfolding cycles. Must be valid infinite derivation.

Trace: Sequence of formula occurrences along path. Track principal formula through cycle.

Global trace condition: Every infinite path carries a trace progressing infinitely often. "Progress" = a strict descendant of an inductive predicate. Condition on paths, not on nodes.

Checking the condition: Paths and progressing traces are ω-regular. Recognized by Büchi automata. Condition = an inclusion between them. Decidable by complementation.

Example (induction as descent): Goal: N(x) ⊢ P(x). Case split on N(x): x = 0, or x = S(y) with N(y). Base case closes; step case back-links to the root. Trace N(x) → N(y) progresses at the case split. No induction rule is used.

μ-calculus proofs: Back-links correspond to fixed-point unfoldings. A trace progresses when a least fixed point is unfolded. Branch succeeds when some trace progresses infinitely often.

Induction capture: Every LKID proof translates into a cyclic one. The converse fails in general. Holds when arithmetic is available.

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Rightwards arrow / Edge	An inference step, or a step along a trace
↩	U+21A9	Hooked arrow / Back-link	Edge from a leaf to an earlier sequent on the same branch
μ	U+03BC	Mu	Least fixed point; unfolding one is what makes a trace progress
ν	U+03BD	Nu	Greatest fixed point
ω	U+03C9	Omega	Superscript in CLKID^ω; also the length of an infinite branch
⊢	U+22A2	Turnstile	Sequents are the nodes of the graph
∀	U+2200	Universal quantifier	The statement proved by descent
trace	—	Trace	A sequence of formula occurrences following one branch
CLKID^ω	—	Cyclic calculus	LK with inductive definitions and back-links
LKID	—	Inductive calculus	The same logic with explicit induction rules
N, P	—	Predicates	An inductive predicate and the property proved of it

Metatheory. The global trace condition is ω-regular, which is what makes cyclic proof workable: the branches of a pre-proof and its progressing traces are recognized by Büchi automata, and the condition amounts to an inclusion between them, decidable by complementation. Brotherston and Simpson (2007) proved CLKID^ω sound and showed that every LKID proof translates into a cyclic one, then conjectured the converse; Berardi and Tatsuta (2017) refuted it, exhibiting a statement about hydras provable cyclically but not by the explicit induction rules of LKID. Arithmetic changes the picture: Simpson (2017) proved that cyclic arithmetic and Peano arithmetic prove the same theorems, the simulation running through a formalized soundness argument rather than through constructed invariants. Cut elimination is settled only in fragments — Fortier and Santocanale (2013) obtained it for circular proofs over fixed points.

Applies to. Arithmetic. μ-calculus. Separation logic with induction. Program verification. Infinite structures.

Limitations. Soundness does not compose. The trace condition is a property of the entire graph, so two sound cyclic proofs cannot simply be pasted together, and this is exactly what makes cut elimination hard: eliminating a cut rewrites the graph and can destroy the progress that justified it. No general cut-elimination theorem for cyclic systems is available. Checking the condition is decidable but costly, resting on Büchi complementation, and proof search must maintain a global invariant rather than a local one, which is why implementations restrict the shape of permitted cycles. Equivalence with inductive proof is not a general fact but depends on the ambient theory, holding for arithmetic and failing for LKID. And a cyclic proof exhibits no induction invariant: it certifies the theorem without yielding the lemma.