Nested sequent systems for modal logics are a relatively recent development, within the general area known as deep reasoning. The idea of deep reasoning is to create systems within which one operates at lower levels in formulas than just those involving the main connective or operator. Prefixed tableaus go back to 1972, and are modal tableau systems with extra machinery to represent accessibility in a purely syntactic way. We show that modal nested sequents and prefixed modal tableaus are notational variants (...) of each other, roughly in the same way that tableaus and Gentzen sequent calculi are notational variants. This immediately gives rise to new modal nested sequent systems which may be of independent interest. We discuss some of these, including those for some justification logics that include standard modal operators. (shrink)

The purpose of this work is to present Gentzen-style formulations of S5 and S4 based on sequents of higher levels. Sequents of level 1 are like ordinary sequents, sequents of level 1 have collections of sequents of level 1 on the left and right of the turnstile, etc. Rules for modal constants involve sequents of level 2, whereas rules for customary logical constants of first-order logic with identity involve only sequents of level 1. A restriction on Thinning on the right (...) of level 2, which when applied to Thinning on the right of level 1 produces intuitionistic out of classical logic (without changing anything else), produces S4 out of S5 (without changing anything else). This characterization of modal constants with sequents of level 2 is unique in the following sense. If constants which differ only graphically are given a formally identical characterization, they can be shown inter-replaceable (not only uniformly) with the original constants salva provability. Customary characterizations of modal constants with sequents of level 1, as well as characterizations in Hilbert-style axiomatizations, are not unique in this sense. This parallels the case with implication, which is not uniquely characterized in Hilbert-style axiomatizations, but can be uniquely characterized with sequents of level 1. These results bear upon theories of philosophical logic which attempt to characterize logical constants syntactically. They also provide an illustration of how alternative logics differ only in their structural rules, whereas their rules for logical constants are identical. (shrink)

The logic CD is an intermediate logic which exactly corresponds to the Kripke models with constant domains. It is known that the logic CD has a Gentzen-type formulation called LD and rules are replaced by the corresponding intuitionistic rules) and that the cut-elimination theorem does not hold for LD. In this paper we present a modification of LD and prove the cut-elimination theorem for it. Moreover we prove a “weak” version of cut-elimination theorem for LD, saying that all “cuts” except (...) some special forms can be eliminated from a proof in LD. From these cut-elimination theorems we obtain some corollaries on syntactical properties of CD: fragments collapsing into intuitionistic logic. Harrop disjunction and existence properties, and a fact on the number of logical symbols in the axiom of CD. (shrink)

We introduce a sequent calculus B for a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic, quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterize B positively: reflection, symmetry and visibility. A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with (...) a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection. To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube. (shrink)

Cut-free sequent calculi for the predicate intermediate logic CD of constant domains have appeared only very recently in literature, even if this logic has been axiomiatized since the early seventies. In the present paper we propose a different cut-free sequent calculus for CD, in which a great care is devoted in avoiding duplications of formulas.