
3ProofTheoretic Analysis of the Logics of Agency: The Deliberative STITStudia Logica 135. forthcoming.A sequent calculus methodology for systems of agency based on branchingtime frames with agents and choices is proposed, starting with a complete and cutfree system for multiagent deliberative STIT; the methodology allows a transparent justification of the rules, good structural properties, analyticity, direct completeness and decidability proofs.

16Proof 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

20Conditional beliefs: From neighbourhood semantics to sequent calculusReview of Symbolic Logic 11 (4): 736779. 2018.The logic of Conditional Beliefs has been introduced by Board, Baltag, and Smets to reason about knowledge and revisable beliefs in a multiagent 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 multiagent 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

8The 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. 322341. 2016.

5Recent Advances in Proof Systems for Modal LogicIn Rajeev Goré, Barteld Kooi & Agi Kurucz (eds.), Advances in Modal Logic, Volume 10, Csli Publications. pp. 421422. 2014.

4Sequent Calculus in Natural Deduction StyleJournal of Symbolic Logic 66 (4): 18031816. 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

12The intensional side of algebraictopological representation theoremsSynthese 123. forthcoming.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 nonconstructive 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

37A normalizing system of natural deduction for intuitionistic linear logicArchive for Mathematical Logic 41 (8): 789810. 2002.The main result of this paper is a normalizing system of natural deduction for the full language of intuitionistic linear logic. No explicit weakening or contraction rules for formulas are needed. By the systematic use of general elimination rules a correspondence between normal derivations and cutfree derivations in sequent calculus is obtained. Normalization and the subformula property for normal derivations follow through translation to sequent calculus and cutelimination

14University of Azores, Ponta Delgada, Azores, Portugal June 30–July 4, 2010Bulletin of Symbolic Logic 17 (3). 2011.

82Varieties of linear calculiJournal of Philosophical Logic 31 (6): 569590. 2002.A uniform calculus for linear logic is presented. The calculus has the form of a natural deduction system in sequent calculus style with general introduction and elimination rules. General elimination rules are motivated through an inversion principle, the dual form of which gives the general introduction rules. By restricting all the rules to their singlesuccedent versions, a uniform calculus for intuitionistic linear logic is obtained. The calculus encompasses both natural deduction and seque…Read more

123Proof Theory for Modal LogicPhilosophy Compass 6 (8): 523538. 2011.The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

13Admissibility of Structural Rules for ContractionFree Systems of Intuitionistic LogicJournal of Symbolic Logic 65 (4): 14991518. 2000.We give a direct proof of admissibility of cut and contraction for the contractionfree sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multisuccedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs. i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi.

49The continuum as a formal spaceArchive for Mathematical Logic 38 (7): 423447. 1999.A constructive definition of the continuum based on formal topology is given and its basic properties studied. A natural notion of Cauchy sequence is introduced and Cauchy completeness is proved. Other results include elementary proofs of the Baire and Cantor theorems. From a classical standpoint, formal reals are seen to be equivalent to the usual reals. Lastly, the relation of real numbers as a formal space to other approaches to constructive real numbers is determined

48Proofs and Countermodels in NonClassical LogicsLogica Universalis 8 (1): 2560. 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 nonclassical 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

63Cut Elimination in the Presence of AxiomsBulletin of Symbolic Logic 4 (4): 418435. 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 freevariable 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

13Equality in the Presence of Apartness: An Application of Structural Proof Analysis to Intuitionistic AxiomaticsPhilosophia Scientiae 6179. 2006.

12Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen’s Altitude Line ConstructionIn Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science, De Gruyter. pp. 269290. 2016.

249Sequent calculus in natural deduction styleJournal of Symbolic Logic 66 (4): 18031816. 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

27Glivenko sequent classes in the light of structural proof theoryArchive for Mathematical Logic 55 (34): 461473. 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

29Geometrisation of firstorder logicBulletin of Symbolic Logic 21 (2): 123163. 2015.That every firstorder 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 wellknown 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

60Tychonoff's theorem in the framework of formal topologiesJournal of Symbolic Logic 62 (4): 13151332. 1997.

103Proof Analysis in Modal LogicJournal of Philosophical Logic 34 (56): 507544. 2005.A general method for generating contraction and cutfree sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also GödelLöb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems.

43Contractionfree sequent calculi for geometric theories with an application to Barr's theoremArchive for Mathematical Logic 42 (4): 389401. 2003.Geometric theories are presented as contraction and cutfree systems of sequent calculi with mathematical rules following a prescribed rulescheme that extends the scheme given in Negri and von Plato. Examples include cutfree calculi for Robinson arithmetic and real closed fields. As an immediate consequence of cut elimination, it is shown that if a geometric implication is classically derivable from a geometric theory then it is intuitionistically derivable.

12Equality in the Presence of Apartness: An Application of Structural Proof Analysis to Intuitionistic AxiomaticsPhilosophia Scientae 6179. 2006.

37Sequent calculus proof theory of intuitionistic apartness and order relationsArchive for Mathematical Logic 38 (8): 521547. 1999.Contractionfree sequent calculi for intuitionistic theories of apartness and order are given and cutelimination 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

31Kripke completeness revisitedIn Giuseppe Primiero (ed.), Acts of Knowledge: History, Philosophy and Logic, College Publications. pp. 233266. 2009.

78Proof analysis in intermediate logicsArchive for Mathematical Logic 51 (12): 7192. 2012.Using labelled formulae, a cutfree sequent calculus for intuitionistic propositional logic is presented, together with an easy cutadmissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the Gödel–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive…Read more

15Tychonoff's Theorem in the Framework of Formal TopologiesJournal of Symbolic Logic 62 (4): 13151332. 1997.

33Prooftheoretical analysis of order relationsArchive for Mathematical Logic 43 (3): 297309. 2004.A prooftheoretical analysis of elementary theories of order relations is effected through the formulation of order axioms as mathematical rules added to contractionfree sequent calculus. Among the results obtained are prooftheoretical 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 quantifierfree sequents is shown by giving terminating methods of pr…Read more

University of HelsinkiDepartment of Philosophy (Theoretical Philosophy, Practical Philosophy, Philosophy in Swedish)Professor