Editing Deep inference

{{Technical|date=August 2022}}
In [[mathematical logic]], '''deep inference''' names a general idea in [[structural proof theory]] that breaks with the classical [[sequent calculus]] by generalising the notion of [[abstract structure|structure]] to permit inference to occur in contexts of high structural complexity.  The term ''deep inference'' is generally reserved for [[proof calculi]] where the structural complexity is unbounded; in this article we will use '''non-shallow inference''' to refer to calculi that have structural complexity greater than the sequent calculus, but not unboundedly so, although this is not at present established terminology.

Deep inference is not important in logic outside of structural proof theory, since the phenomena that lead to the proposal of  [[formal system]]s with deep inference are all related to the [[cut-elimination theorem]].  The first calculus of deep inference was proposed by [[Kurt Schütte]],<ref>Kurt Schütte. Proof Theory. Springer-Verlag, 1977.</ref> but the idea did not generate much interest at the time.

[[Nuel Belnap]] proposed [[display logic]] in an attempt to characterise the essence of structural proof theory.  The [[calculus of structures]] was proposed in order to give a cut-free characterisation of [[noncommutative logic]]. [[Cirquent calculus]] was developed as a system of deep inference allowing to explicitly account for the possibility of subcomponent-sharing.

== Notes ==
{{Reflist}}

== Further reading ==
* Kai Brünnler, "Deep Inference and Symmetry in Classical Proofs" ([http://www.iam.unibe.ch/~kai/Papers/phd.pdf Ph.D. thesis 2004]), also published in book form by Logos Verlag ({{ISBN|978-3-8325-0448-9}}).
* [http://alessio.guglielmi.name/res/cos/index.html Deep Inference and the Calculus of Structures] Intro and reference web page about ongoing research in deep inference.

[[Category:Proof theory]]
[[Category:Inference]]


{{logic-stub}}