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

DOI10.18778/0138-0680.2023.16arXiv2210.05336MaRDI QIDQ6200465FDOQ6200465

David Pym, Alexander V. Gheorghiu

Publication date: 29 February 2024

Published in: Bulletin of the Section of Logic (Search for Journal in Brave)

Abstract: 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 the latter 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.

Full work available at URL: https://arxiv.org/abs/2210.05336

zbMATH Keywords

proof-theoretic semanticslogic programmingbilateralismnegation-as-failure

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Logic and structure
• Rejection
• Classical logic without bivalence
• A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules
• Uniform proofs as a foundation for logic programming
• Contributions to the Theory of Logic Programming
• A logical analysis of modules in logic programming
• Bilateralism in proof-theoretic semantics
• Base-extension semantics for intuitionistic sentential logic
• Title not available (Why is that?)
• A Proof-Theoretic Approach to Logic Programming
• On an inferential semantics for classical logic
• Falsification, natural deduction and bi-intuitionistic logic
• Title not available (Why is that?)
• Book review of: N. Kürbis, Proof and falsity: a logical investigation
• Success and failure for hereditary Harrop formulae

This page was built for publication: Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6200465)