Abstract
This paper is concerned with the first-order paraconsistent logic
LPQ$^{\supset,F}$.
A sequent-style natural deduction proof system for this logic is given
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 presented.
For no logic that is essentially the same as LPQ$^{\supset,F}$, a natural
deduction proof system is currently available in the literature.
The presented embedding provides both a classical-logic explanation of
this logic and a logical justification of its proof system.