Alessio Guglielmi's Research and Teaching / Deep Inference / Deep Inference in One Minute

Deep Inference
Deep Inference in One Minute

This page is for experts in proof theory.

We call 'shallow inference' the methodology behind the traditional formalisms of proof theory: Hilbert-Frege systems, natural deduction, sequent calculus, etc. In all these formalisms, inference rules can only be applied at the root of formulae (or sequents, or other structures). This rigidly constrains deduction, and a great deal of readily available information in formulae is not used.

In deep-inference formalisms, like the calculus of structures, inference rules can be applied anywhere. This way, all the information is available to deduction.

Deep inference can be exploited in many ways, and notably:

If it's such a simple idea, why wasn't deep inference exploited before? Perhaps, the main reason is that deep inference breaks at the core the traditional normalisation techniques. For example, in a typical cut elimination step, one needs to deal with the following situation:

Γ, A   Γ, B    -A, -B, Δ
------------   ------------
 Γ, A ∧ B     -A ∨ -B, Δ
 ------------------------- .
          Γ, Δ

We know how to normalise this piece of proof, because we know that the formulae A ∧ B and -A ∨ -B are 'broken at their root' by the shallow-inference rules. However, this is not true in the case of deep inference. This crucial piece of information is missing, so new techniques for normalisation need to be developed. This is far from trivial. For the calculus of structures, we developed fairly general, new techniques, which not only prove cut elimination, but give us access to many other, very fine-grained normalisation notions, impossible in shallow inference.

30.3.2009Alessio Guglielmiemail