A classical-logic view on a paraconsistent logic

This paper is concerned with the paraconsistent first-order logic LPQ$^{\supset,\mathsf{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$^{\supset,\mathsf{F}}$ concerning its logical consequence relation and its logical equivalence relation are also treated. The paper emphasizes how closely LPQ$^{\supset,\mathsf{F}}$ is related to classical logic.