Intuitionistic proofs without syntax

Willem Heijltjes, Dominic Hughes, Lutz Strassburger

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present Intuitionistic Combinatorial Proofs (ICPs), a concrete geometric semantics of intuitionistic logic based on the principles of the second author’s classical Com- binatorial Proofs.
An ICP naturally factorizes into a linear fragment, a graphical abstraction of an IMLL proof net (an arena net), and a parallel contraction-weakening fragment (a skew fibration). ICPs relate to game semantics, and can be seen as a strategy in a Hyland-Ong arena, generalized from a tree-like to a dag-like strategy.

Our first main result, Polynomial Full Completeness, is that ICPs as a semantics are complexity-aware: the translations to and from sequent calculus are size-preserving (up to a polynomial). By contrast, lambda-calculus and game semantics incur an exponential blowup. Our second main result, Local Canonicity, is that ICPs abstract fully and faithfully over the non-duplicating permutations of the sequent calculus, analogously to the first and second authors’ recent result for MALL.
LanguageEnglish
Title of host publicationLICS '19: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science
PublisherIEEE
Volume2019
ISBN (Electronic)9781728136080
DOIs
StatusPublished - 6 Aug 2019
EventThirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science - Vancouver, Canada
Duration: 24 Jun 201927 Jun 2019

Conference

ConferenceThirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS
CountryCanada
CityVancouver
Period24/06/1927/06/19

Keywords

  • intuitionistic logic
  • proof nets
  • game semantics

Cite this

Heijltjes, W., Hughes, D., & Strassburger, L. (2019). Intuitionistic proofs without syntax. In LICS '19: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (Vol. 2019). IEEE. https://doi.org/10.1109/LICS.2019.8785827

Intuitionistic proofs without syntax. / Heijltjes, Willem; Hughes, Dominic; Strassburger, Lutz.

LICS '19: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science. Vol. 2019 IEEE, 2019.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Heijltjes, W, Hughes, D & Strassburger, L 2019, Intuitionistic proofs without syntax. in LICS '19: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science. vol. 2019, IEEE, Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science, Vancouver, Canada, 24/06/19. https://doi.org/10.1109/LICS.2019.8785827
Heijltjes W, Hughes D, Strassburger L. Intuitionistic proofs without syntax. In LICS '19: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science. Vol. 2019. IEEE. 2019 https://doi.org/10.1109/LICS.2019.8785827
Heijltjes, Willem ; Hughes, Dominic ; Strassburger, Lutz. / Intuitionistic proofs without syntax. LICS '19: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science. Vol. 2019 IEEE, 2019.
@inproceedings{c8ba36667e5047db8a1be81ceaf71162,
title = "Intuitionistic proofs without syntax",
abstract = "We present Intuitionistic Combinatorial Proofs (ICPs), a concrete geometric semantics of intuitionistic logic based on the principles of the second author’s classical Com- binatorial Proofs.An ICP naturally factorizes into a linear fragment, a graphical abstraction of an IMLL proof net (an arena net), and a parallel contraction-weakening fragment (a skew fibration). ICPs relate to game semantics, and can be seen as a strategy in a Hyland-Ong arena, generalized from a tree-like to a dag-like strategy.Our first main result, Polynomial Full Completeness, is that ICPs as a semantics are complexity-aware: the translations to and from sequent calculus are size-preserving (up to a polynomial). By contrast, lambda-calculus and game semantics incur an exponential blowup. Our second main result, Local Canonicity, is that ICPs abstract fully and faithfully over the non-duplicating permutations of the sequent calculus, analogously to the first and second authors’ recent result for MALL.",
keywords = "intuitionistic logic, proof nets, game semantics",
author = "Willem Heijltjes and Dominic Hughes and Lutz Strassburger",
year = "2019",
month = "8",
day = "6",
doi = "10.1109/LICS.2019.8785827",
language = "English",
volume = "2019",
booktitle = "LICS '19: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science",
publisher = "IEEE",
address = "USA United States",

}

TY - GEN

T1 - Intuitionistic proofs without syntax

AU - Heijltjes, Willem

AU - Hughes, Dominic

AU - Strassburger, Lutz

PY - 2019/8/6

Y1 - 2019/8/6

N2 - We present Intuitionistic Combinatorial Proofs (ICPs), a concrete geometric semantics of intuitionistic logic based on the principles of the second author’s classical Com- binatorial Proofs.An ICP naturally factorizes into a linear fragment, a graphical abstraction of an IMLL proof net (an arena net), and a parallel contraction-weakening fragment (a skew fibration). ICPs relate to game semantics, and can be seen as a strategy in a Hyland-Ong arena, generalized from a tree-like to a dag-like strategy.Our first main result, Polynomial Full Completeness, is that ICPs as a semantics are complexity-aware: the translations to and from sequent calculus are size-preserving (up to a polynomial). By contrast, lambda-calculus and game semantics incur an exponential blowup. Our second main result, Local Canonicity, is that ICPs abstract fully and faithfully over the non-duplicating permutations of the sequent calculus, analogously to the first and second authors’ recent result for MALL.

AB - We present Intuitionistic Combinatorial Proofs (ICPs), a concrete geometric semantics of intuitionistic logic based on the principles of the second author’s classical Com- binatorial Proofs.An ICP naturally factorizes into a linear fragment, a graphical abstraction of an IMLL proof net (an arena net), and a parallel contraction-weakening fragment (a skew fibration). ICPs relate to game semantics, and can be seen as a strategy in a Hyland-Ong arena, generalized from a tree-like to a dag-like strategy.Our first main result, Polynomial Full Completeness, is that ICPs as a semantics are complexity-aware: the translations to and from sequent calculus are size-preserving (up to a polynomial). By contrast, lambda-calculus and game semantics incur an exponential blowup. Our second main result, Local Canonicity, is that ICPs abstract fully and faithfully over the non-duplicating permutations of the sequent calculus, analogously to the first and second authors’ recent result for MALL.

KW - intuitionistic logic

KW - proof nets

KW - game semantics

U2 - 10.1109/LICS.2019.8785827

DO - 10.1109/LICS.2019.8785827

M3 - Conference contribution

VL - 2019

BT - LICS '19: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science

PB - IEEE

ER -