This paper is dedicated to extending and adapting to modal logic the approach of fractional semantics to classical logic. This is a multi-valued semantics governed by pure proof-theoretic considerations, whose truth-values are the rational numbers in the closed interval $[0,1]$. Focusing on the modal logic K, the proposed methodology relies on three key components: bilateral sequent calculus, invertibility of the logical rules, and stability (proof-invariance). We show that our semantic analysis of K affords an informational refinement with respect to the (...) standard Kripkean semantics (a new proof of Dugundji’s theorem is a case in point) and it raises the prospect of a proof-theoretic semantics for modal logic. (shrink)

C. I. Lewis’ systems were the first axiomatisations of modal logics. However some of those systems are non-normal modal logics, since they do not admit a full rule of necessitation, but only a restricted version thereof. We provide G3-style labelled sequent calculi for Lewis’ non-normal propositional systems. The calculi enjoy good structural properties, namely admissibility of structural rules and admissibility of cut. Furthermore they allow for straightforward proofs of admissibility of the restricted versions of the necessitation rule. We establish completeness (...) of the calculi and we discuss also related systems. (shrink)

The article deals with infinitary modal logic. We first discuss the difficulties related to the development of a satisfactory proof theory and then we show how to overcome these problems by introducing a labelled sequent calculus which is sound and complete with respect to Kripke semantics. We establish the structural properties of the system, namely admissibility of the structural rules and of the cut rule. Finally, we show how to embed common knowledge in the infinitary calculus and we discuss first-order (...) extensions of infinitary modal logic. (shrink)

In the present paper we deal with subintuitionistic logics and their modal companions. In particular, we introduce nested calculi for subintuitionistic systems and for modal logics in the S5 modal cube ranging from K to S4. The latter calculi differ from standard nested systems, as there are multiple rules handling the modal operator. As an upshot, we get a purely syntactic proof of the Gödel-McKinsey-Tarski embedding which preserves the structure and the height of the derivations. Finally, we obtain a conservativity (...) result for classical logic over a weak subintuitionistic system. (shrink)

The paper investigates from a proof-theoretic perspective various non-contractive logical systems, which circumvent logical and semantic paradoxes. Until recently, such systems only displayed additive quantifiers (Grišin and Cantini). Systems with multiplicative quantifiers were proposed in the 2010s (Zardini), but they turned out to be inconsistent with the naive rules for truth or comprehension. We start by presenting a first-order system for disquotational truth with additive quantifiers and compare it with Grišin set theory. We then analyze the reasons behind the inconsistency (...) phenomenon affecting multiplicative quantifiers. After interpreting the exponentials in affine logic as vacuous quantifiers, we show how such a logic can be simulated within a truth-free fragment of a system with multiplicative quantifiers. Finally, we establish that the logic for these multiplicative quantifiers (but without disquotational truth) is consistent, by proving that an infinitary version of the cut rule can be eliminated. This paves the way to a syntactic approach to the proof theory of infinitary logic with infinite sequents. (shrink)

Fractional semantics provides a multi-valued interpretation of a variety of logics, governed by purely proof-theoretic principles. This approach employs a method of systematic decomposition of formulas through a well-disciplined sequent calculus, assigning a fractional value that measures the “quantity of identity” (intuitively, “quantity of truth”) within a sequent. A key consequence of this framework is the breakdown of the traditional symmetry between truth and contradiction. In this paper, we explore the ramifications of this novel perspective on classical logic. Specifically, we (...) (i) introduce an alternative _paraconsistent_ consequence relation, and (ii) show how the gradual character of contradictions induces a corresponding characterization of tautologies, thereby obtaining a full-fledged informational refinement of classical logic. (shrink)

Decidability of monadic first-order classical logic was established by Löwenheim in 1915. The proof made use of a semantic argument and a purely syntactic proof has never been provided. In the present paper we introduce a syntactic proof of decidability of monadic first-order logic in innex normal form which exploits G3-style sequent calculi. In particular, we introduce a cut- and contraction-free calculus having a (complexity-optimal) terminating proof-search procedure. We also show that this logic can be faithfully embedded in the modal (...) logic T. (shrink)

We present a uniform proof-theoretic proof of the Gödel–McKinsey–Tarski embedding for a class of first-order intuitionistic theories. This is achieved by adapting to the case of modal logic the methods of proof analysis in order to convert axioms into rules of inference of a suitable sequent calculus. The soundness and the faithfulness of the embedding are proved by induction on the height of the derivations in the augmented calculi. Finally, we define an extension of the modal system for which the (...) result holds with respect to geometric intuitionistic. (shrink)

In a recent paper, under the auspices of an unorthodox variety of bilateralism, we introduced a new kind of proof-theoretic semantics for the base modal logic $\mathbf{K}$, whose values lie in the closed interval $[0,1]$ of rational numbers [14]. In this paper, after clarifying our conception of bilateralism – dubbed “soft bilateralism” – we generalize the fractional method to encompass extensions and weakenings of $\mathbf{K}$. Specifically, we introduce well-behaved hypersequent calculi for the deontic logic $\mathbf{D}$ and the non-normal modal logics (...) $\mathbf{E}$ and $\mathbf{M}$ and thoroughly investigate their structural properties. (shrink)