Alessio Guglielmi's Research and Teaching / Deep Inference / Current Research Topics and Open Problems

Deep Inference
Current Research Topics and Open Problems

In this page I list all open and currently explored research subjects I am aware of, in the area of deep inference and closely related matters. The solutions to most of these problems are instrumental in reaching the common goal of a comprehensive bureaucracy-free proof theory based on geometric methods.

Contents

  1. Introduction
  2. Calculus of Structures
    1. Classical, Intuitionistic and Intermediate Logics
    2. Linear Logic
    3. Modal Logic
    4. Commutative/Non-commutative Linear Logic
    5. Computability Logic
    6. Language Design
    7. Proof Search
    8. Implementations
  3. Formalism A
  4. Formalism B, Deductive Nets and Identity of Derivations
  5. Proof Nets and Semantics of Proofs
  6. Deep Inference and Display Calculus
  7. Deep Inference and Hypersequents
  8. Subatomic Proof Theory
  9. Causal Quantum Evolution

1Introduction

In very few words, what we do is looking for the best syntax and the best semantics for proofs (notice that semantics of proofs is a very different thing from semantics of formulae!). It is necessary to improve on the current state of the art in structural proof theory in order to solve important open problems like that of identity of proofs. By employing deep inference, which yields the necessary flexibility for the task, we are making very fast progress.

In case I can assess the difficulty of a topic with reasonable confidence, I rate it according to the following scale:
= simple project for an expert researcher, MSc thesis;
= complex project, suitable for a PhD thesis;
= major or very risky research project.

Please keep in mind that there are three conceptual levels to distinguish, and an associated terminology I'm trying to stick to:

I'm trying to avoid the word 'calculus' as much as possible, because it can ambiguously denote a formalism and a proof system, which are very different things for us.

A logic is considered independent of its proof systems. Very roughly, a logic can simply be considered the set of formulae which are true according to some criterion.

I also distinguish between derivation and proof: a derivation is any object in a proof system, normally the establishing of a conclusion from some premisses; a proof is a derivation without premisses, so it's the derivation of a tautology.

I am always very happy to hear from students and colleagues and to discuss these topics. Consider also using our friendly and responsive mailing list Frogs. Please let me know of problems and conjectures you think should be listed here, and also let me know if anything in this page is obsolete or incorrect.

The following pages contain interesting open problems related to those in this page, and different takes on the same problems one finds below:

2Calculus of Structures

The calculus of structures (CoS) is now mature for logics with involutive negation. This means that for classical logic, for linear logic in all its classical fragments and for modal logics, presentations in CoS exist and their main proof theoretic properties are established, together with the novel properties provided by deep inference. The major, general, but probably not very difficult open problem in the CoS area is:

A general class of possibly interesting problems is:

I will now proceed to examine more circumscribed areas inside CoS.

2.1Classical, Intuitionistic and Intermediate Logics

The best expert of the proof theory of classical logic in CoS is Kai Brünnler and the best starting point is his thesis Deep Inference and Symmetry in Classical Proofs.

2.2Linear Logic

2.3Modal Logic

2.4Commutative/Non-commutative Linear Logic

2.5Computability Logic

Computability logic is a logic motivated by an intuitive semantics of computation, recently conceived by Giorgi Japaridze. It's rather clear already that a good proof theory for it, i.e., proof systems with good properties, is going to require some form of deep inference.

I agree with Giorgi that a logic should mostly be conceived out of semantic needs, and I agree also that this is not really the case with linear logic (he argues about this here). Since computability logic looks very challenging for the traditional syntactic formalisms, it's interesting to see whether the more liberal attitude of deep inference can make for a successful marriage.

Giorgi made some interesting progress with his cirquent calculus, where he shows a proof system adopting a new notion of sharing.

2.6Language Design

There is a broad, ongoing research effort about understanding languages for concurrency, especially process algebras, like CCS and the π-calculus, in a logical setting. For example, one would like to establish a close correspondence between, say, computations in CCS and derivations in some cut-free proof system, like NEL.

Proof theory can be considered a way to explore and exploit the internal symmetries of a language. By doing so for computational languages one hopes to put to use (like, say, in verification of protocols), the plasticity of proof manipulation, which is especially powerful in deep inference.

Establishing a strong connection between proofs and (concurrent) computation means also unifying their semantics. I believe that the future of semantics of proofs, as well as that of semantics of concurrent computations, lies in the use of algebraic topology methods, which will be applied starting from deductive nets. So, this thread of research fits in our general scheme of finding the best semantics of proofs.

I call this thread 'language design' because ultimately we will create new languages: the odds that the old ones perfectly fit proof theory are rather slim! But don't worry, good proof theory does not create monsters; actually, there are chances of smoothing out some of the rough edges of languages designed without a clear understanding of symmetry.

