Deep Inference

Origin. Guglielmi and others developed deep inference (2000s). Rules apply inside formulas, not just at root. Calculus of structures: main formalism. Enables new proof transformations. More symmetric than sequent calculus.

Models. Inference inside formulas. Sequent calculus: rules apply at formula boundary. Deep inference: rules apply anywhere in structure. Formulas are structures. Enables proof compression and new normalizations.

Formalism.

Structures (formulas): S ::= a | S ∧ S | S ∨ S | ¬S | ⊤ | ⊥

Inference rule (in context): S{T} → S{U} means: replace T by U inside S.

Core rules (system SKS for classical logic):

ai↓: S{⊤} → S{a ∨ ¬a} (atomic identity)
ai↑: S{a ∧ ¬a} → S{⊥} (atomic cut)
aw↓: S{⊥} → S{a} (atomic weakening)
aw↑: S{a} → S{⊤} (atomic coweakening)
ac↓: S{a ∨ a} → S{a} (atomic contraction)
ac↑: S{a} → S{a ∧ a} (atomic cocontraction)
s: S{(A ∨ B) ∧ C} → S{A ∨ (B ∧ C)} (switch)
m: S{(A ∧ B) ∨ (C ∧ D)} → S{(A ∨ C) ∧ (B ∨ D)} (medial)

Every rule reads downward from premise to conclusion and must be sound in that direction, which fixes the shape of each pair. The identity rule introduces the excluded middle a ∨ ¬a from ⊤, and the cut collapses a ∧ ¬a to ⊥; the units and the connectives are determined together, since ⊥ → a ∧ ¬a and a ∨ ¬a → ⊤ are both sound but vacuous and prove nothing. The ↓ and ↑ members of each pair are De Morgan duals: turn the derivation upside down and negate, and ai↓ becomes ai↑, ac↓ becomes ac↑.

Switch and medial are different rules. Switch is the linear rule shared with system BV; medial has no analogue in the sequent calculus at all. Medial is the reason SKS exists in the form it does: once identity, cut and weakening are made atomic, contraction is the last remaining non-local rule, and it cannot be made atomic without medial (Tiu). Medial is sound because it is derivable from contraction and weakening. Both rules are self-dual, and both apply deep inside a formula while removing no connective.

Locality: a rule is local when applying it needs no inspection of structures of unbounded size. SKS is obtained from the general system SKSg by restricting identity, cut, weakening and contraction to their atomic forms and adding medial — which is exactly what buys locality. Switch and medial do mention unbounded A, B, C, D, but never duplicate or compare them, so on a tree representation each is a pointer exchange.

The down fragment: {ai↓, aw↓, ac↓, s, m} is the cut-free system KS, complete for classical propositional logic on its own. The up rules are admissible.

Deep vs shallow: Shallow: rules only at root (standard). Deep: rules at any depth in structure.

Proof compression: Deep inference proofs can be exponentially shorter. More proof transformations available.

System BV (linear logic + non-commutativity): Extends calculus of structures to capture more logics.

Symbols.

Symbol	Unicode	Name	Meaning
S{·}	—	Context	Structure with hole
→	U+2192	Derives	Inference step
↓	U+2193	Down rule	Cut-free fragment KS
↑	U+2191	Up rule	De Morgan dual; admissible
s	—	Switch	(A ∨ B) ∧ C → A ∨ (B ∧ C)
m	—	Medial	Makes contraction atomic
∧	U+2227	Conjunction	And
∨	U+2228	Disjunction	Or
⊤, ⊥	U+22A4, U+22A5	Units	True, false

Metatheory. Cut-elimination (atomic cut-elimination) holds. Proof compression: deep inference can be exponentially more succinct. Symmetric: up/down duality. Confluence: some systems confluent. NP-completeness for some search problems.

Applies to. Proof complexity. Proof search algorithms. Linear logic variants. Proof nets alternatives. Symmetric presentations of logic. Computational interpretations.

Limitations. Less familiar than sequent calculus. Rule application non-determinism. Tool support limited. Proof identity more complex. Adoption slower than sequent methods. Research community smaller.