Deep inference names a general idea in structural proof theory that breaks with the classical sequent calculus by generalising the notion of 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 systems with deep inference are all related to the cut-elimination theorem. The first calculus of deep inference was proposed by Kurt Schütte, 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.
Famous quotes containing the words deep and/or inference:
“The poor in bustling towns aren’t called upon, but the rich deep in the mountains have relatives visiting them from afar.”
—Chinese proverb.
“I shouldn’t want you to be surprised, or to draw any particular inference from my making speeches, or not making speeches, out there. I don’t recall any candidate for President that ever injured himself very much by not talking.”
—Calvin Coolidge (1872–1933)