Deep inference
Encyclopedia
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 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
, 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
.
Structural proof theory
In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof.-Analytic proof:...
that breaks with the classical sequent calculus
Sequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
by generalising the notion of structure
Abstract structure
An abstract structure in mathematics is a formal object that is defined by a set of laws, properties, and relationships in a way that is logically if not always historically independent of the structure of contingent experiences, for example, those involving physical objects...
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
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
s with deep inference are all related to the cut-elimination theorem
Cut-elimination theorem
The cut-elimination theorem is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen 1934 in his landmark paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively...
. The first calculus of deep inference was proposed by Kurt Schütte
Kurt Schütte
Kurt Schütte was a German mathematician who worked on proof theory and ordinal analysis. The Feferman-Schütte ordinal, which he showed to be the precise ordinal bound for predicativity, is named after him.-References:...
, but the idea did not generate much interest at the time.
Nuel Belnap
Nuel Belnap
Nuel D. Belnap, Jr. is an American logician and philosopher who has made many important contributions to the philosophy of logic, temporal logic, and structural proof theory. He has taught at the University of Pittsburgh since 1961; before that he was at Yale University. His best known work is...
proposed display logic in an attempt to characterise the essence of structural proof theory. The calculus of structures
Calculus of structures
The calculus of structures is a proof calculus with deep inference for studying the structural proof theory of noncommutative logic. The calculus has since been applied to study linear logic, classical logic, modal logic, and process calculi, and many benefits are claimed to follow in these...
was proposed in order to give a cut-free characterisation of noncommutative logic
Noncommutative logic
Noncommutative logic is an extension of linear logic which combines the commutative connectives of linear logic with the noncommutative multiplicative connectives of the Lambek calculus...
.
Further reading
- Kai Brünnler, "Deep Inference and Symmetry in Classical Proofs" (Ph.D. thesis 2004) http://www.iam.unibe.ch/~kai/Papers/phd.pdf, also published in book form by Logos Verlag (ISBN 978-3-8325-0448-9).
- Deep Inference and the Calculus of Structures Intro and reference web page about ongoing research in deep inference.