arXiv:2603.13018 · v2

Support is Search

首次提交 2026-03-13 22:24

版本更新 2026-11-12 17:26

雷达观测 2026-11-13 14:15

摘要

For intuitionistic propositional logic, Sandqvist's base-extension semantics 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 hereditary Harrop logic program with a quantifier over atoms, via an encoding of formulae as logic programming goals. The encoding is a variant of the Russell-Prawitz translation of the connectives, with quantification restricted to atoms, and it is obtained by reading the semantic clauses in continuation-passing style. So read, the universal quantifiers over base extensions and atoms in those clauses need not range over a completed totality: they are eigenvariables under a standard freshness discipline. Base-extension semantics thereby acquires an explicit computational content: support is proof-search. The result complements Sandqvist's global theorem with a local correspondence and makes the constructive character of the framework explicit.

作者备注：24 pages

期刊信息：Journal of Logic and Computation 2026