Herbrand's theorem exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula to that of a finite disjunction. More generally, it reduces 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, we show that Herbrand's theorem in its general form can be elegantly stated and proved as a theorem in the framework of concurrent games, a denotational semantics designed to faithfully represent causality and independence in concurrent systems. Closely related to expansion trees, the causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers. As furthermore these strategies can be composed we are able to interpret classical sequent proofs, yielding a compositional proof of Herbrand's theorem.