Two talks for Friday, 4 May 2012

System L syntax for sequent calculus

We recall two related syntaxes for focalised logic (linear and classical), derived from Curien-Herbelin’s duality of computation work, that have been proposed by Munch-Maccagnoni in 2009 and (for the classical case) by Curien – Munch-Maccagnoni in 2010.  We explain how the latter (with explicit “shifts”, i.e. change-of-polarity operators) is an “indirect style” version of the former. We explain their relation with tensor logic and LLP. We then discuss bilateral systems, in which the duality positive/negative is made distinct from the duality  programme/context.   We recover (a sequent calculus version of) Levy’s Call-By-Push-Value as a fragment, and we discuss the conditions under which the shifts are or are not forced to  define the monad of continuations. This last part is developped in collaboration with Marcelo Fiore.  Slides are available at http://www.pps.jussieu.fr/~curien/Bath-2012.pdf.

We develop a system called Polarized Intuitionistic Logic (PIL).  This logic predates, and is similar to the logic “ICL,” which was the subject of other talks.  However, while ICL has more of the characteristics of an intermediate logic with a natural deduction and term calculus, the goal of PIL is to *combine* classical logic and intuitionistic logic into a single system, both semantically and proof-theoretically.  We begin by describing a double-negation translation of classical logic into intuitionistic logic, then assign polarities to the translated formulas.  We then use an intuitionistic, focused sequent calculus to show that the translations of the classical connectives observe focalization, which is to say that they are valid as synthetic connectives. The sequent calculus we derive merges LJ and a version of LC, in which classical proofs also have access to a *stoup*. This combination is much more than a disjoint union: classical and intuitionistic connectives can freely mix without either destroying the other.  Kripke and algebraic semantics are also defined for this logic.Note: this logic was the subject of an earlier talk given in June 2011.  However, a totally different approach is used to describe the logic and there will also be much material that is entirely new.