A 4-valued framework is proposed to distinguish intuitionistically valid formulas within classical validities.

In this introduction to the special issue “40 years of FDE”, we offer an overview of the field and put the papers included in the special issue into perspective. More specifically, we first present various semantics and proof systems for FDE, and then survey some expansions of FDE by adding various operators starting with constants. We then turn to unary and binary connectives, which are classified in a systematic manner. First-order FDE is also briefly revisited, and we conclude by listing (...) some open problems for future research. (shrink)

Łukasiewicz presented two different analyses of modal notions by means of many-valued logics: the linearly ordered systems Ł3,..., Open image in new window,..., \; the 4-valued logic Ł he defined in the last years of his career. Unfortunately, all these systems contain “Łukasiewicz type paradoxes”. On the other hand, Brady’s 4-valued logic BN4 is the basic 4-valued bilattice logic. The aim of this paper is to show that BN4 can be strengthened with modal operators following Łukasiewicz’s strategy for defining truth-functional (...) modal logics. The systems we define lack “Łukasiewicz type paradoxes”. Following Brady, we endow them with Belnap–Dunn type bivalent semantics. (shrink)

A classical paraconsistent logic, which is regarded as a modified extension of first-degree entailment logic, is introduced as a Gentzen-type sequent calculus. This logic can simulate the classical negation in classical logic by paraconsistent double negation in CP. Theorems for syntactically and semantically embedding CP into a Gentzen-type sequent calculus LK for classical logic and vice versa are proved. The cut-elimination and completeness theorems for CP are also shown using these embedding theorems. Similar results are also obtained for an intuitionistic (...) paraconsistent logic, and several versions of Glivenko and Gödel-Gentzen translation theorems are proved for CP and IP. (shrink)

In this study, we introduce Gentzen-type sequent calculi BDm and BDi for a modal extension and an intuitionistic modification, respectively, of De and Omori’s extended Belnap–Dunn logic BD+ with classical negation. We prove theorems for syntactically and semantically embedding BDm and BDi into Gentzen-type sequent calculi S4 and LJ for normal modal logic and intuitionistic logic, respectively. The cut-elimination, decidability, and completeness theorems for BDm and BDi are obtained using these embedding theorems. Moreover, we prove the Glivenko theorem for embedding (...) BD+ into BDi and the McKinsey–Tarski theorem for embedding BDi into BDm. (shrink)

We investigate the notion of classical negation from a non-classical perspective. In particular, one aim is to determine what classical negation amounts to in a paracomplete and paraconsistent four-valued setting. We first give a general semantic characterization of classical negation and then consider an axiomatic expansion BD+ of four-valued Belnap–Dunn logic by classical negation. We show the expansion complete and maximal. Finally, we compare BD+ to some related systems found in the literature, specifically a four-valued modal logic of Béziau and (...) the logic of classical implication and a paraconsistent de Morgan negation of Zaitsev. (shrink)

We analyze the variety of A. Monteiro’s tetravalent modal algebras under the perspective of two logic systems naturally associated to it. Taking profit of the contrapositive implication introduced by A. Figallo and P. Landini, sound and complete Hilbert-style calculi for these logics are presented.

There are several three-valued logical systems that form a scattered landscape, even if all reasonable connectives in three-valued logics can be derived from a few of them. Most papers on this subject neglect the issue of the relevance of such logics in relation with the intended meaning of the third truth-value. Here, we focus on the case where the third truth-value means unknown, as suggested by Kleene. Under such an understanding, we show that any truth-qualified formula in a large range (...) of three-valued logics can be translated into KD as a modal formula of depth 1, with modalities in front of literals only, while preserving all tautologies and inference rules of the original three-valued logic. This simple information logic is a two-tiered classical propositional logic with simple semantics in terms of epistemic states understood as subsets of classical interpretations. We study in particular the translations of Kleene, Gödel, ᴌukasiewicz and Nelson logics. We show that Priest’s logic of paradox, closely connected to Kleene’s, can also be translated into our modal setting, simply by exchanging the modalities possible and necessary. Our work enables the precise expressive power of three-valued logics to be laid bare for the purpose of uncertainty management. (shrink)

The logic BN4 was defined by R.T. Brady as a four-valued extension of Routley and Meyer’s basic logic B. The system EF4 is defined as a companion to BN4 to represent the four-valued system of implication. The system Ł was defined by J. Łukasiewicz and it is a four-valued modal logic that validates what is known as strong Łukasiewicz-type modal paradoxes. The systems EF4-M and EF4-Ł are defined as alternatives to Ł without modal paradoxes. This paper aims to define a (...) Belnap-Dunn semantics for EF4, EF4-M and EF4-Ł. It is shown that EF4, EF4-M and EF4-Ł are strongly sound and complete w.r.t. their respective semantics and that EF4-M and EF4-Ł are free from strong Łukasiewicz-type modal paradoxes. (shrink)