Proof schemata are finite representations of recursively defined families of proofs. They provide a framework for formalising and analysing inductive arguments while retaining access, at the instance level, to methods from classical proof theory. At the same time, their recursive structure supports schematic methods, including schematic CERES and the extraction of so-called Herbrand systems, which generalise Herbrand’s theorem to the schematic setting.

In this talk, I will explore the relationship between proof schemata and the cyclic proof system CLKIDω of Brotherston and Simpson [1]. Using an extension of proof schemata based on point transition systems, a substantial class of cyclic proofs can be translated into the schematic framework. The expressive strength of this extension is illustrated by translating the 2-Hydra proof of Berardi and Tatsuta [2] into a proof schema. The example is particularly significant because the 2-Hydra statement is provable in CLKIDω but not in the corresponding finitary inductive system LKID.

  1. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177–1216, 2011.
  2. Stefano Berardi and Makoto Tatsuta. Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proofs. Logical Methods in Computer Science, 15, 2019.