Schemata, Cyclic Proofs and Herbrand Systems
2026-06-22 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors explore a way to represent infinite sequences of mathematical proofs using something called proof schemata, which avoid traditional induction steps. They create a new kind of proof schema based on point transition systems that can handle special formulas called Herbrand systems. This approach can express Herbrand's theorem for these infinite proofs and connects to another proof technique called cyclic proofs by showing how to convert between them. Finally, the authors demonstrate that their method can prove a statement known as the 2-Hydra, which some other proof systems cannot.
Inductive proofProof schemaHerbrand's theoremSkolemizationQuantified formulaCyclic proofPoint transition systemHerbrand system2-HydraLKID
Authors
Alexander Leitsch, Anela Lolic, Stella Mahler
Abstract
Inductive proofs can be represented by proof schemata, a formalism that represents infinite sequences of proofs by recursive definitions. Since proof schemata avoid the explicit application of induction rules, they admit novel applications, one of which is the realization of Herbrand's theorem in the presence of induction. In this paper, we develop a new type of proof schema based on point transition systems. For skolemized proof schemata without quantified cuts, so-called Herbrand systems, that is, schemata of Herbrand instances of quantified formulas, can be computed. Herbrand systems also allow the representation of schemata of Herbrand sequents, thereby realizing Herbrand's theorem for proof schemata. We compare proof schemata with cyclic proofs and define a transformation from a large class of cyclic proofs to proof schemata. Finally, we show that proof schemata based on point transition systems are capable of proving the 2-Hydra statement, a well-known example that is provable by the cyclic proof system CLKIDωbut not in LKID.