A CALCULUS FOR BELNAP'S LOGIC IN WHICH EACH PROOF CONSISTS OF TWO TREES

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 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 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.