Abstract
In this paper we introduce a Gentzen calculus for (a
functionally complete variant of) Belnap's logic in which
establishing the provability of a sequent in general requires
\emph{two} proof trees, one establishing that whenever all premises
are true some conclusion is true and one that guarantees the falsity
of at least one premise if all conclusions are false. The calculus
can also be put to use in proving that one statement
\emph{necessarily approximates} another, where necessary
approximation is a natural dual of entailment. The calculus, and its
tableau variant, not only capture the classical connectives, but
also the `information' connectives of four-valued Belnap logics.
This answers a question by Avron.