A classical-logic view on a paraconsistent logic

2020/08/17 by C.A. Middelburg, Middelburg, C. A.
Computer Science · #Advanced Algebra and Logic #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.2008.07292

Abstract

This paper is concerned with the paraconsistent first-order logic LPQ^⊃,F, Priest's LPQ enriched with an implication connective and a falsity constant. A sequent-style natural deduction proof system for this logic is presented and, for this proof system, both a model-theoretic justification and a logical justification by means of an embedding into first-order classical logic is given. The given embedding provides in addition a classical-logic explanation of this paraconsistent logic. As a further matter, its use in decidability issues concerning this paraconsistent logic is discussed. The major properties of LPQ^⊃,F concerning its logical consequence relation and its logical equivalence relation are also treated. The paper emphasizes how closely LPQ^⊃,F is related to classical logic.

Related

• A Proof in Coq that Core Logic is not Paraconsistent
• Natural Deduction Calculus for First-Order Logic
• Analytic proofs for logics of evidence and truth
• A machine-assisted view of paraconsistency
• Paraconsistent First-Order Logic with restricted modus ponens rule and infinite hierarchy levels of contradiction LP^#_ω. Axiomatical system HST^#_ω, as paraconsistent generalization of Hrbacek set theory HST