Abstract
This paper concerns an expansion of first-order Belnap-Dunn logic whose
connectives and quantifiers all have a counterpart in classical logic.
The language and logical consequence relation of this paradefinite logic
are defined, a sequent calculus proof system for this logic is
presented, and the soundness and completeness of this proof system is
established.
It is shown that the defined logic distinguishes itself from the many
other paradefinite logics that are usually considered equally classical
by the classical laws of logical equivalence that hold for it.
It is further argued that the defined logic is the most natural
paradefinite logic relative to the version of classical logic with the
same language.
Moreover, a simple embedding of the defined logic in that version of
classical logic is presented and the potential of the logic for dealing
with inconsistencies and incompletenesses in inductive machine learning
is discussed.