A compositional account of Herbrand's theorem via concurrent games

Pierre Clairambault ( ENS Lyon )

Herbrand's theorem, often regarded as a cornerstone of proof theory, exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula ∃x.φ(x) (with φ quantifier-free) to that of a finite disjunction φ(t₁) ∨ ... ∨ φ(tn). More generally, it gives a reduction of first-order validity to propositional validity, by understanding the structure of the assignment of first-order terms to existential quantifiers, and the causal dependency between quantifiers.

In this talk, I will show that Herbrand's theorem in its general form can be elegantly stated as a theorem in the framework of concurrent games. The causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers. Furthermore concurrent strategies can be composed, yielding a compositional proof of Herbrand's theorem, simply by interpreting classical sequent proofs in a well-chosen denotational model. I assume no prior knowledge of Herbrand's theorem or concurrent games.

This is joint work with Aurore Alcolei, Martin Hyland and Glynn Winskel.