**ICCL Workshop
Proof Theory 2004
Technische Universität Dresden
September 27-28, 2004**

This meeting is dedicated to structural proof theory and related matters. The meeting will mostly take place on September 27 and 28.

**Participants**

- Kai Brünnler (Bern)
- Paola Bruscoli (TU Dresden)
- Ugo Dal Lago (Bologna)
- Jeremy Dawson (NICTA, Canberra)
- Roy Dyckhoff (St Andrews)
- Birgit Elbl (Universität der Bundeswehr München)
- José Espírito Santo (Universidade do Minho)
- Nissim Francez (Technion Haifa)
- Alessio Guglielmi (TU Dresden)
- Ozan Kahramanogullari (Leipzig)
- François Lamarche (LORIA, Nancy)
- Stéphane Lengrand (St Andrews and Paris VII)
- Michel Parigot (CNRS, Paris)
- Elaine Pimentel (Belo Horizonte and Torino)
- Charles Stewart (TU Dresden)
- Lutz Straßburger (LORIA, Nancy)

**Talks**

Deep Inference and Cut Elimination for Predicate Logic

Kai Brünnler (Bern)In my thesis I gave a proof of cut elimination for the presentation of predicate logic in the calculus of structures. This proof is indirect: it translates a proof to the sequent calculus by introducing lots of new cuts, makes use of Gentzen's cut elimination result, and translates back the cut-free proof. My talk will be about a new, direct proof without any reference to the sequent calculus.

On Light Logics, Uniform Encoding and Polynomial Time

Ugo Dal Lago (Bologna), joint work with Patrick Baillot (Paris 13)We investigate on the extensional expressive power of Light Affine Logic, analysing the class of uniformly representable functions for various fragments of the logic. We give evidence on the incompleteness (for polynomial time) of the propositional fragment. Following previous work, we show that second order leads to polytime unsoundness. We then introduce simple constraints on second order quantification and least fixpoints, proving the obtained fragment to be polytime sound and complete.

Focused Proof Systems in Intuitionistic Logic

Roy Dyckhoff (St Andrews)We survey results about several proof systems for intuitionistic logic, beginning with a paper by Vorob'ev and including work of Hudelmaier and Herbelin. All have the property that, in our notation, there are two kinds of sequent, in one of which the formula in a special place, here called the

focus, is the only possibility for use as principal formula.Inter aliawe present some strengthenings of classical (but not well-known) results and an application to Jankov logic.

The Lambda-CT-calculus

Birgit Elbl (Universität der Bundeswehr München)Lambda-CT is a calculus for modelling predicational computation where propagation of results is realized by delayed instantiation, and lambda abstraction and application can be used to define operations on predicates and goals as well as higher order functionals. We present the system and investigate properties of its reduction relation.

An Isomorphism Between Sequent Calculus and Natural Deduction for Minimal Logic

José Espírito Santo (Universidade do Minho)Roughly speaking, the traditional mappings between sequent calculus and natural deduction translate an elimination as a combination of a left introduction and a cut; translate a left introduction as a combination of an elimination and substitution; and translate cut as substitution. We show, for minimal logic, how to formulate sequent calculus and natural deduction in such a way that both systems have a cut rule and a substitution operation; and the left introduction rule, the cut rule and the substitution operation of the sequent calculus "correspond" to the elimination rule, the cut rule and the substitution operation of the natural deduction system. The correspondence between rules induces a correspondence between derivations: giving a derivation in one system, and replacing each occurrence of one rule by one occurrence of the corresponding rule, one obtains a derivation in the other system (up to "turning branches upside down"). This process defines a bijection between the two sets of derivations. Moreover, we may define, with the help of substitution, simple cut elimination rules in both systems in such a way that "cut-elimination" in the natural deduction system subsumes normalisation; and the bijection between the sets of derivations becomes an isomorphism between the two cut-elimination relations. In addition: (1) The isomorphism between the two systems, when the systems are presented as extensions of the simply typed lambda-calculus, may be described as an inversion of the associativity of application. (2) Traditional natural deduction, even in the extended sense of von Plato, is a common core of our systems.

Lambek Calculus with General Elimination-rules

Nissim Francez (Technion Haifa)In modern approaches to proof-theory natural-deduction (ND) proof systems are presented with

general elimination-rules (GE-rules), derived from a more general (re)formulation of Prawitz'sinversion principle. The setting of such enterprises are usually intuitionistic (and occasionally classic), but alsolinearpropositional calculi.The aim of this paper is to investigate the effect of passing to GE-rules in the (associative) Lambek-calculus

