Editing Sequent calculus (section)

=== Reduction trees<!--'Reduction tree', 'Reduction trees', 'Inference line' and 'Inference lines' redirect here--> ===
Sequent calculus can be seen as a tool for proving formulas in [[propositional logic]], similar to the [[method of analytic tableaux]]. It gives a series of steps that allows one to reduce the problem of proving a logical formula to simpler and simpler formulas until one arrives at trivial ones.{{sfn|Kreitz|Constable|2009}}

Consider the following formula:
:<math>((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)</math>

This is written in the following form, where the proposition that needs to be proven is to the right of the [[Turnstile (symbol)|turnstile symbol]] <math>\vdash</math>:
:<math>\vdash((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)</math>

Now, instead of proving this from the axioms, it is enough to assume the premise of the [[Logical consequence|implication]] and then try to prove its conclusion.<ref name=Wadler>"Remember, the way that you [[Proof (truth)|prove]]  an [[logical consequence|implication]] is by assuming the [[hypothesis]]."—[[Philip Wadler]], [https://www.youtube.com/watch?v=OGF-TGd-CIo&list=PLWbHc_FXPo2jB6IZ887vLXsPoympL3KEy&index=11 on 2 November 2015, in his  Keynote: "Propositions as Types". Minute 14:36 /55:28 of Code Mesh video clip ]</ref> Hence one moves to the following sequent:
:<math>(p\rightarrow r)\lor (q\rightarrow r)\vdash (p\land q)\rightarrow r</math>

Again the right hand side includes an implication, whose premise can further be assumed so that only its conclusion needs to be proven:
:<math>(p\rightarrow r)\lor (q\rightarrow r), (p\land q)\vdash r</math>

Since the arguments in the left-hand side are assumed to be related by [[Logical conjunction|conjunction]], this can be replaced by the following:
:<math>(p\rightarrow r)\lor (q\rightarrow r), p, q\vdash r</math>

This is equivalent to proving the conclusion in both cases of the [[Logical disjunction|disjunction]] on the first argument on the left. Thus we may split the sequent to two, where we now have to prove each separately:
:<math>p\rightarrow r, p, q\vdash r</math>
:<math>q\rightarrow r, p, q\vdash r</math>

In the case of the first judgment, we rewrite <math>p\rightarrow r</math> as <math>\lnot p \lor r</math> and split the sequent again to get:
:<math>\lnot p, p, q \vdash r</math>
:<math>r, p, q \vdash r</math>

The second sequent is done; the first sequent can be further simplified into:
:<math>p, q \vdash p, r</math>

This process can always be continued until there are only atomic formulas in each side. 
The process can be graphically described by a [[Tree (graph theory)|rooted tree]], as depicted on the right. The root of the tree is the formula we wish to prove; the leaves consist of atomic formulas only. The tree is known as a '''reduction tree'''<!--boldface per WP:R#PLA-->.{{sfn|Kreitz|Constable|2009}}{{sfn|Tait|2010}}

The items to the left of the turnstile are understood to be connected by conjunction, and those to the right by disjunction. Therefore, when both consist only of atomic symbols, the sequent is accepted axiomatically (and always true) if and only if at least one of the symbols on the right also appears on the left.

Following are the rules by which one proceeds along the tree. Whenever one sequent is split into two, the tree vertex has two child vertices, and the tree is branched. Additionally, one may freely change the order of the arguments in each side; &Gamma; and &Delta; stand for possible additional arguments.{{sfn|Kreitz|Constable|2009}}

The usual term for the horizontal line used in Gentzen-style layouts for natural deduction is '''inference line'''<!--boldface per WP:R#PLA-->.{{sfn|von Plato|2014|page=32}}

{| class="wikitable"
|-
! Left
! Right
|-
| <math>L\land \text{rule: }\quad\cfrac{\Gamma, A \land B\vdash \Delta} {\Gamma, A, B \vdash \Delta}
 </math>
| <math>R\land  \text{rule: }\cfrac{\Gamma\vdash \Delta, A \land B} {\Gamma \vdash \Delta, A \qquad \Gamma \vdash \Delta, B}
 </math>
|-
| <math>L\lor \text{rule: }\cfrac{\Gamma, A \lor B\vdash \Delta} {\Gamma, A \vdash \Delta \qquad \Gamma, B \vdash \Delta}
 </math>
| <math>R\lor  \text{rule: }\quad\cfrac{\Gamma\vdash \Delta, A \lor B} {\Gamma \vdash \Delta, A, B}
 </math>
|-
| <math>L\rightarrow \text{rule: }\cfrac{\Gamma, A \rightarrow B\vdash \Delta} {\Gamma \vdash \Delta,A \qquad \Gamma, B \vdash \Delta}
 </math>
| <math>R\rightarrow  \text{rule: }\quad\cfrac{\Gamma\vdash \Delta, A \rightarrow B} {\Gamma, A \vdash \Delta, B}
 </math>
|-
| <math>L\lnot \text{rule: }\quad\cfrac{\Gamma, \lnot A \vdash \Delta} {\Gamma \vdash \Delta,A }
 </math>
| <math>R\lnot  \text{rule: }\quad\cfrac{\Gamma\vdash \Delta, \lnot A} {\Gamma, A \vdash \Delta}
 </math>
|-
| colspan="2" | Axiom:  <math>  \Gamma,A \vdash \Delta, A </math>
|}

Starting with any formula in propositional logic, by a series of steps, the right side of the turnstile can be processed until it includes only atomic symbols. Then, the same is done for the left side. Since every logical operator appears in one of the rules above, and is removed by the rule, the process terminates when no logical operators remain: The formula has been ''decomposed''.

Thus, the sequents in the leaves of the trees include only atomic symbols, which are either provable by the axiom or not, according to whether one of the symbols on the right also appears on the left.

It is easy to see that the steps in the tree preserve the semantic truth value of the formulas implied by them, with conjunction understood between the tree's different branches whenever there is a split. It is also obvious that an axiom is provable if and only if it is true for every assignment of truth values to the atomic symbols. Thus this system is [[soundness|sound]] and [[completeness (logic)|complete]] for classical propositional logic.