Intuitionistic proofs without syntax

Willem Heijltjes, Dominic Hughes, Lutz Strassburger

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

1 Citation (Scopus)
12 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)

Projects

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