-
Natural deduction and normal form for intuitionistic linear logicArchive for Mathematical Logic. forthcoming.
-
A proof theoretical perspective on public announcement logicLogic and Philosophy of Science. forthcoming.
-
53Proof-theoretical analysis of order relationsArchive for Mathematical Logic 43 (3): 297-309. 2004.A proof-theoretical analysis of elementary theories of order relations is effected through the formulation of order axioms as mathematical rules added to contraction-free sequent calculus. Among the results obtained are proof-theoretical formulations of conservativity theorems corresponding to Szpilrajn’s theorem on the extension of a partial order into a linear one. Decidability of the theories of partial and linear order for quantifier-free sequents is shown by giving terminating methods of pr…Read more
-
25Alternative Axiomatization for Logics of Agency in a G3 CalculusFoundations of Science 28 (1): 205-224. 2021.In a recent paper, Negri and Pavlović (Studia Logica 1–35, 2020) have formulated a decidable sequent calculus for the logic of agency, specifically for a deliberative see-to-it-that modality, or dstit. In that paper the adequacy of the system is demonstrated by showing the derivability of the axiomatization of dstit from Belnap et al. (Facing the future: agents and choices in our indeterminist world. Oxford University Press, Oxford, 2001). And while the influence of the latter book on the study …Read more
-
121Reasoning About Collectively Accepted Group BeliefsJournal of Philosophical Logic 40 (4): 531-555. 2011.A proof-theoretical treatment of collectively accepted group beliefs is presented through a multi-agent sequent system for an axiomatization of the logic of acceptance. The system is based on a labelled sequent calculus for propositional multi-agent epistemic logic with labels that correspond to possible worlds and a notation for internalized accessibility relations between worlds. The system is contraction- and cut-free. Extensions of the basic system are considered, in particular with rules th…Read more
-
284Does the deduction theorem fail for modal logic?Synthese 187 (3): 849-867. 2012.Various sources in the literature claim that the deduction theorem does not hold for normal modal or epistemic logic, whereas others present versions of the deduction theorem for several normal modal systems. It is shown here that the apparent problem arises from an objectionable notion of derivability from assumptions in an axiomatic system. When a traditional Hilbert-type system of axiomatic logic is generalized into a system for derivations from assumptions, the necessitation rule has to be m…Read more
-
191The Church–Fitch knowability paradox in the light of structural proof theorySynthese 190 (14): 2677-2716. 2012.Anti-realist epistemic conceptions of truth imply what is called the knowability principle: All truths are possibly known. The principle can be formalized in a bimodal propositional logic, with an alethic modality ${\diamondsuit}$ and an epistemic modality ${\mathcal{K}}$, by the axiom scheme ${A \supset \diamondsuit \mathcal{K} A}$. The use of classical logic and minimal assumptions about the two modalities lead to the paradoxical conclusion that all truths are known, ${A \supset \mathcal{K} A}…Read more
-
8Admissibility of structural rules for extensions of contraction-free sequent calculiLogic Journal of the IGPL 9 (4): 541-548. 2001.The contraction-free sequent calculus G4 for intuitionistic logic is extended by rules following a general rule-scheme for nonlogical axioms. Admissibility of structural rules for these extensions is proved in a direct way by induction on derivations. This method permits the representation of various applied logics as complete, contraction- and cut-free sequent calculus systems with some restrictions on the nature of the derivations. As specific examples, intuitionistic theories of apartness and…Read more
-
30The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensionsAnnals of Pure and Applied Logic 174 (8): 103285. 2023.
-
38Mathesis Universalis, Computability and Proof (edited book)Springer Verlag. 2019.In a fragment entitled Elementa Nova Matheseos Universalis Leibniz writes “the mathesis [...] shall deliver the method through which things that are conceivable can be exactly determined”; in another fragment he takes the mathesis to be “the science of all things that are conceivable.” Leibniz considers all mathematical disciplines as branches of the mathesis and conceives the mathesis as a general science of forms applicable not only to magnitudes but to every object that exists in our imaginat…Read more
-
20Glivenko sequent classes and constructive cut elimination in geometric logicsArchive 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
-
9Geometric Rules in Infinitary LogicIn Ofer Arieli & Anna Zamansky (eds.), Arnon Avron on Semantics and Proof Theory of Non-Classical Logics, Springer Verlag. pp. 265-293. 2021.Large portions of mathematics such as algebra and geometry can be formalized using first-order axiomatizations. In many cases it is even possible to use a very well-behaved class of first-order axioms, namely, what are called coherent or geometric implications. Such class of axioms can be translated to inference rules that can be added to a sequent calculus while preserving its structural properties. In this work, this fundamental result is extended to their infinitary generalizations as extensi…Read more
-
16Proof-Theoretic Analysis of the Logics of Agency: The Deliberative STITStudia Logica 109 (3): 473-507. 2020.A sequent calculus methodology for systems of agency based on branching-time frames with agents and choices is proposed, starting with a complete and cut-free system for multi-agent deliberative STIT; the methodology allows a transparent justification of the rules, good structural properties, analyticity, direct completeness and decidability proofs.
-
50Proof theory for quantified monotone modal logicsLogic 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
-
44Conditional beliefs: From neighbourhood semantics to sequent calculusReview of Symbolic Logic 11 (4): 736-779. 2018.The logic of Conditional Beliefs has been introduced by Board, Baltag, and Smets to reason about knowledge and revisable beliefs in a multi-agent setting. In this article both the semantics and the proof theory for this logic are studied. First, a natural semantics forCDLis defined in terms of neighbourhood models, a multi-agent generalisation of Lewis’ spheres models, and it is shown that the axiomatization ofCDLis sound and complete with respect to this semantics. Second, it is shown that the …Read more
-
17The Logic of Conditional Beliefs: Neighbourhood Semantics and Sequent CalculusIn Lev Beklemishev, Stéphane Demri & András Máté (eds.), Advances in Modal Logic, Volume 11, Csli Publications. pp. 322-341. 2016.
-
17Recent Advances in Proof Systems for Modal LogicIn Rajeev Goré, Barteld Kooi & Agi Kurucz (eds.), Advances in Modal Logic, Volume 10, Csli Publications. pp. 421-422. 2014.
-
7Sequent Calculus in Natural Deduction StyleJournal of Symbolic Logic 66 (4): 1803-1816. 2001.A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. Therefo…Read more
-
26The intensional side of algebraic-topological representation theoremsSynthese 198 (Suppl 5): 1121-1143. 2017.Stone representation theorems are a central ingredient in the metatheory of philosophical logics and are used to establish modal embedding results in a general but indirect and non-constructive way. Their use in logical embeddings will be reviewed and it will be shown how they can be circumvented in favour of direct and constructive arguments through the methods of analytic proof theory, and how the intensional part of the representation results can be recovered from the syntactic proof of those…Read more
-
73Tychonoff's theorem in the framework of formal topologiesJournal of Symbolic Logic 62 (4): 1315-1332. 1997.
-
73Proofs and Countermodels in Non-Classical LogicsLogica Universalis 8 (1): 25-60. 2014.Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the correspon…Read more
-
104Cut Elimination in the Presence of AxiomsBulletin of Symbolic Logic 4 (4): 418-435. 1998.A way is found to add axioms to sequent calculi that maintains the eliminability of cut, through the representation of axioms as rules of inference of a suitable form. By this method, the structural analysis of proofs is extended from pure logic to free-variable theories, covering all classical theories, and a wide class of constructive theories. All results are proved for systems in which also the rules of weakening and contraction can be eliminated. Applications include a system of predicate l…Read more
-
18Equality in the Presence of Apartness: An Application of Structural Proof Analysis to Intuitionistic AxiomaticsPhilosophia Scientiae 61-79. 2006.The theories of apartness, equality, and n-stable equality are presented through contraction- and cut-free sequent calculi. By methods of proof analysis, a purely proof-theoretic characterization of the equality fragment of apartness is obtained.
-
50Sequent calculus proof theory of intuitionistic apartness and order relationsArchive for Mathematical Logic 38 (8): 521-547. 1999.Contraction-free sequent calculi for intuitionistic theories of apartness and order are given and cut-elimination for the calculi proved. Among the consequences of the result is the disjunction property for these theories. Through methods of proof analysis and permutation of rules, we establish conservativity of the theory of apartness over the theory of equality defined as the negation of apartness, for sequents in which all atomic formulas appear negated. The proof extends to conservativity re…Read more
-
34Glivenko sequent classes in the light of structural proof theoryArchive for Mathematical Logic 55 (3-4): 461-473. 2016.In 1968, Orevkov presented proofs of conservativity of classical over intuitionistic and minimal predicate logic with equality for seven classes of sequents, what are known as Glivenko classes. The proofs of these results, important in the literature on the constructive content of classical theories, have remained somehow cryptic. In this paper, direct proofs for more general extensions are given for each class by exploiting the structural properties of G3 sequent calculi; for five of the seven …Read more
-
61Geometrisation of first-order logicBulletin of Symbolic Logic 21 (2): 123-163. 2015.That every first-order theory has a coherent conservative extension is regarded by some as obvious, even trivial, and by others as not at all obvious, but instead remarkable and valuable; the result is in any case neither sufficiently well-known nor easily found in the literature. Various approaches to the result are presented and discussed in detail, including one inspired by a problem in the proof theory of intermediate logics that led us to the proof of the present paper. It can be seen as a …Read more