Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic

Bulletin of the Section of Logic 52 (2):239-266 (2023)
  Copy   BIBTEX


Proof-theoretic semantics (P-tS) is the paradigm of semantics in which meaning in logic is based on proof (as opposed to truth). A particular instance of P-tS for intuitionistic propositional logic (IPL) is its base-extension semantics (B-eS). This semantics is given by a relation called support, explaining the meaning of the logical constants, which is parameterized by systems of rules called bases that provide the semantics of atomic propositions. In this paper, we interpret bases as collections of definite formulae and use the operational view of them as provided by uniform proof-search—the proof-theoretic foundation of logic programming (LP)—to establish the completeness of IPL for the B-eS. This perspective allows negation, a subtle issue in P-tS, to be understood in terms of the negation-as-failure protocol in LP. Specifically, while the denial of a proposition is traditionally understood as the assertion of its negation, in B-eS we may understand the denial of a proposition as the failure to find a proof of it. In this way, assertion and denial are both prime concepts in P-tS.



    Upload a copy of this work     Papers currently archived: 92,347

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Proof-Theoretic Semantics and Inquisitive Logic.Will Stafford - 2021 - Journal of Philosophical Logic 50 (5):1199-1229.
Inquisitive Intuitionistic Logic.Wesley H. Holliday - 2020 - In Nicola Olivetti & Rineke Verbrugge (eds.), Advances in Modal Logic, Vol. 11. College Publications. pp. 329-348.
N-prolog and equivalence of logic programs.Nicola Olivetti & Lea Terracini - 1992 - Journal of Logic, Language and Information 1 (4):253-340.
Safe beliefs for propositional theories.Mauricio Osorio, Juan Pérez & José Arrazola - 2005 - Annals of Pure and Applied Logic 134 (1):63-82.
Disjunctive logic programs, answer sets, and the cut rule.Éric Martin - 2022 - Archive for Mathematical Logic 61 (7):903-937.
Negative Predication and Distinctness.Bartosz Więckowski - 2023 - Logica Universalis 17 (1):103-138.


Added to PP

16 (#911,799)

6 months
14 (#185,390)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

David Pym
University College London

References found in this work

Articulating Reasons: An Introduction to Inferentialism.Robert Brandom - 2000 - Cambridge, Mass.: Harvard University Press.
The collected papers of Gerhard Gentzen.Gerhard Gentzen - 1969 - Amsterdam,: North-Holland Pub. Co.. Edited by M. E. Szabo.
Yes and no.I. Rumfitt - 2000 - Mind 109 (436):781-823.
Rejection.Timothy Smiley - 1996 - Analysis 56 (1):1–9.
The Collected Papers of Gerhard Gentzen.K. Schütte - 1972 - Journal of Symbolic Logic 37 (4):752-753.

View all 14 references / Add more references