License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2018.5
URN: urn:nbn:de:0030-drops-96723
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9672/
Go to the corresponding LIPIcs Volume Portal

Alcolei, Aurore ; Clairambault, Pierre ; Hyland, Martin ; Winskel, Glynn

The True Concurrency of Herbrand's Theorem

pdf-format:
LIPIcs-CSL-2018-5.pdf (0.6 MB)

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 first-order purely existential formula to that of a finite disjunction. In the general case, 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 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 first-order 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 well-chosen denotational model.

BibTeX - Entry

@InProceedings{alcolei_et_al:LIPIcs:2018:9672,
  author =	{Aurore Alcolei and Pierre Clairambault and Martin Hyland and Glynn Winskel},
  title =	{{The True Concurrency of Herbrand's Theorem}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic  (CSL 2018)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Dan Ghica and Achim Jung},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9672},
  URN =		{urn:nbn:de:0030-drops-96723},
  doi =		{10.4230/LIPIcs.CSL.2018.5},
  annote =	{Keywords: Herbrand's theorem, Game semantics, True concurrency}
}

Keywords: Herbrand's theorem, Game semantics, True concurrency
Collection: 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
Issue Date: 2018
Date of publication: 29.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI