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
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.
Categories
PhilPapers/Archive ID
WINACF
Revision history
Archival date: 2018-08-27
View upload history
References found in this work BETA
Reasoning with Logical Bilattices.Arieli, Ofer & Avron, Arnon
Meaning and Partiality.Muskens, Reinhard

View all 7 references / Add more references

Citations of this work BETA
A Gentzen Calculus for Nothing but the Truth.Wintein, Stefan & Muskens, Reinhard
Analytic Tableaux for All of SIXTEEN 3.Wintein, Stefan & Muskens, Reinhard
From Bi-Facial Truth to Bi-Facial Proofs.Wintein, Stefan & Muskens, Reinhard A.

Add more citations

Added to PP index
2013-12-13

Total views
24 ( #41,618 of 43,933 )

Recent downloads (6 months)
11 ( #39,664 of 43,933 )

How can I increase my downloads?

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