Editing Natural deduction (section)

===Example: Dependent Type Theory===
{{Unreferenced section|date=May 2024}}
Like logic, type theory has many extensions and variants, including first-order and higher-order versions. One branch, known as [[dependent type theory]], is used in a number of [[computer-assisted proof]] systems.  Dependent type theory allows quantifiers to range over programs themselves. These quantified types are written as Π and Σ instead of ∀ and ∃, and have the following formation rules:
{| style="margin-left: 2em;"
|-
|
 Γ ⊢ A type    Γ, x:A ⊢ B type
 ───────────────────────────── Π-F
 Γ ⊢ Πx:A. B type
| width="10%" |  || 
 Γ ⊢ A type  Γ, x:A ⊢ B type
 ──────────────────────────── Σ-F
 Γ ⊢ Σx:A. B type
|}
These types are generalisations of the arrow and product types, respectively, as witnessed by their introduction and elimination rules.
{| style="margin-left: 2em;"
|-
|
 Γ, x:A ⊢ π : B
 ──────────────────── ΠI
 Γ ⊢ λx. π : Πx:A. B
| width="10%" |  || 
 Γ ⊢ π<sub>1</sub> : Πx:A. B   Γ ⊢ π<sub>2</sub> : A
 ───────────────────────────── ΠE
 Γ ⊢ π<sub>1</sub> π<sub>2</sub> : [π<sub>2</sub>/x] B
|}
{| style="margin-left: 2em;"
|-
|
 Γ ⊢ π<sub>1</sub> : A    Γ, x:A ⊢ π<sub>2</sub> : B
 ───────────────────────────── ΣI
 Γ ⊢ (π<sub>1</sub>, π<sub>2</sub>) : Σx:A. B
| width="10%" |  || 
 Γ ⊢ π : Σx:A. B
 ──────────────── ΣE<sub>1</sub>
 Γ ⊢ '''fst''' π : A
|}
{| style="margin-left: 2em;"
|-
|
 Γ ⊢ π : Σx:A. B
 ──────────────────────── ΣE<sub>2</sub>
 Γ ⊢ '''snd''' π : ['''fst''' π/x] B
|}
Dependent type theory in full generality is very powerful: it is able to express almost any conceivable property of programs directly in the types of the program. This generality comes at a steep price &mdash; either typechecking is undecidable ([[extensional type theory]]), or extensional reasoning is more difficult ([[intensional type theory]]). For this reason, some dependent type theories do not allow quantification over arbitrary programs, but rather restrict to programs of a given decidable ''index domain'', for example integers, strings, or linear programs.

Since dependent type theories allow types to depend on programs, a natural question to ask is whether it is possible for programs to depend on types, or any other combination. There are many kinds of answers to such questions. A popular approach in type theory is to allow programs to be quantified over types, also known as ''[[parametric polymorphism]]''; of this there are two main kinds: if types and programs are kept separate, then one obtains a somewhat more well-behaved system called ''[[predicative polymorphism]]''; if the distinction between program and type is blurred, one obtains the type-theoretic analogue of higher-order logic, also known as ''[[impredicative polymorphism]]''. Various combinations of dependency and polymorphism have been considered in the literature, the most famous being the [[lambda cube]] of [[Henk Barendregt]].

The intersection of logic and type theory is a vast and active research area. New logics are usually formalised in a general type theoretic setting, known as a [[logical framework]]. Popular modern logical frameworks such as the [[calculus of constructions]] and [[LF (logical framework)|LF]] are based on higher-order dependent type theory, with various trade-offs in terms of decidability and expressive power. These logical frameworks are themselves always specified as natural deduction systems, which is a testament to the versatility of the natural deduction approach.