Editing Natural deduction (section)

==Comparison with sequent calculus==
{{Unreferenced section|date=May 2024}}
{{Main|Sequent calculus}}

The sequent calculus is the chief alternative to natural deduction as a foundation of [[mathematical logic]]. In natural deduction the flow of information is bi-directional: elimination rules flow information downwards by deconstruction, and introduction rules flow information upwards by assembly. Thus, a natural deduction proof does not have a purely bottom-up or top-down reading, making it unsuitable for automation in proof search. To address this fact, [[Gerhard Gentzen|Gentzen]] in 1935 proposed his [[sequent calculus]], though he initially intended it as a technical device for clarifying the consistency of [[predicate logic]]. [[Stephen Cole Kleene|Kleene]], in his seminal 1952 book ''Introduction to Metamathematics'', gave the first formulation of the sequent calculus in the modern style.<ref>{{harvnb|Kleene|2009|pp=440–516}}. See also {{harvnb|Kleene|1980}}.</ref>

In the sequent calculus all inference rules have a purely bottom-up reading. Inference rules can apply to elements on both sides of the [[Turnstile (symbol)|turnstile]]. (To differentiate from natural deduction, this article uses a double arrow ⇒ instead of the right tack ⊢ for sequents.) The introduction rules of natural deduction are viewed as ''right rules'' in the sequent calculus, and are structurally very similar. The elimination rules on the other hand turn into ''left rules'' in the sequent calculus. To give an example, consider disjunction; the right rules are familiar:
{| style="margin-left: 2em;"
|-
|
 Γ ⇒ A
 ───────── ∨R<sub>1</sub>
 Γ ⇒ A ∨ B
| with="10%" |  || 
 Γ ⇒ B
 ───────── ∨R<sub>2</sub>
 Γ ⇒ A ∨ B
|}
On the left:
{| style="margin-left: 2em;"
|-
|
 Γ, u:A ⇒ C       Γ, v:B ⇒ C
 ─────────────────────────── ∨L
 Γ, w: (A ∨ B) ⇒ C
|}
Recall the ∨E rule of natural deduction in localised form:
{| style="margin-left: 2em;"
|-
|
 Γ ⊢ A ∨ B    Γ, u:A ⊢ C    Γ, v:B ⊢ C
 ─────────────────────────────────────── ∨E
 Γ ⊢ C
|}
The proposition ''A ∨ B'', which is the succedent of a premise in ∨E, turns into a hypothesis of the conclusion in the left rule ∨L. Thus, left rules can be seen as a sort of inverted elimination rule. This observation can be illustrated as follows:
{| align="center"
|-
! natural deduction
|
! sequent calculus
|-
|<pre>
 ────── hyp
 |
 | elim. rules
 |
 ↓
 ────────────────────── ↑↓ meet
 ↑
 |
 | intro. rules
 |
 conclusion</pre>
| width="20%" align="center" | ⇒ ||<pre>
 ─────────────────────────── init
 ↑            ↑
 |            |
 | left rules | right rules
 |            |
 conclusion</pre>
|}
In the sequent calculus, the left and right rules are performed in lock-step until one reaches the ''initial sequent'', which corresponds to the meeting point of elimination and introduction rules in natural deduction. These initial rules are superficially similar to the hypothesis rule of natural deduction, but in the sequent calculus they describe a ''transposition'' or a ''handshake'' of a left and a right proposition:
{| style="margin-left: 2em;"
|-
|
 ────────── init
 Γ, u:A ⇒ A
|}
The correspondence between the sequent calculus and natural deduction is a pair of soundness and completeness theorems, which are both provable by means of an inductive argument.

; Soundness of ⇒ wrt. ⊢ : ''If'' Γ ⇒ ''A'', ''then'' Γ ⊢ ''A''.
; Completeness of ⇒ wrt. ⊢ : ''If'' Γ ⊢ ''A'', ''then'' Γ ⇒ ''A''.

