Continuations and Completeness in Proof-theoretic Semantics

TL;DR

This paper explores the connection between proof-theoretic semantics and continuation-passing semantics in logic and computation, analyzing completeness proofs and their semantic intuitions.

Contribution

It reveals how syntactic representations of continuations embody intensional semantic intuitions within proof-theoretic semantics.

Findings

Analyzes Sandqvist's proof of the completeness theorem.

Shows how continuations relate to proof-theoretic semantics.

Connects natural deduction, lambda calculus, and proof-search.

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.