pith. sign in

arxiv: 2605.04689 · v1 · submitted 2026-05-06 · 🧮 math.LO · cs.LO

Continuations and Completeness in Proof-theoretic Semantics

Tao Gu , David Pym , Eike Ritter , Edmund Robinson This is my paper

Pith reviewed 2026-05-08 16:47 UTC · model grok-4.3

classification 🧮 math.LO cs.LO
keywords base-extension semanticscontinuationsproof-theoretic semanticsintuitionistic logiccompleteness theoremnatural deductionlambda calculusKripke semantics
0
0 comments X

The pith

Syntactic continuations embody intensional semantical intuitions about the meaning-use relationship in intuitionistic logic.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper aims to connect the completeness theorem for intuitionistic propositional logic in base-extension semantics with continuation-passing from computation theory. It does so by reanalyzing Sandqvist's proof from the standpoint of Kripke's and Heyting's semantics, showing that syntactic forms of continuations capture intuitions about how meaning relates to use. Readers would care because this link lets proof-theoretic tools give precise semantic content to a core computational idea. The work treats continuations both as reduction steps in natural deduction and lambda calculus and as features of proof-search.

Core claim

The central claim is that our analysis of Sandqvist's completeness proof for base-extension semantics, viewed from the mathematical perspective of Kripke's and Heyting's semantics, reveals how syntactic representations of continuations embody intensional semantical intuitions about the relationship between their meaning and use. These intuitions are made precise using the tools of proof-theoretic semantics.

What carries the argument

The analysis of Sandqvist's completeness proof for base-extension semantics, interpreted through Kripke and Heyting semantics, which connects continuation-passing reduction in natural deduction and the lambda calculus to proof-search.

Load-bearing premise

Sandqvist's completeness proof for base-extension semantics will reveal syntactic continuations as embodiments of intensional semantical intuitions when viewed through the mathematical perspective of Kripke's and Heyting's semantics.

What would settle it

A detailed walkthrough of the completeness proof that finds no structural alignment between continuation representations and the intensional meaning-use intuitions drawn from Kripke and Heyting models would falsify the claim.

read the original abstract

This is a short paper about the relationship between logic and computation. More specifically, it is about a relationship between the completeness proof for intuitionistic propositional logic within the form of proof-theoretic semantics that is known as base-extension semantics and a fundamental idea from the theory of computation called continuation-passing semantics. The latter is explained herein both in terms of reduction in natural deduction and the lambda calculus and in terms of proof-search. The relationship between completeness and continuations is explored through an analysis of Sandqvist's proof of the completeness theorem as seen from the mathematical perspective of Kripke's and Heyting's semantics. Our analysis can be seen to reveal how syntactic representations of continuations embody intensional semantical intuitions about the relationship between their meaning and use. These intuitions are made precise using the tools of proof-theoretic semantics.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper explores the relationship between logic and computation by analyzing Sandqvist's completeness proof for intuitionistic propositional logic in base-extension semantics. It interprets this proof through the lens of Kripke's and Heyting's semantics to argue that syntactic representations of continuations embody intensional semantical intuitions about the relationship between meaning and use. These intuitions are made precise using tools from proof-theoretic semantics, with connections drawn via natural deduction reduction, the lambda calculus, and proof-search.

Significance. If the interpretive analysis holds, the paper provides a conceptual bridge between proof-theoretic semantics and computational notions like continuation-passing, potentially clarifying how syntactic structures in proofs capture semantic intuitions in intuitionistic logic. This could contribute to interdisciplinary discussions in logic and theoretical computer science, though its value rests on the depth of the reanalysis rather than new formal results.

minor comments (2)
  1. The abstract and overall presentation would benefit from more explicit pointers to specific steps or lemmas in Sandqvist's original completeness proof to ground the reinterpretation.
  2. Consider clarifying the precise sense in which 'syntactic representations of continuations' are identified with intensional intuitions, perhaps with a brief illustrative example from natural deduction or proof-search.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the paper and for recommending minor revision. No specific major comments were raised in the report, so there are no individual points requiring detailed rebuttal or targeted changes at this stage.

Circularity Check

0 steps flagged

No significant circularity; interpretive analysis of prior result

full rationale