An interesting possibility exists about unifying, at the level of languages, the two fields of planning and concurrency. Planning, or reasoning about actions, is an area of artificial intelligence concerned about scheduling actions for solving specified tasks. Clearly, this is an inherently concurrent activity. Many languages for planning are very close to logic, for example those in the neighbourhood of logic programming. So, an investigation aiming at providing a common linguistic setting can be both interesting and fruitful.

A good reason for doing so is that, again, semantics of concurrent computations could be applied in the case of planning. Apart from its intrinsic interest, I also see a political interest in this research. Artificial intelligence seems to be resisting all formal methods which require more technical expertise than that of high school students. It looks to me that AI is trying to make progress by connecting philosophical intuition directly to engineering; this (of course!!) cannot work: a solid scientific layer in the middle is needed. So, we'd like modestly to contribute to this scientific layer.

2.7Proof Search

It's great to have the freedom and expressiveness of CoS, but for proof search more freedom means a larger search space, what we need to restrict if we look for implementations of our proof systems. Splitting theorems are the key to reducing nondeterminism, because they allow for a trade-off between length of proofs and width of the search space, and this ratio can be varied at will. We are now in the same situation as the sequent calculus was before Dale Miller introduced the notion of uniform provability, which is a way of matching provability and the kind of goal-drivenness necessary in implementations.

2.8Implementations

3Formalism A

There is still no real name for what I call formalism A. This is the first in a two step movement for removing all bureaucracy induced by permutation of rules in CoS and in all other formalisms. The movement should also lead us to deductive nets (see below). Formalism A doesn't yield the final victory over bureaucracy, but it is a very convenient and straightforward formalism, arguably of independent interest. It should allow representing and conveniently studying a very vast array of logics.

4Formalism B, Deductive Nets and Identity of Derivations

One of the major goals of our research is obtaining deductive nets. These objects should be derivations without bureaucracy, and such that the mathematical argument the derivation stands for is immediately readable from the corresponding deductive net.

Right now, all formalisms for proof systems suffer from bureaucracy: for example, one can always come up with two proofs of the same sentence that are morally the same but differ in inessential details, such as the permutation of two inference rules upon two independent subformulae.

In proof nets (which come in several variations over a notion that Jean-Yves Girard introduced), there is no bureaucracy. However, proof nets are not deductive, because it's very difficult, by simply looking at a proof net, to know what is the argument of the proof, and even if the net stands for a valid proof (technically, in the sense of proof complexity,proof nets are not a proof system). The correctness of the net must be checked by a correctness criterion, which in general is a rather complex algorithm, or perhaps a simple but computationally expensive one.

So, the chase is open for a formalism that is both bureaucracy-free and deductive. Deductive nets should be both bureaucracy-free derivations of some proof system and graphical objects, such that they can be manipulated and studied by geometric methods.

The first natural candidate for a logic for which to accomplish this is, of course, classical logic. Its deductive nets would be the natural playground for solving the long-standing problem of identity of proofs, which asks for non-trivial criteria for comparing proofs. It is embarrassing for proof theory that this absolutely basic question still hasn't been answered!

Deep inference has two important assets: it allows for inference rules of very fine granularity and extreme regularity. Both aspects are key to our ability of manipulating graphs, which is what deductive nets ultimately will be.

My current working hypothesis is the following. What I call formalism B is the formalism in which to design proof systems that are bureaucracy-free and where to study the properties deductive nets should possess. A closely related but different problem is finding deductive nets; they should be suitable, geometric representations of derivations in formalism B.

There are currently several slightly different proposed definitions for formalism B, however I know what is the most important property they must possess: inference rules apply to derivations (as opposed to formulae/structures). What I know about B is in the note Formalism B. There is a discussion about bureaucracy and deductive nets in this Frogs list thread.

The most important goal of our research is giving satisfactory, non-trivial answers to the problem of identity of proofs, or, better, more in general, identity of derivations. This objective is important per se, and also because such broad, open objectives as this one typically spawn several lines of research just for making the tools necessary to solve the problem. This is what is happening to us, and I think this will continue to happen for a long time.

In the three problems mentioned above I was careful in not asking for the formalisms to be defined for a particular logic. This is so because I believe that the problem of addressing bureaucracy and identity of derivations is essentially formalism-dependent.

It seems to me that many people, especially coming from Girard's school, believe that these are problems (at least in part) dependent on the logic. I believe that this is just another illusion of the sequent calculus. These are problems of the formalism!

Anyway, if a logic is to be preferred for at least giving partial answers to the problems above, than this must clearly be classical logic (and not linear logic, say).

I recently became aware of a very interesting, independent characterisation of bureaucracy based on n-dimensional categories. Here is a description:

5Proof Nets and Semantics of Proofs

There is currently much activity going on in this area, especially about classical logic. Two questions are intimately related and motivate this research: What is the essence of a proof? and How can we eliminate bureaucracy from a proof?.

