Abstract

Herbrand's theorem provides constructive content to classical logic. Given an existentially quantified and provable statement, the theorem provides a valid finite disjunction of formulas substituting ground terms for the bound variables. This can be seen as a weaker form of the existence property for intuitionistic logic, in which for any provable existentially quantified formula one can find concrete witnesses for the bound variables. The standard proof of Herbrand's theorem uses cut elimination. In recent work by Afshari, Hetzl and Leigh, a direct interpretation of classical sequent calculus proofs in terms of so-called higher-order recursion schemes is given, in order to directly compute a Herbrand disjunction from a given proof (cut-free or not). This can be seen as a model of the computational content of a proof in classical sequent calculus. As a model of computation, it is however rather weak in the sense that no actual recursion takes place - as expected, since first-order logic has no built-in means to make recursive definitions. In order to extend the expressive power of this computational interpretation of classical logic, we therefore propose to consider cyclic (or, non-wellfounded) sequent calculus proofs for first-order logic extended with inductively defined predicates in the style of Martin-Löf, following an approach of Brotherston and Simpson. In this talk I will sketch how this framework can be set up, and present some simple applications. The talk is based on ongoing joint work with Bahareh Afshari and Graham Leigh.