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

Logique Et Analyse 220:643-656 (2012)
Download Edit this record How to cite View on PhilPapers
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.
PhilPapers/Archive ID
Upload history
Archival date: 2018-08-27
View other versions
Added to PP index

Total views
58 ( #54,239 of 2,454,496 )

Recent downloads (6 months)
4 ( #60,382 of 2,454,496 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.