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} (weakening down)
aw↑: S{a} → S{⊤} (weakening up)
ac↓: S{a} → S{a ∧ a} (contraction down)
ac↑: S{a ∨ a} → S{a} (contraction up)
s: S{(A ∧ B) ∨ C} → S{A ∧ (B ∨ C)} (switch/medial)

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	Introduction
↑	U+2191	Up	Elimination
∧	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.