Support is Search

TL;DR

This paper establishes a correspondence between support in fixed bases within Sandqvist's semantics for intuitionistic logic and proof-search in second-order hereditary Harrop logic, providing a constructive computational interpretation.

Contribution

It shows that support in a fixed base corresponds to proof-search in a second-order hereditary Harrop logic program, bridging semantics and computation.

Findings

Support coincides with proof-search in logic programming.

Encoding uses continuation-passing style revealing eigenvariables.

Supports a constructive, computational interpretation of semantics.

Abstract

Sandqvist's base-extension semantics for intuitionistic propositional logic defines a support relation parametrised by atomic bases, with validity identified as support in every base. Sandqvist's completeness theorem answers the global question: which formulae are valid? This paper addresses the local question: given a fixed base, what does support in that base correspond to? We show that support in a fixed base coincides with proof-search in a second-order hereditary Harrop logic program, via an encoding of formulae as logic-programming goals. This encoding proceeds by reading the semantic clauses in continuation-passing style, revealing that the universal quantifiers over base extensions and atoms appearing in those clauses are not domain-ranging quantifiers over a completed totality, but eigenvariables governed by a standard freshness discipline. Base-extension semantics thereby admits a fully constructive and computationally transparent interpretation: support is proof-search. The result complements Sandqvist's global theorem with a local correspondence, vindicates the anti-realist foundations of the framework on its own terms, and opens the way for implementing the semantics in modelling tasks.