A calculus for Belnap's logic in which each proof consists of two trees

Logique Et Analyse 220:643-656 (2012)
  Copy   BIBTEX


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.

Author Profiles

Reinhard Muskens
University of Amsterdam
Stefan Wintein
Erasmus University Rotterdam


Added to PP

120 (#71,737)

6 months
32 (#79,330)

Historical graph of downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.
How can I increase my downloads?