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

DOI10.18778/0138-0680.2023.16MaRDI QIDQ6200465zbMATH OpenFDO

Authors Alexander V. Gheorghiu, David Pym

Publication date 29 February 2024

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

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

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)

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.

Cites work

• scientific article; zbMATH DE number 3872640 (Why is no real title available?)
• scientific article; zbMATH DE number 3664336 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 2095713 (Why is no real title available?)
• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• A Proof-Theoretic Approach to Logic Programming
• A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules
• A logical analysis of modules in logic programming
• Base-extension semantics for intuitionistic sentential logic
• Bilateralism in proof-theoretic semantics
• Book review of: N. Kürbis, Proof and falsity: a logical investigation
• Classical logic without bivalence
• Contributions to the Theory of Logic Programming
• Falsification, natural deduction and bi-intuitionistic logic
• Logic and structure
• On an inferential semantics for classical logic
• Rejection
• Success and failure for hereditary Harrop formulae
• The definitional view of atomic systems in proof-theoretic semantics
• Uniform proofs as a foundation for logic programming

Cited in

(5)

• A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic
• From proof-theoretic validity to base-extension semantics for intuitionistic propositional logic
• Base-extension semantics for modal logic
• On an inferential semantics for intuitionistic sentential logic
• Proof-theoretic semantics for first-order logic

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)