Deep inference

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,[1] 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
  1. Kurt Schütte. Proof Theory. Springer-Verlag, 1977.

Further reading
  • Kai Brünnler, "Deep Inference and Symmetry in Classical Proofs" (Ph.D. thesis 2004) , 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.


gollark: They don't need to know what potatOS is, only what a semiprime is, and it would be easy enough to just look it up.
gollark: It would be a utopia!
gollark: And then even when it was explained "you can just look up a thing to solve this, it is easy" people just go "AAAA MAFS TOO HARD" still.
gollark: But instead people just decide that anything complicated-looking is obviously impossible?
gollark: I mean, my approach to such a problem would just be to duckduckgo "factorize number" or something, and most of the programmers on the servers potatOS is tested on were fine with it. People could even have just *asked* how to do it.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.