Abstract
Herbrand's theorem, widely 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 firstorder purely existential formula to that of a finite disjunction. In the general case, it reduces firstorder validity to propositional validity, by understanding the structure of the assignment of firstorder terms to existential quantifiers, and the causal dependency between quantifiers. In this paper, 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, thereby exposing the concurrency underlying the computational content of classical proofs. The causal structure of concurrent strategies, paired with annotations by firstorder terms, is used to specify the dependency between quantifiers implicit in proofs. Furthermore concurrent strategies can be composed, yielding a compositional proof of Herbrand's theorem, simply by interpreting classical sequent proofs in a wellchosen denotational model.
Original language  English 

Title of host publication  27th EACSL Annual Conference on Computer Science Logic (CSL 2018) 
Editors  Dan R. Ghica, Achim Jung 
Place of Publication  Dagstuhl, Germany 
Pages  5:15:22 
Number of pages  22 
DOIs  
Publication status  Published  29 Aug 2018 
Event  27th Annual EACSL Conference Computer Science Logic, CSL 2018  Birmingham, United Kingdom Duration: 4 Sept 2018 → 7 Sept 2018 
Publication series
Name  Leibniz International Proceedings in Informatics, LIPIcs 

Volume  119 
ISSN (Print)  18688969 
Conference
Conference  27th Annual EACSL Conference Computer Science Logic, CSL 2018 

Country/Territory  United Kingdom 
City  Birmingham 
Period  4/09/18 → 7/09/18 
Keywords
 game semantics
 Herbrand's theorem
 true concurrency
Fingerprint
Dive into the research topics of 'The true concurrency of Herbrand's theorem'. Together they form a unique fingerprint.Profiles

Glynn Winskel
Person: Academic