Support is Search
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866912964873814016 |
|---|---|
| author | Gheorghiu, Alexander V. |
| author_facet | Gheorghiu, Alexander V. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_13018 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Support is Search Gheorghiu, Alexander V. Logic in Computer Science Logic 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. |
| title | Support is Search |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2603.13018 |