L, the heart of Type-Logical Grammar formalisms. The added dimensions here are the following.

- The
non-commutativityof the structural comma.- The
peripheralityrequirement on discharge of assumptions, imposed on the implication-introduction rules inL.These two issues pose certain questions about how should GE-rules for the

directed implications(the two residuals of the non-commutative product) be formulated. We suggest such a formulation, and show that, augmented by its Curry-Howard image ofgeneralized application, we obtain a wal for L-grammars to expresscontinuation-semanticswithout type-raising via CPSs, as proposed recently.

Splitting and Cut Elimination

Alessio Guglielmi (TU Dresden)Kai Brünnler's technique for proving cut elimination in deep inference presentations of classical logic is very compact, elegant and efficient from the point of view of complexity. However, it is possible further to improve on the size of cut free proofs by establishing a preliminary, so-called splitting theorem. The integration of the two techniques provides for a general, efficient and elegant cut elimination technique for a wide variety of logics in their deep inference presentation.

Labeled Event Structure Semantics of Plans—Work in Progress

Ozan Kahramanogullari (Leipzig)Labeled event structures (LES) is a model for concurrency which had been studied for linear logic proofs in the sequent calculus [1]. We investigate the LES semantics of planning problems by resorting to linear logic approach to planning within the calculus of structures presentation of linear logic. This way we establish a bridge between planning and concurrency which will allow for a structural analysis of plans. We argue that these methods can be carried to system NEL, the conservative extension of multiplicative exponential linear logic with a non-commutative operator, where plans can be naturally expressed.

[1] Alessio Guglielmi, Abstract logic programming in linear logic, independence and causality in a first order calculus, Ph.D. thesis, Università di Pisa, 1996.

What Is a Model of Linear Logic Without Units, and What Has It Got to Do with Classical Logic?

François Lamarche (LORIA, Nancy), joint work with Lutz Straßburger (LORIA, Nancy)The interplay between syntax and semantics in logic has been going on since at least Tarski, but there is always some discrepancy between the two. This is because semantical objects live in the real world, and syntactical objects live in the soft-camembert universe. Linear logic has been discovered by observation of a semantical entity, namely the category of coherence spaces and linear maps. There, there is some amount of degeneracy with the units, since 1 = \bot. The best syntax we have for linear logic (multiplicative proof nets) also have problems with units; in a recent paper with Lutz we give the best solution there is so far, but this solution sill involves some amount of quotienting and its complexity is not trivial.

Category theory is the bridge between the real world and the soft-camembert universe. For obvious historical reasons it has been inspired by the former, and much less by the latter (although there are very good exceptions, like Moggi monads). More than ten years ago I found a simple way to give a categorical axiomatization of a model of linear logic without units. It was very simple, next to trivial. I had no immediate use for it, and I never wrote it up, and I am not certain at all it has been mentioned by other authors.

Some problems related to the use of units in classical proof nets have made take this idea out of the mothballs, and now it is obvious that it gives a lot back for a very small investment.

This recent research is an opportunity to introduce some elementary, but very important ideas of category theory to beginners.

Normalising Permutations in Sequent Calculus

Stéphane Lengrand (St Andrews and Paris VII)In Prawitz's translation from the sequent calculus LJ to natural deduction, many proofs are mapped to the same one and only differ by the order in which inference rules are applied. One can be transformed into another by simple permutations of these rules. By the use of focusing conditions, a canonical proof can be elected in each permutation class, thus forming Herbelin's permutation-free calculus LJT, which is in bijection with proofs in natural deduction. The cut-elimination in LJT can simulate beta (in other words, normalisation in natural deduction), but has little to do with Gentzen-style cut-elimination in LJ. Previous attempts to unify a Gentzen-style cut-elimination with normalisation in natural deduction seem to be flawed. Moreover, previous systems of permutation rules, by the use of which proofs in LJ can be turned into canonical ones, fail to be strongly normalising. We show how permutations can be turned into a normalising system incorporated to a cut-elimination process that unifies that of LJ and that of LJT (and hence simulates beta-reduction).

Constructive Existence in Classical Logic

Michel Parigot (CNRS, Paris)

On the Specification of Sequent Systems

