**Abstract:**

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.

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.

To get to campus, take the train from Birmingham New Street to the University stop (7 minutes).

School of Mathematics

University of Birmingham

http://web.mat.bham.ac.uk/R.W.Kaye/

Dr Walter Dean

Department of Philosophy

University of Warwick

http://go.warwick.ac.uk/whdean