pith. machine review for the scientific record. sign in

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

Recognition: unknown

Continuations and Completeness in Proof-theoretic Semantics

David Pym, Edmund Robinson, Eike Ritter, Tao Gu

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 · 10 canonical work pages

  1. [1]

    Topology Via Logic

    Vickers, Steven. Topology Via Logic

  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=

    2023

  4. [4]

    Miller, Dale , year = 1989, journal =

    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

  6. [6]

    Prawitz, Dag , year = 1974, journal =

    1974

  7. [7]

    Prawitz, Dag , year = 1972, booktitle =

    1972

  8. [8]

    Prawitz, Dag , year = 1973, booktitle =

    1973

  9. [9]

    Prawitz, Dag , year =

  10. [10]

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

    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 =

    2014

  13. [13]

    , booktitle = "

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

  14. [14]

    Johnstone, Peter T. , year=. Stone Spaces

  15. [15]

    Theoretical Computer Science

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

    1975

  16. [16]

    LISP and Symbolic Computation

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

    1993

  17. [17]

    Investigations into Logical Deduction

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

    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=

    2015

  19. [19]

    2018 , edition =

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

    2018

  20. [20]

    Mind and language

    Dummett, Michael , title=". Mind and language

  21. [21]

    Advances in Proof-Theoretic Semantics , year =

  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 =

  24. [24]

    Towards a Foundation of General Proof Theory

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

    1973

  25. [25]

    Synthese. 1974 , url=

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

    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="

  29. [29]

    Mathematische Zeitschrift

    Gentzen, Gerhard , title=". Mathematische Zeitschrift

  30. [30]

    2005 , note=

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

    2005

  31. [31]

    2016 , publisher=

    Piecha, Thomas , booktitle=. 2016 , publisher=

    2016

  32. [32]

    2019 , publisher=

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

    2019

  33. [33]

    2025 , eprint=

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

    2025

  34. [34]

    Yes” and “No

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

  35. [35]

    Zwischen traditioneller und moderner Logik: Nichtklassische Ans\

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

  36. [36]

    and Pym, D.J

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

  37. [37]

    The Logic of Bunched Implications

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

  38. [38]

    , title="

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

  39. [39]

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

  40. [40]

    Dummett, Michael , title="

  41. [41]

    2006 , publisher=

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

    2006

  42. [42]

    2008 , editor =

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

    2008

  43. [43]

    van Benthem, Johan , title="

  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=

    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

    2016

  46. [46]

    and Pym, David J

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

    2025

  47. [47]

    Pym , title =

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

    2019

  48. [48]

    Hlobil, Ulf and Brandom, Robert , title =

  49. [49]

    Brandom, Robert , title = "

  50. [50]

    Brandom, Robert , title=". 1994

    1994

  51. [51]

    Floridi, Luciano , title="

  52. [52]

    Philosophy and phenomenological research , volume=

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

    2005

  53. [53]

    Information Flow and Relevant Logics , year =

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

  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 =

  55. [55]

    Logic Journal of IGPL , volume=

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

    1995

  56. [56]

    Studia Logica , note=

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

  57. [57]

    Sandqvist, Tor , title=

  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=

  60. [60]

    Prawitz, Dag , year = 1971, booktitle =

    1971

  61. [61]

    Studia Logica

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

  62. [62]

    Gheorghiu and David J

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

    2023

  63. [63]

    Studia Logica

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

    2025

  64. [64]

    Gheorghiu and Tao Gu and David J

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

    2024

  65. [65]

    The Journal of Philosophy , volume=

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

    1981

  66. [66]

    1986 , booktitle =

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

    1986

  67. [67]

    Situations and

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

  68. [68]

    Situations and

    Jon Barwise and John Perry , year=. Situations and

  69. [69]

    Situation Theory and Its Applications; Volume 1 , publisher=

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

  70. [70]

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

    1997

  71. [71]

    , title="

    Dretske, Fred L. , title="

  72. [72]

    Wittgenstein and the Philosophy of Information

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

    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=

    1993

  74. [74]

    Information as Correlation versus Information as Range

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

    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

    1999

  76. [76]

    The Stories of Logic and Information

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

  77. [77]

    Logic and information

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

    1991

  78. [78]

    Logic Journal of the IGPL

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

    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=

Showing first 80 references.