Circular Proofs

Origin. Brotherston, Simpson (2007). Proofs with cycles. Infinite descent for induction. Finitely representable infinite proofs. Foundation for cyclic proof theory.

Models. Proof graphs, not trees. Back-links create cycles. Soundness via trace conditions. Captures induction without explicit induction rules.

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.

Soundness condition: Every infinite path has infinitely progressing trace. "Progress" = inductive measure decreases.

Example (Peano arithmetic): Prove: ∀x. P(x) Use cycle: P(n) derives P(S(n)) derives P(n)... Progress: n increases, trace on P descends.

μ-calculus proofs: Back-links correspond to fixed points. Greatest fixed point: infinite unfolding. Trace through μ-formula.

Induction capture: Explicit induction rule replaceable by cycles. Cyclic proofs = inductive proofs (for many systems).

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Link	Derivation step
↩	U+21A9	Back-link	Cycle
μ	U+03BC	Mu	Fixed point
trace	—	Trace	Formula path

Metatheory. Soundness via infinite descent. Equivalence to inductive systems (many cases). Cut elimination for cycles. Decidability varies.

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

Limitations. Global soundness condition. Trace finding complex. Not all induction captured. Implementation challenges.