•  272
    Proof Systems for Super- Strict Implication
    with Guido Gherardi and Eric Raidl
    Studia Logica 112 (1): 249-294. 2023.
    This paper studies proof systems for the logics of super-strict implication ST2–ST5, which correspond to C.I. Lewis’ systems S2–S5 freed of paradoxes of strict implication. First, Hilbert-style axiomatic systems are introduced and shown to be sound and complete by simulating STn in Sn and backsimulating Sn in STn, respectively(for n=2,...,5). Next, G3-style labelled sequent calculi are investigated. It is shown that these calculi have the good structural properties that are distinctive of G3-sty…Read more
  •  87
    Proof-theoretic pluralism
    Synthese 198 (Suppl 20): 4879-4903. 2019.
    Starting from a proof-theoretic perspective, where meaning is determined by the inference rules governing logical operators, in this paper we primarily aim at developing a proof-theoretic alternative to the model-theoretic meaning-invariant logical pluralism discussed in Beall and Restall. We will also outline how this framework can be easily extended to include a form of meaning-variant logical pluralism. In this respect, the framework developed in this paper—which we label two-level proof-theo…Read more
  •  56
    Proof theory for quantified monotone modal logics
    with Sara Negri
    Logic Journal of the IGPL 27 (4): 478-506. 2019.
    This paper provides a proof-theoretic study of quantified non-normal modal logics. It introduces labelled sequent calculi based on neighbourhood semantics for the first-order extension, with both varying and constant domains, of monotone NNML, and studies the role of the Barcan formulas in these calculi. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction and syntactic cut eliminati…Read more
  •  45
    Free Quantified Epistemic Logics
    Studia Logica 101 (6): 1159-1183. 2013.
    The paper presents an epistemic logic with quantification over agents of knowledge and with a syntactical distinction between de re and de dicto occurrences of terms. Knowledge de dicto is characterized as ‘knowledge that’, and knowlegde de re as ‘knowledge of’. Transition semantics turns out to be an adequate tool to account for the distinctions introduced
  •  43
    G3-style sequent calculi for the logics in the cube of non-normal modal logics and for their deontic extensions are studied. For each calculus we prove that weakening and contraction are height-preserving admissible, and we give a syntactic proof of the admissibility of cut. This implies that the subformula property holds and that derivability can be decided by a terminating proof search whose complexity is in Pspace. These calculi are shown to be equivalent to the axiomatic ones and, therefore,…Read more
  •  38
    Logicality, Double-Line Rules, and Modalities
    Studia Logica 107 (1): 85-107. 2019.
    This paper deals with the question of the logicality of modal logics from a proof-theoretic perspective. It is argued that if Dos̆en’s analysis of logical constants as punctuation marks is embraced, it is possible to show that all the modalities in the cube of normal modal logics are indeed logical constants. It will be proved that the display calculus for each displayable modality admits a purely structural presentation based on double-line rules which, following Dos̆en’s analysis, allows us to…Read more
  •  37
    In previous work by Baaz and Iemhoff, a Gentzen calculus for intuitionistic logic with existence predicate is presented that satisfies partial cut elimination and Craig's interpolation property; it is also conjectured that interpolation fails for the implication-free fragment. In this paper an equivalent calculus is introduced that satisfies full cut elimination and allows a direct proof of interpolation via Maehara's lemma. In this way, it is possible to obtain much simpler interpolants and to …Read more
  •  36
    Super-Strict Implications
    with Guido Gherardi
    Bulletin of the Section of Logic 50 (1): 1-34. 2021.
    This paper introduces the logics of super-strict implications, where a super-strict implication is a strengthening of C.I. Lewis' strict implication that avoids not only the paradoxes of material implication but also those of strict implication. The semantics of super-strict implications is obtained by strengthening the (normal) relational semantics for strict implication. We consider all logics of super-strict implications that are based on relational frames for modal logics in the modal cube. …Read more
  •  34
    Interpolation in Extensions of First-Order Logic
    with Guido Gherardi and Paolo Maffezioli
    Studia Logica 108 (3): 619-648. 2020.
    We prove a generalization of Maehara’s lemma to show that the extensions of classical and intuitionistic first-order logic with a special type of geometric axioms, called singular geometric axioms, have Craig’s interpolation property. As a corollary, we obtain a direct proof of interpolation for (classical and intuitionistic) first-order logic with identity, as well as interpolation for several mathematical theories, including the theory of equivalence relations, (strict) partial and linear orde…Read more
  •  30
    Glivenko sequent classes and constructive cut elimination in geometric logics
    with Giulio Fellin and Sara Negri
    Archive for Mathematical Logic 62 (5): 657-688. 2023.
    A constructivisation of the cut-elimination proof for sequent calculi for classical, intuitionistic and minimal infinitary logics with geometric rules—given in earlier work by the second author—is presented. This is achieved through a procedure where the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. The proof of admissibility of the structural rules is made ordinal-free by introducing a new well-founded relation…Read more
  •  28
    Proof Systems for Super- Strict Implication
    with Guido Gherardi and Eric Raidl
    Studia Logica 112 (1): 249-294. 2024.
    This paper studies proof systems for the logics of super-strict implication \(\textsf{ST2}\) – \(\textsf{ST5}\), which correspond to C.I. Lewis’ systems \(\textsf{S2}\) – \(\textsf{S5}\) freed of paradoxes of strict implication. First, Hilbert-style axiomatic systems are introduced and shown to be sound and complete by simulating \(\textsf{STn}\) in \(\textsf{Sn}\) and backsimulating \(\textsf{Sn}\) in \(\textsf{STn}\), respectively (for \({\textsf{n}} =2, \ldots, 5\) ). Next, \(\textsf{G3}\) -s…Read more
  •  27
    Quantified Modal Logics: One Approach to Rule (Almost) them All!
    Journal of Philosophical Logic 53 (4): 959-996. 2024.
    We present a general approach to quantified modal logics that can simulate most other approaches. The language is based on operators indexed by terms which allow to express de re modalities and to control the interaction of modalities with the first-order machinery and with non-rigid designators. The semantics is based on a primitive counterpart relation holding between n-tuples of objects inhabiting possible worlds. This allows an object to be represented by one, many, or no object in an access…Read more
  •  22
    A Syntactic Proof of the Decidability of First-Order Monadic Logic
    with Matteo Tesi
    Bulletin of the Section of Logic 53 (2): 223-244. 2024.
    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 l…Read more
  •  18
    Double-line Harmony in a Sequent Setting
    In Arazim Pavel & Lávička Tomáš (eds.), The Logica Yearbook 2016, College Publications. 2017.
    This paper concentrates on how to capture harmony in sequent calculi. It starts by considering a proposal made by Tennant and some objections to it which have been presented by Steinberger. Then it proposes a different analysis which makes use of a double-line presentation of sequent calculi in the style of Dosen and it shows that this proposal is able to dismiss disharmonious operators without thereby adopting any global criterion.