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 yields 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
→	U+2192	Rightwards arrow / Inference step	Reads downward, premise to conclusion
↓	U+2193	Downwards arrow / Down rule	Member of the cut-free fragment KS
↑	U+2191	Upwards arrow / Up rule	De Morgan dual of a down rule; admissible
∧	U+2227	Conjunction	Structural and logical conjunction coincide
∨	U+2228	Disjunction	Structural and logical disjunction coincide
¬	U+00AC	Negation	Pushed to atoms; duality is negation plus vertical flip
⊤, ⊥	U+22A4, U+22A5	Units	Premises of ai↓ and aw↓ respectively
S{ }	—	Context	A structure with a hole; a rule fires inside the hole
a	—	Atom	Propositional variable; restricting rules to atoms yields locality
s	—	Switch	The linear rule (A ∨ B) ∧ C → A ∨ (B ∧ C)
m	—	Medial	(A ∧ B) ∨ (C ∧ D) → (A ∨ C) ∧ (B ∨ D); makes contraction atomic
SKS, KS	—	Systems	The symmetric classical system and its down fragment
BV	—	System BV	Linear logic with a self-dual non-commutative connective

Metatheory. Deep inference erases the distinction between the root of a formula and its interior, and the payoff is locality: Brünnler and Tiu (2001) showed that in SKS identity, cut, weakening and contraction can all be restricted to atoms, which the sequent calculus cannot achieve for contraction, and medial is exactly what makes atomic contraction possible. Cut elimination survives as admissibility of the up rules — the down fragment KS is complete for classical propositional logic on its own — but it is proved by splitting or by decomposition, not by Gentzen's induction, since there is no principal formula at a root to induct on. Proof complexity is where the gain is measurable: Bruscoli and Guglielmi showed SKS has polynomial proofs of the Statman tautologies, which have no polynomial cut-free sequent proofs, and Jeřábek proved that the cut-free system KS quasipolynomially simulates Frege. Tiu (2006) proved system BV cannot be presented in the sequent calculus at all.

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

Limitations. Locality comes at the loss of the boundary Gentzen's methods relied on: with no principal formula at a root, cut elimination cannot be proved by induction on cut rank, and each system needs its own splitting or decomposition argument — there is no theorem covering the family. The same freedom inflates proof search, since a rule may apply at every position in a structure; Kahramanoğulları (2008) proved that provability in system BV, though linear and contraction-free, is NP-complete. Normalization is not canonical: splitting, decomposition and atomic flows coexist and yield different normal forms, so the formalism does not by itself settle proof identity, and derivations differing only in the order of independent deep steps remain distinct objects. Locality also raises the rule count — making identity, cut, weakening and contraction atomic requires medial and a larger rule set than the corresponding sequent calculus.