Intuitionistic proofs without syntax

Willem Heijltjes, Dominic Hughes, Lutz Strassburger

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

1 Citation (Scopus)
5 Downloads (Pure)

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.
Original languageEnglish
Title of host publication2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019
PublisherIEEE
Number of pages13
Volume2019
ISBN (Electronic)9781728136080
DOIs
Publication statusPublished - 6 Aug 2019
EventThirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science - Vancouver, Canada
Duration: 24 Jun 201927 Jun 2019

Publication series

NameProceedings - Symposium on Logic in Computer Science
Volume2019-June
ISSN (Print)1043-6871

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

ASJC Scopus subject areas

  • Software
  • Mathematics(all)

Cite this

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

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

2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. Vol. 2019 IEEE, 2019. (Proceedings - Symposium on Logic in Computer Science; Vol. 2019-June).

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

Heijltjes, W, Hughes, D & Strassburger, L 2019, Intuitionistic proofs without syntax. in 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. vol. 2019, Proceedings - Symposium on Logic in Computer Science, vol. 2019-June, 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 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. Vol. 2019. IEEE. 2019. (Proceedings - Symposium on Logic in Computer Science). https://doi.org/10.1109/LICS.2019.8785827
Heijltjes, Willem ; Hughes, Dominic ; Strassburger, Lutz. / Intuitionistic proofs without syntax. 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. Vol. 2019 IEEE, 2019. (Proceedings - Symposium on Logic in Computer Science).
@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",
series = "Proceedings - Symposium on Logic in Computer Science",
publisher = "IEEE",
booktitle = "2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019",
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

UR - http://www.scopus.com/inward/record.url?scp=85068594634&partnerID=8YFLogxK

U2 - 10.1109/LICS.2019.8785827

DO - 10.1109/LICS.2019.8785827

M3 - Conference contribution

VL - 2019

T3 - Proceedings - Symposium on Logic in Computer Science

BT - 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019

PB - IEEE

ER -