Intuitionistic proofs without syntax

Willem Heijltjes, Dominic Hughes, Lutz Strassburger

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

7 Citations (SciVal)
94 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
Pages1-13
Number of pages13
ISBN (Electronic)9781728136080
ISBN (Print)9781728136097
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

NameAnnual 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
Country/TerritoryCanada
CityVancouver
Period24/06/1927/06/19

Keywords

  • intuitionistic logic
  • proof nets
  • game semantics

ASJC Scopus subject areas

  • Software
  • General Mathematics

Fingerprint

Dive into the research topics of 'Intuitionistic proofs without syntax'. Together they form a unique fingerprint.

Cite this