In their paper Nothing but the Truth Andreas Pietz and Umberto Rivieccio present Exactly True Logic, an interesting variation upon the four-valued logic for first-degree entailment FDE that was given by Belnap and Dunn in the 1970s. Pietz & Rivieccio provide this logic with a Hilbert-style axiomatisation and write that finding a nice sequent calculus for the logic will presumably not be easy. But a sequent calculus can be given and in this paper we will show that a calculus for (...) the Belnap-Dunn logic we have defined earlier can in fact be reused for the purpose of characterising ETL, provided a small alteration is made—initial assignments of signs to the sentences of a sequent to be proved must be different from those used for characterising FDE. While Pietz & Rivieccio define ETL on the language of classical propositional logic we also study its consequence relation on an extension of this language that is functionally complete for the underlying four truth values. On this extension the calculus gets a multiple-tree character—two proof trees may be needed to establish one proof. (shrink)

In this paper we study 12 four-valued logics arisen from Belnap's truth and/or knowledge four-valued lattices, with or without constants, by adding one or both or none of two new non-regular operations—classical negation and natural implication. We prove that the secondary connectives of the bilattice four-valued logic with bilattice constants are exactly the regular four-valued operations. Moreover, we prove that its expansion by any non-regular connective (such as, e.g., classical negation or natural implication) is strictly functionally complete. Further, finding axiomatizations (...) of the quasi varieties generated by the 12 logics involved (that prove to be varieties), we find naturell equational axiomatizations of these logics. Finally, applying Pynko's general theory of algebraizable sequential consequence operations, we also find equivalent natural sequentiell axiomatizations of the logics under consideration that expand either of two Pynko's sequential calculi for the constant-free truth-lattice four-valued logic. (shrink)

Bilattices, due to M. Ginsberg, are a family of truth value spaces that allow elegantly for missing or conflicting information. The simplest example is Belnap’s four-valued logic, based on classical two-valued logic. Among other examples are those based on finite many-valued logics, and on probabilistic valued logic. A fixed point semantics is developed for logic programming, allowing any bilattice as the space of truth values. The mathematics is little more complex than in the classical two-valued setting, but the result provides (...) a natural semantics for distributed logic programs, including those involving confidence factors. The classical two-valued and the Kripke/Kleene three-valued semantics become special cases, since the logics involved are natural sublogics of Belnap’s logic, the logic given by the simplest bilattice. (shrink)

In this paper we consider the theory of predicate logics in which the principle of Bivalence or the principle of Non-Contradiction or both fail. Such logics are partial or paraconsistent or both. We consider sequent calculi for these logics and prove Model Existence. For L4, the most general logic under consideration, we also prove a version of the Craig-Lyndon Interpolation Theorem. The paper shows that many techniques used for classical predicate logic generalise to partial and paraconsistent logics once the right (...) set-up is chosen. Our logic L4 has a semantics that also underlies Belnap’s [4] and is related to the logic of bilattices. L4 is in focus most of the time, but it is also shown how results obtained for L4 can be transferred to several variants. (shrink)

The notion of bilattice was introduced by Ginsberg, and further examined by Fitting, as a general framework for many applications. In the present paper we develop proof systems, which correspond to bilattices in an essential way. For this goal we introduce the notion of logical bilattices. We also show how they can be used for efficient inferences from possibly inconsistent data. For this we incorporate certain ideas of Kifer and Lozinskii, which happen to suit well the context of our work. (...) The outcome are paraconsistent logics with a lot of desirable properties.1. (shrink)

A curious feature of Belnap’s “useful four-valued logic”, also known as first-degree entailment (FDE), is that the overdetermined value B (both true and false) is treated as a designated value. Although there are good theoretical reasons for this, it seems prima facie more plausible to have only one of the four values designated, namely T (exactly true). This paper follows this route and investigates the resulting logic, which we call Exactly True Logic.

One of the problems we face in many-valued logic is the difficulty of capturing the intuitive meaning of the connectives introduced through truth tables. At the same time, however, some logics have nice ways to capture the intended meaning of connectives easily, such as four-valued logic studied by Belnap and Dunn. Inspired by Dunn’s discovery, we first describe a mechanical procedure, in expansions of Belnap-Dunn logic, to obtain truth conditions in terms of the behavior of the Truth and the False, (...) which gives us intuitive readings of connectives, out of truth tables. Then, we revisit the notion of functional completeness, which is one of the key notions in many-valued logic, in view of Dunn’s idea. More concretely, we introduce a generalized notion of functional completeness which naturally arises in the spirit of Dunn’s idea, and prove some fundamental results corresponding to the classical results proved by Post and Słupecki. (shrink)