
272Proof Systems for Super Strict ImplicationStudia Logica 112 (1): 249294. 2023.This paper studies proof systems for the logics of superstrict implication ST2–ST5, which correspond to C.I. Lewis’ systems S2–S5 freed of paradoxes of strict implication. First, Hilbertstyle 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, G3style labelled sequent calculi are investigated. It is shown that these calculi have the good structural properties that are distinctive of G3sty…Read more

87Prooftheoretic pluralismSynthese 198 (Suppl 20): 48794903. 2019.Starting from a prooftheoretic perspective, where meaning is determined by the inference rules governing logical operators, in this paper we primarily aim at developing a prooftheoretic alternative to the modeltheoretic meaninginvariant logical pluralism discussed in Beall and Restall. We will also outline how this framework can be easily extended to include a form of meaningvariant logical pluralism. In this respect, the framework developed in this paper—which we label twolevel prooftheo…Read more

56Proof theory for quantified monotone modal logicsLogic Journal of the IGPL 27 (4): 478506. 2019.This paper provides a prooftheoretic study of quantified nonnormal modal logics. It introduces labelled sequent calculi based on neighbourhood semantics for the firstorder 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, heightpreserving admissibility of weakening and contraction and syntactic cut eliminati…Read more

45Free Quantified Epistemic LogicsStudia Logica 101 (6): 11591183. 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

43Sequent Calculi and Interpolation for NonNormal Modal and Deontic LogicsLogic and Logical Philosophy 1. forthcoming.G3style sequent calculi for the logics in the cube of nonnormal modal logics and for their deontic extensions are studied. For each calculus we prove that weakening and contraction are heightpreserving 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

38Logicality, DoubleLine Rules, and ModalitiesStudia Logica 107 (1): 85107. 2019.This paper deals with the question of the logicality of modal logics from a prooftheoretic 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 doubleline rules which, following Dos̆en’s analysis, allows us to…Read more

37Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence PredicateBulletin of the Section of Logic 48 (2): 137158. 2019.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 implicationfree 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

36SuperStrict ImplicationsBulletin of the Section of Logic 50 (1): 134. 2021.This paper introduces the logics of superstrict implications, where a superstrict 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 superstrict implications is obtained by strengthening the (normal) relational semantics for strict implication. We consider all logics of superstrict implications that are based on relational frames for modal logics in the modal cube. …Read more

34Interpolation in Extensions of FirstOrder LogicStudia Logica 108 (3): 619648. 2020.We prove a generalization of Maehara’s lemma to show that the extensions of classical and intuitionistic firstorder 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) firstorder logic with identity, as well as interpolation for several mathematical theories, including the theory of equivalence relations, (strict) partial and linear orde…Read more

30Glivenko sequent classes and constructive cut elimination in geometric logicsArchive for Mathematical Logic 62 (5): 657688. 2023.A constructivisation of the cutelimination 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 nonconstructive 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 ordinalfree by introducing a new wellfounded relation…Read more

28Proof Systems for Super Strict ImplicationStudia Logica 112 (1): 249294. 2024.This paper studies proof systems for the logics of superstrict implication \(\textsf{ST2}\) – \(\textsf{ST5}\), which correspond to C.I. Lewis’ systems \(\textsf{S2}\) – \(\textsf{S5}\) freed of paradoxes of strict implication. First, Hilbertstyle 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

27Quantified Modal Logics: One Approach to Rule (Almost) them All!Journal of Philosophical Logic 53 (4): 959996. 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 firstorder machinery and with nonrigid designators. The semantics is based on a primitive counterpart relation holding between ntuples of objects inhabiting possible worlds. This allows an object to be represented by one, many, or no object in an access…Read more

22A Syntactic Proof of the Decidability of FirstOrder Monadic LogicBulletin of the Section of Logic 53 (2): 223244. 2024.Decidability of monadic firstorder 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 firstorder logic in innex normal form which exploits G3style sequent calculi. In particular, we introduce a cut and contractionfree calculus having a (complexityoptimal) terminating proofsearch procedure. We also show that this l…Read more

18Doubleline Harmony in a Sequent SettingIn 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 doubleline 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.
Areas of Specialization
Science, Logic, and Mathematics 
Areas of Interest
Science, Logic, and Mathematics 