Alessio Guglielmi's Research and Teaching / Deep Inference / Deep Inference in One Minute
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.
Above there's the sequent-calculus inference
Γ, A B, Δ ------------ . Γ, A ∧ B, Δ
The part circled in red is the only one that can be inspected by the inference rule, and it can only occur at the root of the entire structure.
Above there's the calculus-of-structures inference
S((Γ ∨ A) ∧ (B ∨ Δ)) ---------------------- . S(Γ ∨ (A ∧ B) ∨ Δ)
The inference rule can be applied anywhere, i.e., S is an additional schematic variable.
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.