Herbrand schemes for cyclic proofs
Sebastian Enqvist
Authors: Bahareh Afshari, Sebastian Enqvist and Graham Leigh
Recent work by Afshari et al. introduce a notion of Herbrand schemes for first-order logic by associating a higher-order recursion scheme to a sequent calculus proof. Calculating the language of associated Herbrand schemes directly yields Herbrand disjunctions. As such, these schemes can be seen as programs extracted from proofs. Here, this computational interpretation is explored further by removing the restriction of acyclicity from Herbrand schemes which amounts to admitting recursively defined programs. It is shown that the notion of proof corresponding to these generalised Herbrand schemes is cyclic proofs, considered here in the context of classical theories of inductively defined predicates. In particular, for proofs with end sequents of a form generalising the notion of \(\Sigma_1\)-sequents in the first-order setting, Herbrand schemes derive a language of witnesses from cyclic proofs via a simulation of non-wellfounded cut elimination. Thus Herbrand schemes can be used to directly compute the “Herbrand content” of cyclic proofs. This is based on unpublished work, for which a preprint is available at: https://eprints.illc.uva.nl/id/eprint/2292/1/Herbrand_schemes_for_cyclic_proofs.pdf