Suppose a mathematician produces a proof of a theorem: every known formal system admits several different representations of this proof, which differ in inessential details. Typically, the differences are in the order in which the inference rules are applied. After Girard, people call this phenomenon bureaucracy. In another section in this page I argue about deductive nets as a formalism which will get rid of bureaucracy. Finding deductive nets is no easy task, and there are two possible directions of attack: getting there from syntax and from semantics. Deep inference helps in finding our way on both fronts.

Semantics of proofs should not be confused with semantics of formulae. We all know that formulae can be given truth values by way of tarskian semantics, for classical logic, or frame semantics, for modal and intuitionistic logics, or other algebraic structures for other logics. The point of semantics of proofs is to give semantics to proofs themselves. This is normally done by building a category whose objects are formulas and whose arrows are derivations. It turns out that a very good way of capturing the essence of proofs is to to employ categories where the arrows are proof nets, i.e., derivations stripped of all bureaucracy. Proof nets also provide for very concrete, geometric objects, amenable to be dealt with by distributed algorithms. They provide insight on many aspects of theoretical computer science, for example they help in finding optimal computational models for functional programming languages.

Much of the inspiration in this area comes from considering proofs as functional programs, in the so called Curry-Howard correspondence. The meaning of a proof is normally an invariant for the cut elimination procedure, which is a way of computing the program associated to the proof. For too long, people believed that classical logic can not be given any meaningful semantics in this sense. Our point of view is that this was a consequence of the sequent calculus's misleading characteristics.

In fact, when proofs are looked at under the microscope of deep inference, many assumptions turn out to be false, because deep inference rules have a much smaller granularity than shallow inference ones, so many roadblocks can be removed, and one can see new, simpler proof nets, which in turn open new perspectives for semantics.

Experts in this area are François Lamarche and Lutz Straßburger. Richard McKinley recently started working on it by employing deep inference. Lutz keeps a web page about this subject, where more open problems are listed.

Currently, the area is in a state of rapid movement. Probably, concentrating on classical logic is what makes most sense, although proof nets for linear logic are certainly still interesting. I think the two most important 'open problems' are at the same time technical and sociopolitical, meaning that we should expect several proposals in addition to the existing ones, and at some point in the future one will prevail over the others, also based on intangible properties like beauty and luck.

6Deep Inference and Display Calculus

The display calculus of Nuel Belnap (Journal of Philosophical Logic, 11:375-417, 1982) is another, very general proof theoretical formalism, which employs a mechanism for making inferences anywhere deep inside formulae.

It enjoys the important property that any system in this formalism meeting eight simple conditions is guaranteed to enjoy cut admissibility. Jeremy Dawson and Rajeev Goré have formalised this general cut elimination proof in Isabelle, and have extended it to a proof of strong normalisation for all systems in the display calculus formalism (see Formalised Cut Admissibility for Display Logic). All of this suggests the following project:

I know a bit of display calculus, but am no expert. My personal take on this project is that it will be successful, i.e., it will be possible to use many of the ideas in display calculus for a very general cut elimination proof. By using CoS it will also be possible to simplify the technical treatment.

However, since I believe that the CoS version of deep inference is stronger than the one in the display calculus, I think it is impossible to find a general cut elimination proof for every CoS system (see the project below). The success of the display calculus stems from its strict control of the meta-level form, what instead in CoS is completely liberal. In fact, I believe the following project can be done:

7Deep Inference and Hypersequents

Deep inference is more general than hypersequents, and goes farther in the same direction, which is coping with the limitations of the sequent calculus meta level. I am not an expert of hypersequents, but Kai Brünnler, Rajeev Goré, Robert Hein, Charles Stewart and Phiniki Stouppa are.

8Subatomic Proof Theory

There is a fantastic possibility of studying most proof theory for most logics once and for all by examining a single proof system, entirely generated by a single rule. The trick is considering atoms as logical operations over units. You can find the basic observations in my (very rough and terse) notes Subatomic Logic and Some News on Subatomic Logic. The successful development of this theory depends crucially on our ability of proving splitting theorems. This is weird stuff, stay away from it!

9Causal Quantum Evolution

This is something absolutely fantastic, which I basically don't understand at all: it looks like system BV is able to describe quantum causal evolution. This physical phenomenon causes several problems to other logics which people considered for the task, like linear logic. The basic idea is to represent quantum states as propositions and interactions as axioms. Thus if a and b are states of two systems coming together and their interaction produces c, d and e, we would write

a, b |– c, d, e .

The question is: what sort of logic correctly captures entanglement and causality? It seems that BV is the only logic that does it properly. The secret of its success is apparently its ability to deal with a self-dual connective, intermediate between (linear) conjunction and disjunction.

20.11.2007Alessio Guglielmiemail