13 found
Order:
  1. Proof Systems for Super- Strict Implication.Guido Gherardi, Eugenio Orlandelli & Eric Raidl - 2023 - Studia Logica 112 (1):249-294.
    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-style calculi, that they are sound and complete, and (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  2.  32
    Super-Strict Implications.Guido Gherardi & Eugenio Orlandelli - 2021 - Bulletin of the Section of Logic 50 (1):1-34.
    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. it is shown that all logics of super-strict implications are (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  3.  25
    Glivenko sequent classes and constructive cut elimination in geometric logics.Giulio Fellin, Sara Negri & Eugenio Orlandelli - 2023 - Archive for Mathematical Logic 62 (5):657-688.
    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 based on a notion of embeddability of derivations. Additionally, conservativity for (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  4.  33
    Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate.Paolo Maffezioli & Eugenio Orlandelli - 2019 - Bulletin of the Section of Logic 48 (2):137-158.
    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 better understand and overcome the failure of (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  5.  78
    Proof-theoretic pluralism.Filippo Ferrari & Eugenio Orlandelli - 2019 - Synthese 198 (Suppl 20):4879-4903.
    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-theoretic pluralism—is much broader in scope than the one discussed in Beall (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  6.  39
    Free Quantified Epistemic Logics.Giovanna Corsi & Eugenio Orlandelli - 2013 - Studia Logica 101 (6):1159-1183.
    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.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  7.  52
    Proof theory for quantified monotone modal logics.Sara Negri & Eugenio Orlandelli - 2019 - Logic Journal of the IGPL 27 (4):478-506.
    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 elimination. It will also be shown that each of the calculi introduced (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  8.  18
    Proof Systems for Super- Strict Implication.Guido Gherardi, Eugenio Orlandelli & Eric Raidl - 2024 - Studia Logica 112 (1):249-294.
    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}\) -style labelled sequent calculi are investigated. It is shown that these calculi have the good structural properties that are distinctive (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  9.  33
    Logicality, Double-Line Rules, and Modalities.Norbert Gratzl & Eugenio Orlandelli - 2019 - Studia Logica 107 (1):85-107.
    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 claim that (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  10.  29
    Interpolation in Extensions of First-Order Logic.Guido Gherardi, Paolo Maffezioli & Eugenio Orlandelli - 2020 - Studia Logica 108 (3):619-648.
    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 orders, and various intuitionistic order theories such as apartness and positive partial (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  11.  13
    Quantified Modal Logics: One Approach to Rule (Almost) them All!Eugenio Orlandelli - forthcoming - Journal of Philosophical Logic:1-38.
    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 accessible world. Moreover (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  12.  19
    A Syntactic Proof of the Decidability of First-Order Monadic Logic.Eugenio Orlandelli & Matteo Tesi - 2024 - Bulletin of the Section of Logic 53 (2):223-244.
    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 (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  13.  38
    Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics.Eugenio Orlandelli - forthcoming - Logic and Logical Philosophy:1.
    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, they are (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark