We develop a general theory of FDE-based modal logics. Our framework takes into account the four-valued nature of FDE by considering four partially defined modal operators corresponding to conditions for verifying and falsifying modal necessity and possibility operators. The theory comes with a uniform characterization for all obtained systems in terms of FDE-style formula-formula sequents. We also develop some correspondence theory and show how Hilbert-style axiom systems can be obtained in appropriate cases. Finally, we outline how different systems from the (...) literature can be expressed in our framework. (shrink)

This paper is dedicated to developing a formalism that takes rejection seriously. Bilateral notation of signed formulas with force indicators is adopted to define signed consequences which can be viewed as the bilateral counterpart of Tarskian consequence relations. Its relation to some other bilateral approaches is discussed. It is shown how David Nelson’s logic N4 can be characterized bilaterally and the corresponding completeness result is proved. Further, bilateral variants of three familiar notions are considered and investigated: that of a fragment, (...) of definitional equivalence, and of a conservative extension. (shrink)

The work is concerned with the so called display property of display logic. The motivation behind it is discussed and challenged. It is shown using one display calculus for intuitionistic logic as an example that the display property can be abandoned without losing subformula, cut elimination and completeness properties in such a way that results in additional expressive power of the system. This is done by disentangling structural connectives so that they are no longer context-sensitive. A recipe for characterizing structural (...) extensions of display calculi is provided. (shrink)

We present novel proof systems for various FDE-based modal logics. Among the systems considered are a number of Belnapian modal logics introduced in Odintsov & Wansing and Odintsov & Wansing, as well as the modal logic KN4 with strong implication introduced in Goble. In particular, we provide a Hilbert-style axiom system for the logic $BK^{\square - } $ and characterize the logic BK as an axiomatic extension of the system $BK^{FS} $. For KN4 we provide both an FDE-style axiom system (...) and a decidable sequent calculus for which a contraction elimination and a cut elimination result are shown. (shrink)