Editing Proof theory (section)

==Structural proof theory==
{{Main|Structural proof theory}}

Structural proof theory is the subdiscipline of proof theory that studies the specifics of [[proof calculi]]. The three most well-known styles of proof calculi are:
*The [[Hilbert system|Hilbert calculi]]
*The [[natural deduction calculus|natural deduction calculi]]
*The [[sequent calculus|sequent calculi]]

Each of these can give a complete and axiomatic formalization of [[propositional logic|propositional]] or [[predicate logic]] of either the [[classical logic|classical]] or [[intuitionistic logic|intuitionistic]] flavour, almost any [[modal logic]], and many [[substructural logic]]s, such as [[relevance logic]] or [[linear logic]].  Indeed, it is unusual to find a logic that resists being represented in one of these calculi.

Proof theorists are typically interested in proof calculi that support a notion of [[analytic proof]].  The notion of analytic proof was introduced by Gentzen for the sequent calculus; there the analytic proofs are those that are [[cut-elimination theorem|cut-free]]. Much of the interest in cut-free proofs comes from the {{vanchor|subformula property}}: every formula in the end sequent of a cut-free proof is a subformula of one of the premises. This allows one to show consistency of the sequent calculus easily; if the empty sequent were derivable it would have to be a subformula of some premise, which it is not. Gentzen's midsequent theorem, the Craig interpolation theorem, and Herbrand's theorem also follow as corollaries of the cut-elimination theorem. 

Gentzen's natural deduction calculus also supports a notion of analytic proof, as shown by [[Dag Prawitz]]. The definition is slightly more complex: we say the analytic proofs are the [[Natural deduction#Consistency.2C completeness.2C and normal forms|normal forms]], which are related to the notion of normal form in term rewriting.  More exotic proof calculi such as [[Jean-Yves Girard]]'s [[proof net]]s also support a notion of analytic proof.

A particular family of analytic proofs arising in [[reductive logic]] are [[focused proof]]s which characterise a large family of goal-directed proof-search procedures. The ability to transform a proof system into a focused form is a good indication of its syntactic quality, in a manner similar to how admissibility of cut shows that a proof system is syntactically consistent.<ref>{{Citation|last1=Chaudhuri|first1=Kaustuv|title=Focused and Synthetic Nested Sequents|date=2016|pages=390–407|place=Berlin, Heidelberg|publisher=Springer Berlin Heidelberg|isbn=978-3-662-49629-9|last2=Marin|first2=Sonia|last3=Straßburger|first3=Lutz|series=Lecture Notes in Computer Science |volume=9634 |doi=10.1007/978-3-662-49630-5_23}}</ref>

Structural proof theory is connected to [[type theory]] by means of the [[Curry–Howard correspondence]], which observes a structural analogy between the process of normalisation in the natural deduction calculus and beta reduction in the [[typed lambda calculus]].  This provides the foundation for the [[intuitionistic type theory]] developed by [[Per Martin-Löf]], and is often extended to a three way correspondence, the third leg of which are the [[cartesian closed category|cartesian closed categories]].

Other research topics in structural theory include analytic tableau, which apply the central idea of analytic proof from structural proof theory to provide decision procedures and semi-decision procedures for a wide range of logics, and the proof theory of substructural logics.