Editing Natural deduction (section)

==Classical and modal logics==
{{Unreferenced section|date=May 2024}}
For simplicity, the logics presented so far have been [[intuitionistic logic|intuitionistic]]. [[Classical logic]] extends intuitionistic logic with an additional [[axiom]] or principle of [[excluded middle]]:

:For any proposition p, the proposition p ∨ ¬p is true.

This statement is not obviously either an introduction or an elimination; indeed, it involves two distinct connectives. Gentzen's original treatment of excluded middle prescribed one of the following three (equivalent) formulations, which were already present in analogous forms in the systems of [[David Hilbert|Hilbert]] and [[Arend Heyting|Heyting]]:
{| style="margin-left: 2em;"
|-
|
 ────────────── XM<sub>1</sub>
 A ∨ ¬A
| width="5%" |  ||
 ¬¬A
 ────────── XM<sub>2</sub>
 A
| width="5%" |  ||
 ──────── ''u''
 ¬A
 ⋮
 ''p''
 ────── XM<sub>3</sub><sup>''u, p''</sup>
 A
|}

(XM<sub>3</sub> is merely XM<sub>2</sub> expressed in terms of E.) This treatment of excluded middle, in addition to being objectionable from a purist's standpoint, introduces additional complications in the definition of normal forms.

A comparatively more satisfactory treatment of classical natural deduction in terms of introduction and elimination rules alone was first proposed by [[Michel Parigot|Parigot]] in 1992 in the form of a classical [[lambda calculus]] called [[Lambda-mu calculus|λμ]]. The key insight of his approach was to replace a truth-centric judgment ''A'' with a more classical notion, reminiscent of the [[sequent calculus]]: in localised form, instead of Γ ⊢ ''A'', he used Γ ⊢ Δ, with Δ a collection of propositions similar to Γ. Γ was treated as a conjunction, and Δ as a disjunction. This structure is essentially lifted directly from classical [[sequent calculus|sequent calculi]], but the innovation in λμ was to give a computational meaning to classical natural deduction proofs in terms of a [[callcc]] or a throw/catch mechanism seen in [[LISP]] and its descendants. (See also: [[first class control]].)

Another important extension was for [[modal logic|modal]] and other logics that need more than just the basic judgment of truth. These were first described, for the alethic modal logics [[S4 (modal logic)|S4]] and [[S5 (modal logic)|S5]], in a natural deduction style by [[Dag Prawitz|Prawitz]] in 1965,<ref name=prawitz1965 /> and have since accumulated a large body of related work. To give a simple example, the modal logic S4 requires one new judgment, "''A valid''", that is categorical with respect to truth:

:If "A" (is true) under no assumption that "B" (is true), then "A valid".

This categorical judgment is internalised as a unary connective ◻''A'' (read "''necessarily A''") with the following introduction and elimination rules:
{| style="margin-left: 2em;"
|-
|
 A valid
 ──────── ◻I
 ◻ A
| width="5%" |  ||
 ◻ A
 ──────── ◻E
 A
|}

Note that the premise "''A valid''" has no defining rules; instead, the categorical definition of validity is used in its place. This mode becomes clearer in the localised form when the hypotheses are explicit. We write "Ω;Γ ⊢ ''A''" where Γ contains the true hypotheses as before, and Ω contains valid hypotheses. On the right there is just a single judgment "''A''"; validity is not needed here since "Ω ⊢ ''A valid''" is by definition the same as "Ω;⋅ ⊢ ''A''". The introduction and elimination forms are then:
{| style="margin-left: 2em;"
|-
|
 Ω;⋅ ⊢ π : A
 ──────────────────── ◻I
 Ω;⋅ ⊢ '''box''' π : ◻ A
| width="5%" |  ||
 Ω;Γ ⊢ π : ◻ A
 ────────────────────── ◻E
 Ω;Γ ⊢ '''unbox''' π : A
|}

The modal hypotheses have their own version of the hypothesis rule and substitution theorem.
{| style="margin-left: 2em;"
|-
|
 ─────────────────────────────── valid-hyp
 Ω, u: (A valid) ; Γ ⊢ u : A
|}

=== Modal substitution theorem ===
; {{Unreferenced section|date=May 2024}}: ''If'' Ω;⋅ ⊢ π<sub>1</sub> : ''A'' ''and'' Ω, ''u'': (''A valid'') ; Γ ⊢ π<sub>2</sub> : ''C'', ''then'' Ω;Γ ⊢ [π<sub>1</sub>/''u''] π<sub>2</sub> : ''C''.

This framework of separating judgments into distinct collections of hypotheses, also known as ''multi-zoned'' or ''polyadic'' contexts, is very powerful and extensible; it has been applied for many different modal logics, and also for [[linear logic|linear]] and other [[substructural logic]]s, to give a few examples. However, relatively few systems of modal logic can be formalised directly in natural deduction. To give proof-theoretic characterisations of these systems, extensions such as labelling or systems of deep inference.

The addition of labels to formulae permits much finer control of the conditions under which rules apply, allowing the more flexible techniques of [[analytic tableau]]x to be applied, as has been done in the case of [[labelled deduction]]. Labels also allow the naming of worlds in Kripke semantics; {{harvtxt|Simpson|1994}} presents an influential technique for converting frame conditions of modal logics in Kripke semantics into inference rules in a natural deduction formalisation of [[hybrid logic]]. {{harvtxt|Stouppa|2004}} surveys the application of many proof theories, such as Avron and Pottinger's [[hypersequent]]s and Belnap's [[display logic]] to such modal logics as S5 and B.