It is clear by these theorems that the sequent calculus does not change the notion of truth, because the same collection of propositions remain true. Thus, one can use the same proof objects as before in sequent calculus derivations. As an example, consider the conjunctions. The right rule is virtually identical to the introduction rule
{| style="margin-left: 2em;"
|-
! sequent calculus
|
! natural deduction
|-
|
 Γ ⇒ π<sub>1</sub> : A     Γ ⇒ π<sub>2</sub> : B
 ─────────────────────────── ∧R
 Γ ⇒ (π<sub>1</sub>, π<sub>2</sub>) : A ∧ B
| width="20%" |  || 
 Γ ⊢ π<sub>1</sub> : A      Γ ⊢ π<sub>2</sub> : B
 ───────────────────────── ∧I
 Γ ⊢ (π<sub>1</sub>, π<sub>2</sub>) : A ∧ B
|}
The left rule, however, performs some additional substitutions that are not performed in the corresponding elimination rules.
{| style="margin-left: 2em;"
|-
! sequent calculus
|
! natural deduction
|-
|
 Γ, u:A ⇒ π : C
 ──────────────────────────────── ∧L<sub>1</sub>
 Γ, v: (A ∧ B) ⇒ ['''fst''' v/u] π : C
| width="20%" |  || 
 Γ ⊢ π : A ∧ B
 ───────────── ∧E<sub>1</sub>
 Γ ⊢ '''fst''' π : A
|-
|
 Γ, u:B ⇒ π : C
 ──────────────────────────────── ∧L<sub>2</sub>
 Γ, v: (A ∧ B) ⇒ ['''snd''' v/u] π : C
| width="20%" |  || 
 Γ ⊢ π : A ∧ B
 ───────────── ∧E<sub>2</sub>
 Γ ⊢ '''snd''' π : B
|}

The kinds of proofs generated in the sequent calculus are therefore rather different from those of natural deduction. The sequent calculus produces proofs in what is known as the ''β-normal η-long'' form, which corresponds to a canonical representation of the normal form of the natural deduction proof. If one attempts to describe these proofs using natural deduction itself, one obtains what is called the ''intercalation calculus'' (first described by John Byrnes), which can be used to formally define the notion of a ''normal form'' for natural deduction.

The substitution theorem of natural deduction takes the form of a [[structural rule]] or structural theorem known as ''cut'' in the sequent calculus.

=== Cut (substitution) ===
{{Unreferenced section|date=May 2024}}
: ''If'' Γ ⇒ π<sub>1</sub> : ''A'' ''and'' Γ, ''u'':''A'' ⇒ π<sub>2</sub> : ''C'', ''then'' Γ ⇒ [π<sub>1</sub>/u] π<sub>2</sub> : ''C''.

In most well behaved logics, cut is unnecessary as an inference rule, though it remains provable as a [[meta-theorem]]; the superfluousness of the cut rule is usually presented as a computational process, known as ''cut elimination''. This has an interesting application for natural deduction; usually it is extremely tedious to prove certain properties directly in natural deduction because of an unbounded number of cases. For example, consider showing that a given proposition is ''not'' provable in natural deduction. A simple inductive argument fails because of rules like ∨E or E which can introduce arbitrary propositions. However, we know that the sequent calculus is complete with respect to natural deduction, so it is enough to show this unprovability in the sequent calculus. Now, if cut is not available as an inference rule, then all sequent rules either introduce a connective on the right or the left, so the depth of a sequent derivation is fully bounded by the connectives in the final conclusion. Thus, showing unprovability is much easier, because there are only a finite number of cases to consider, and each case is composed entirely of sub-propositions of the conclusion. A simple instance of this is the ''global consistency'' theorem: "⋅ ⊢ ⊥" is not provable. In the sequent calculus version, this is manifestly true because there is no rule that can have "⋅ ⇒ ⊥" as a conclusion! Proof theorists often prefer to work on cut-free sequent calculus formulations because of such properties.