The paper offers an interpretive re-reading of Sandqvist's existing completeness theorem for base-extension semantics, connecting it to continuation-passing via natural deduction, lambda calculus, and Kripke/Heyting semantics. No new theorems, equations, fitted parameters, or derivations are introduced. The central claim is an analysis that reveals an embodiment of intuitions, not a self-contained derivation that reduces to its own inputs by construction. Dependence on Sandqvist is external prior literature, not self-citation or ansatz smuggling. No steps match any enumerated circularity pattern.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard background from proof theory and semantics rather than new postulates; full details unavailable from abstract alone.

axioms (2)
  • domain assumption Base-extension semantics provides a valid framework for intuitionistic propositional logic
    Invoked as the setting for Sandqvist's completeness proof.
  • domain assumption Kripke and Heyting semantics offer appropriate perspectives for reinterpreting the completeness proof
    Used explicitly to analyze the relationship with continuations.

pith-pipeline@v0.9.0 · 5435 in / 1380 out tokens · 62020 ms · 2026-05-08T16:47:40.315818+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

89 extracted references · 89 canonical work pages

  1. [1]

    Topology Via Logic

    Vickers, Steven. Topology Via Logic

    work page

  2. [2]

    Proceedings of the ACM Annual Conference - Volume 2 , pages =

    Reynolds, John , title = ". Proceedings of the ACM Annual Conference - Volume 2 , pages =. 1972 , isbn =. doi:10.1145/800194.805852 , abstract =

    work page doi:10.1145/800194.805852 1972

  3. [3]

    and Pym, David J

    Gheorghiu, Alexander V. and Pym, David J. , title=". Bulletin of the Section of Logic. 2023 , pages=

    work page 2023

  4. [4]

    Miller, Dale , year = 1989, journal =

    work page 1989

  5. [5]

    Sheaves in Geometry and Logic: A First Introduction to Topos Theory

    Mac Lane, Saunders and Moerdijk, Ieke. Sheaves in Geometry and Logic: A First Introduction to Topos Theory

    work page

  6. [6]

    Prawitz, Dag , year = 1974, journal =

    work page 1974

  7. [7]

    Prawitz, Dag , year = 1972, booktitle =

    work page 1972

  8. [8]

    Prawitz, Dag , year = 1973, booktitle =

    work page 1973

  9. [9]

    Prawitz, Dag , year =

    work page

  10. [10]

    Fernando Ferreira and Gilda Ferreira , year = 2013, journal =

    work page 2013

  11. [11]

    doi:10.1007/s10992-005-9001-z , issn =

    Fernando Ferreira , year = 2006, journal =. doi:10.1007/s10992-005-9001-z , issn =

    work page doi:10.1007/s10992-005-9001-z 2006

  12. [12]

    Ferreira, Fernando and Ferreira, Gilda , year = 2014, journal =

    work page 2014

  13. [13]

    , booktitle = "

    Howard, W.A. , booktitle = ". The Formulae-as-Types Notion of Construction

    work page

  14. [14]

    Johnstone, Peter T. , year=. Stone Spaces

    work page

  15. [15]

    Theoretical Computer Science

    Call-by-name, call-by-value and the -calculus , author=. Theoretical Computer Science. 1975 , publisher=

    work page 1975

  16. [16]

    LISP and Symbolic Computation

    Reynolds, John , title=". LISP and Symbolic Computation. 1993 , url=

    work page 1993

  17. [17]

    Investigations into Logical Deduction

    Gentzen, Gerhard , booktitle=". Investigations into Logical Deduction. 1969 , publisher=

    work page 1969

  18. [18]

    Some Remarks on Proof-Theoretic Semantics

    Dyckhoff, Roy , series=". Some Remarks on Proof-Theoretic Semantics. Advances in Proof-Theoretic Semantics (Thomas Piecha and Peter Schroeder-Heister, editors). 2015 , publisher=

    work page 2015

  19. [19]

    2018 , edition =

    Schroeder-Heister, Peter , title =. 2018 , edition =

    work page 2018

  20. [20]

    Mind and language

    Dummett, Michael , title=". Mind and language

    work page

  21. [21]

    Advances in Proof-Theoretic Semantics , year =

    work page

  22. [22]

    Validity Concepts in Proof-Theoretic Semantics , volume =

    Peter Schroeder. Validity Concepts in Proof-Theoretic Semantics , volume =. doi:10.1007/s11229-004-6296-1 , journal =

    work page doi:10.1007/s11229-004-6296-1

  23. [23]

    Meaning Approached Via Proofs

    Prawitz, Dag , doi =. Meaning Approached Via Proofs. Synthese , number =

    work page

  24. [24]

    Towards a Foundation of General Proof Theory

    Prawitz, Dag , booktitle =. Towards a Foundation of General Proof Theory. 1973 , pages =

    work page 1973

  25. [25]

    Synthese. 1974 , url=

    Prawitz, D. , title=". Synthese. 1974 , url="

    work page 1974

  26. [26]

    Tracking Information

    van Benthem, Johan. Tracking Information. J. Michael Dunn on Information Based Logics. 2016. doi:10.1007/978-3-319-29300-4_17

    work page doi:10.1007/978-3-319-29300-4_17 2016

  27. [27]

    Introduction: From Information at Large to Semantics of Logics

    Bimb \'o , Katalin. Introduction: From Information at Large to Semantics of Logics. J. Michael Dunn on Information Based Logics. 2016. doi:10.1007/978-3-319-29300-4_1

    work page doi:10.1007/978-3-319-29300-4_1 2016

  28. [28]

    Girard, Jean-Yves and Lafont, Yves and Taylor, Paul , title="

    work page

  29. [29]

    Mathematische Zeitschrift

    Gentzen, Gerhard , title=". Mathematische Zeitschrift

    work page

  30. [30]

    2005 , note=

    Prawitz, Dag , title=". 2005 , note="

    work page 2005

  31. [31]

    2016 , publisher=

    Piecha, Thomas , booktitle=. 2016 , publisher=

    work page 2016

  32. [32]

    2019 , publisher=

    Piecha, Thomas and Schroeder-Heister, Peter , journal=. 2019 , publisher=

    work page 2019

  33. [33]

    2025 , eprint=

    Proof-theoretic Semantics for Classical Propositional Logic with Assertion and Denial , author=. 2025 , eprint=

    work page 2025

  34. [34]

    Yes” and “No

    Rumfitt, I. “Yes” and “No”. Mind

    work page

  35. [35]

    Zwischen traditioneller und moderner Logik: Nichtklassische Ans\

    Dunn, Jon , title=". Zwischen traditioneller und moderner Logik: Nichtklassische Ans\" a tze

    work page

  36. [36]

    and Pym, D.J

    Gu, T., Gheorghiu, A.V. and Pym, D.J. , title=". Studia Logica

    work page

  37. [37]

    The Logic of Bunched Implications

    O'Hearn, Peter and Pym, David. The Logic of Bunched Implications. Bulletin of Symbolic Logic

    work page

  38. [38]

    , title="

    Gheorghiu, A.V., and Pym, D.J. , title=". Studia Logica

    work page

  39. [39]

    Formal Theories of Information: From Shannon to Semantic Information Theory and General Concepts of Information , year =

    work page

  40. [40]

    Dummett, Michael , title="

    work page

  41. [41]

    2006 , publisher=

    Schroeder-Heister, Peter , journal=. 2006 , publisher=

    work page 2006

  42. [42]

    2008 , editor =

    Schroeder-Heister, Peter , booktitle =. 2008 , editor =

    work page 2008

  43. [43]

    van Benthem, Johan , title="

    work page

  44. [44]

    Information, Veridicalitym and Inferential Knowledge

    Fresco, Nir and McGivern, Patrick and Ghose, Aditya. Information, Veridicalitym and Inferential Knowledge. American Philosophical Quarterly. 2017 , pages=

    work page 2017

  45. [45]

    Epistemology, Knowledge and the Impact of Interaction, Logic, Epistemology, and the Unity of Science

    Piecha, Thomas and Schroeder-Heister, Peter , title=". Epistemology, Knowledge and the Impact of Interaction, Logic, Epistemology, and the Unity of Science. 2016

    work page 2016

  46. [46]

    and Pym, David J

    Gheorghiu, Alexander V. and Pym, David J. , title = ". 2025

    work page 2025

  47. [47]

    Pym , title =

    David J. Pym , title =. 2019 , doi =

    work page 2019

  48. [48]

    Hlobil, Ulf and Brandom, Robert , title =

    work page

  49. [49]

    Brandom, Robert , title = "

    work page

  50. [50]

    Brandom, Robert , title=". 1994

    work page 1994

  51. [51]

    Floridi, Luciano , title="

    work page

  52. [52]

    Philosophy and phenomenological research , volume=

    Is semantic information meaningful data? , author=. Philosophy and phenomenological research , volume=. 2005 , publisher=

    work page 2005

  53. [53]

    Information Flow and Relevant Logics , year =

    Greg Restall , booktitle =. Information Flow and Relevant Logics , year =

    work page

  54. [54]

    Information Flow and the Lambek Calculus , volume =

    Barwise, Jon and Gabbay, Dov and Hartonas, Chrysafis (Takis) , year =. Information Flow and the Lambek Calculus , volume =

    work page

  55. [55]

    Logic Journal of IGPL , volume=

    On the logic of information flow , author=. Logic Journal of IGPL , volume=. 1995 , publisher=

    work page 1995

  56. [56]

    Studia Logica , note=

    David Pym and Eike Ritter and Edmund Robinson , title=. Studia Logica , note=

    work page

  57. [57]

    Sandqvist, Tor , title=

    work page

  58. [58]

    Logic Journal of the IGPL

    Gheorghiu, Alexander V , title = ". Logic Journal of the IGPL. 2025 , month =. doi:10.1093/jigpal/jzaf062 , url =

    work page doi:10.1093/jigpal/jzaf062 2025

  59. [59]

    Peter Schroeder-Heister , title=

    work page

  60. [60]

    Prawitz, Dag , year = 1971, booktitle =

    work page 1971

  61. [61]

    Studia Logica

    Alexander Gheorghiu and David Pym , title=". Studia Logica

    work page

  62. [62]

    Gheorghiu and David J

    Alexander V. Gheorghiu and David J. Pym , title =. 2023 , journal =

    work page 2023

  63. [63]

    Studia Logica

    Tao Gu and Alexander Gheorghiu and David Pym , title=". Studia Logica. 2025

    work page 2025

  64. [64]

    Gheorghiu and Tao Gu and David J

    Alexander V. Gheorghiu and Tao Gu and David J. Pym , title=". ENTICS 14727. 2024

    work page 2024

  65. [65]

    The Journal of Philosophy , volume=

    Scenes and other situations , author=. The Journal of Philosophy , volume=. 1981 , publisher=

    work page 1981

  66. [66]

    1986 , booktitle =

    The Situation in Logic --- I , editor =. 1986 , booktitle =

    work page 1986

  67. [67]

    Situations and

    Barwise, Jon and Perry, John , journal=. Situations and

    work page

  68. [68]

    Situations and

    Jon Barwise and John Perry , year=. Situations and

    work page

  69. [69]

    Situation Theory and Its Applications; Volume 1 , publisher=

    Information, infons, and inference , author=. Situation Theory and Its Applications; Volume 1 , publisher=

    work page

  70. [70]

    Barwise, Jon and Seligman, Jerry , title=". 1997

    work page 1997

  71. [71]

    , title="

    Dretske, Fred L. , title="

    work page

  72. [72]

    Wittgenstein and the Philosophy of Information

    Dretske, Fred , title=". Wittgenstein and the Philosophy of Information. 2008

    work page 2008

  73. [73]

    Imperfect information flow

    Barwise, Jon and Seligman, Jerry. Imperfect information flow. Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science. 1993 , organization=

    work page 1993

  74. [74]

    Information as Correlation versus Information as Range

    Johan van Benthem. Information as Correlation versus Information as Range. 2006

    work page 2006

  75. [75]

    van Benthem and D

    J. van Benthem and D. Israel. I nformation F low: T he L ogic of D istributed S ystems, J on B arwise and J erry S eligman. Journal of Logic, Language and Information. 1999

    work page 1999

  76. [76]

    The Stories of Logic and Information

    van Benthem, Johan and Martinez, Maricarmen , journal=. The Stories of Logic and Information

    work page

  77. [77]

    Logic and information

    Devlin, Keith , publisher=". Logic and information. 1991

    work page 1991

  78. [78]

    Logic Journal of the IGPL

    Eckhardt, Timo and Pym, David , title = ". Logic Journal of the IGPL. 2025 , month =

    work page 2025

  79. [79]

    Arxiv, math.LO, eprint=2411.15775,https://arxiv.org/abs/2411.15775

    Timo Eckhardt and David J. Pym , year=. Inferentialist Public Announcement Logic: Base-extension Semantics. 2411.15775 ,

    work page arXiv

  80. [80]

    Synthese , pages=

    Situations, possible worlds, and attitudes , author=. Synthese , pages=

    work page

Showing first 80 references.