Week 5, 28 October 2014 (16:00-18:00 Watson R17/18)

Hidenori Kurokawa (Kobe, Helsinki)

Title: The Principle of reflection via nested sequents


Sambin, Battilotti and Faggian (2000, JSL) propose a means of introducing logical constants by a proof-theoretic method which can broadly be understood as beloning to the framework of proof theoretic semantics. Roughly speaking, the idea is 1) to use an equivalence formula as a “definition” of a logical constant, 2) to derive ordinary operational rules in a cut-free sequent calculus for the logical constant using only via minimal background assumptions, and 3) to understand various non-classical logics as structural variants. The idea works well for multiplicative and additive conjunction and disjunction. But handling implication in this manner is more complicated.

I will propose a means of treating implication in this framework using a proof theoretic technique known as nested sequents which adheres as closely as possible to Sambin et al.’s conceptual motivations. Nested sequents have been use in modal logic as a natural proof-theoretic representation of Kripke semantics. I will argue, however, that there are better means of motivating nested sequents, both technically and philosophically.

On the philosophical side, I will first argue that there are conceptual problems arising in standard formulations of intuitionistic logic which point towards the adoption of strictly weaker logics. In formulate these concerns proof theoretically, it is often more convenient to use nested sequents rather than traditional sequent calculi. Once this step is undertaken, we can then show that nested sequents can be used to formulate a variety of non-classical logics in a uniform way. (I will present some new results, as well as surveying the literature.)

Time permitting, I will also discuss two further issues related to the proposed approach. One is the issue of how nested sequents can be compared with other generalizations of sequent calculi. The other is an open problem of extending this approach to Sambin’s treatment of quantifiers, which is related to his minimal foundation in constructive type theory.

About the seminar

The Midlands Logic Seminar was founded in 2011 and aims to cover all areas of mathematical logic, as well as related areas of theoretical computer science and philosophy of mathematics.

Study group

Our topic for Term 1 of 2014-2015 is the use of induction and heuristics in mathematical problem solving. We will be working through George Polya's book Induction and Analogy in Mathematics .


All meetings for Term 1 2014-15 will be Tuesday from 16:00-18:00 (study group 16:00-17:00, research talks 17:00-18:00) in room 310 of Watson Building (TBC) on the campus of the University of Birmingham.
  • campus map
  • google maps
    To get to campus, take the train from Birmingham New Street to the University stop (7 minutes).


    Dr Richard Kaye
    School of Mathematics
    University of Birmingham


    Dr Walter Dean
    Department of Philosophy
    University of Warwick