The global consequence relation of a normal modal logic \ is formulated as a global sequent calculus which extends the local sequent theory of \ with global sequent rules. All global sequent calculi of normal modal logics admits global cut elimination. This property is utilized to show that decidability is preserved from the local to global sequent theories of any normal modal logic over \. The preservation of Craig interpolation property from local to global sequent theories of any normal modal (...) logic is shown by proof-theoretic method. (shrink)

We prove that certain natural sequent systems for bi-intuitionistic logic have the analytic cut property. In the process we show that the (global) subformula property implies the (local) analytic cut property, thereby demonstrating their equivalence. Applying a version of Maehara technique modified in several ways, we prove that bi-intuitionistic logic enjoys the classical Craig interpolation property and Maximova variable separation property; its Halldén completeness follows.

Non-classical negations may fail to be contradictory-forming operators in more than one way, and they often fail also to respect fundamental meta-logical properties such as the replacement property. Such drawbacks are witnessed by intricate semantics and proof systems, whose philosophical interpretations and computational properties are found wanting. In this paper we investigate congruential non-classical negations that live inside very natural systems of normal modal logics over complete distributive lattices; these logics are further enriched by adjustment connectives that may be used (...) for handling reasoning under uncertainty caused by inconsistency or undeterminedness. Using such straightforward semantics, we study the classes of frames characterized by seriality, reflexivity, functionality, symmetry, transitivity, and some combinations thereof, and discuss what they reveal about sub-classical properties of negation. To the logics thereby characterized we apply a general mechanism that allows one to endow them with analytic ordinary sequent systems, most of which are even cut-free. We also investigate the exact circumstances that allow for classical negation to be explicitly defined inside our logics. (shrink)