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.
TalksI'm collecting the abstracts, here is a partial list:
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 alia we present some strengthenings of classical (but not well-known) results and an application to Jankov logic.
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's inversion principle. The setting of such enterprises are usually intuitionistic (and occasionally classic), but also linear propositional 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-commutativity of the structural comma.
- The peripherality requirement on discharge of assumptions, imposed on the implication-introduction rules in L.
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 of generalized application, we obtain a wal for L-grammars to express continuation-semantics without 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 PlansWork 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 . 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.
 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 , 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  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.
 Dale Miller and Elaine Pimentel, Linear logic as a framework for specifying sequent calculus. To appear in the Proceedings of Logic Colloquium 1999.
 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.
Room 359 for talks and room 357 for coffee breaks
Computer Science Department
Tel.: +49 (351) 463 38340 (Sylvia Epp, secretary)
See here how to reach us.
TimetableChanges are possible until the last minute.
Monday 27.9 morning
Monday 27.9 afternoon
Tuesday 28.9 morning
Tuesday 28.9 afternoon