DI & CoS - Deep Inference in One Minute

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.

Shallow Inference		Deep Inference



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:

to shorten proofs, even by an exponential factor, compared to shallow inference, with no loss of analyticity;

to express logics that cannot be expressed in shallow-inference formalisms;

to make the proof theory of a really vast range of logics very regular and modular;

to design very simple deductive systems for logics that only have awkward ones in shallow inference;

to design deductive systems whose inference rules are all local, which is usually impossible in shallow inference;

to recover a De Morgan-like premiss-conclusion symmetry that is usually lost in shallow inference;

to obtain new notions of normalisation for proofs, in addition to cut elimination;

to inspire a new generation of proof nets and semantics of proofs;

to attack the problem of identity of proofs.

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.

Deep Inference Deep Inference in One Minute

Deep Inference
Deep Inference in One Minute