Elaine Pimentel (Belo Horizonte and Torino), joint work with Dale Miller (INRIA and École Polytechnique, Paris)As described in [1], Linear Logic can be used as a framework for specifying sequent calculus. Since the encodings were done in a very natural and direct way, it was possible to use the rich meta-theory of linear logic to help on drawing conclusions about object-level proof systems. The work done in [2] goes one step further and shows a characterization that implies the cut-elimination property on specified systems. The goal of the present work is to show a complete characterization of the property: the initial axiom can be replaced by its atomic version. Also we'll discuss about adding the notions of induction and definition to a fragment of Linear Logic in order to present a semi-automatized proof of cut-elimination for the specified systems.

References:

[1] Dale Miller and Elaine Pimentel,

Linear logic as a framework for specifying sequent calculus. To appear in the Proceedings of Logic Colloquium 1999.[2] Dale Miller and Elaine Pimentel,

Using linear logic to reason about sequent systems. LNCS, Proceedings of Tableaux 2002.

Towards a Proof-theoretical Justification for Intersection Types

Elaine Pimentel (Belo Horizonte and Torino), joint work with Simona Ronchi della Rocca (Torino) and Luca Roversi (Torino)It is well known that derivations in Intersection Types (IT) form a strict subset of deductions in Intuitionistic Logic (LJ) -- up to term decorations -- in the sense that IT imposes a meta-theoretical restriction on proofs: conjunction can be introduced only between derivations that are synchronized with respect to the implication.

The goal of this work is to present a proof-theoretical justification for IT. In particular, we discuss the relationship between the intersection connective and the intuitionistic conjunction. For this purpose, we define a new logical system called Intersection Synchronous Logic (ISL), that proves properties of sets of deductions of the implication-conjunction fragment of LJ.

The main idea behind ISL is the decomposition of the intuitionistic conjunction into two connectives, one with synchronous and the other with asynchronous behavior.

Also in the present work, we prove that ISL enjoys both the strong normalization and sub-formula properties as well as that the Intersection Type assignment can be viewed as standard term decoration of ISL.

Notions of Derivability for the Modal Logic S5 in the Calculus of Structures

Charles Stewart (TU Dresden)Generally we are interested in cut-free, or analytic, derivability from the point of view of theoremhood, and are not usually concerned with the consequences derivable from a formula. The notion becomes interesting if we want to look at the fine structure of cut-free proofs.

The calculus of structures has a rather richer notion of analytic derivability than either the sequent calculus or natural deduction; particularly of interest is the case of S5 where there is a great deal of freedom in formalising the calculus, leading to a family of notions of derivability. I will attempt to relate this fine structure firstly to questions of proof search, and secondly to try and cast more light on the calculus-independant question of what is an analytic proof.

From Proof Nets to the Free *-Autonomous Category

Lutz Straßburger (LORIA, Nancy), joint work with François Lamarche (LORIA, Nancy)In the first part of this talk we present a theory of proof nets for full multiplicative linear logic, including the two units. It naturally extends the well-known theory of unit-free multiplicative proof nets. A linking is no longer a set of axiom links but a tree in which the axiom links are subtrees. These trees will be identified according to an equivalence relation based on a simple form of graph rewriting. We show the standard results of sequentialization and strong normalization of cut elimination. In the second part of the talk we show that the identifications enforced on proofs are such that our proof nets form the arrows of the free *-autonomous category.

**Venue**

Room 359 for talks and room 357 for coffee breaks

Computer Science Department

Hans-Grundig-Str. 25

01307 Dresden

Tel.: +49 (351) 463 38340 (Sylvia Epp, secretary)

See here how to reach us.

**Timetable**

**Monday 27.9 morning **

- 9:00-10:10 Birgit Elbl
- 10:20-11:30 Nissim Francez
- 11:45-12:30 Ugo Dal Lago

**Monday 27.9 afternoon**

- 13:45-14:45 Lutz Straßburger
- 15:00-16:00 François Lamarche
- 16:15-17:30 Elaine Pimentel
- 17:45-18:45 Charles Stewart

**Tuesday 28.9 morning**

- 9:00-10:00 Roy Dyckhoff
- 10:15-11:15 Stéphane Lengrand
- 11:30-12:30 José Espírito Santo

**Tuesday 28.9 afternoon**

- 13:45-14:45 Michel Parigot
- 15:00-16:00 Kai Brünnler
- 16:15-17:00 Ozan Kahramanogullari
- 17:15-18:00 Alessio Guglielmi

24.9.2004Alessio Guglielmiemail