natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
basic constructions:
strong axioms
The framework of natural deduction describes a particular class of deductive systems which formalize “natural” deductive reasoning or reasoning from assumptions. It is used particularly to describe the syntax of formal logic and type theory.
The phrase “natural deduction” is not always used to mean the same thing. Some people use it semi-informally to refer to a “sort of reasoning” that involves making assumptions, perhaps formalized using hypothetical judgments. Other people take it to refer specifically to deductive systems which are presented using introduction and elimination rules, which is the meaning we adopt on this page. There is significant overlap between the two meanings, but they are not identical.
A system of natural deduction is a deductive system containing a class of judgments generated by some “constructor” operations, and for which each constructor comes with two relevant classes of rules:
Introduction rules, which allow us to conclude a judgment built using the constructor from simpler judgments; and
Elimination rules, which allow us to conclude some other judgment by using a judgment involving the constructor.
For instance, in a system of propositional logic whose judgments are the truth of propositions, one such constructor might be the “conjunction” connective $\wedge$. The introduction rule for $\wedge$ would be
while its elimination rules might be
The introduction and elimination rules must fit together in an appropriate way, sometimes referred to as “harmony”.
Similarly, in a system of type theory, the relevant judgments are typing judgments of the form $a:A$, meaning that the term $a$ belongs to the type $A$. In this case, an analogous constructor might be the cartesian product type, whose rules are analogous, but keeping track of the specific terms involved (see propositions as types):
and
In natural deduction systems for type theory, there are usually two other classes of rules:
Formation rules, which declare on which basis a new type can be introduced; and
Computation rules or conversion rules, which constrain the result of combining term introduction with term elimination.
These two rules refer to different classes of judgments than the introduction and elimination rules: judgments that a certain thing is a type for the formation rules, and judgments that one term reduces to, or converts with, another, for the computation rules.
For instance, the cartesian product type would come with a formation rule
and computation rules such as beta-reduction
(and possibly eta-conversion).
Technically, the propositional logic system could also come with a formation rule involving a judgment “is a proposition”:
But it would not have a computation rule, as there are no terms inhabiting its propositions. (It could, however, be embedded into a type theory via propositions as types, where there would be terms inhabiting its propositions regarded as types).
More generally, natural deduction with computation rules gives a formulation of computation. See computational trinitarianism for discussion of this unification of concepts.
On the other hand, in type theories that have a type of types, there may be no need for a separate judgment “$A\;type$”, as it can be replaced by a typing judgment “$A:Type$” that $A$ belongs to a type of types.
Natural deduction also generally involves hypothetical judgments or reasoning from assumptions. For instance, the introduction rule for implication in a system of propositional logic says that if, assuming “$A$”, we can derive “$B$”, then we can derive “$A\Rightarrow B$”. This is sometimes written as
(We now follow the common practice of writing the judgment “$A\;true$” as simply “$A$”.) Here the $\vdots$ indicate an arbitrary derivation tree, while the brackets around $A$ indicate that this assumption has been “discharged” and is no longer an assumption in the conclusion $A\Rightarrow B$. To be precise, we should annotate each bracket somehow to indicate which rule discharged that assumption.
Another way to indicate hypothetical reasoning (which also allows it to fit once again within the general notion of deductive system) is to indicate in each judgment the hypotheses on which it depends. Thus, we might write “$A\vdash B$” to mean a hypothetical judgment of $B$ assuming $A$. With this notation, the introduction rule for $\Rightarrow$ can be written as:
The rule (1), where $\vdots$ indicates an arbitrary derivation, can then be written as
Here we have prefixed the entire derivation $\vdots$ in (1) by “$A\vdash$” to indicate that it is all performed with $A$ as an assumption, and the discharge of that assumption is indicated by removing this prefix from the final conclusion. We also begin the deduction with the axiom $A\vdash A$ (the identity rule?).
To be fully precise, we should now allow all rules to take place under arbitrary additional hypotheses; thus the introduction rule of $\Rightarrow$ should really be
where $\Gamma$ denotes an arbitrary list of hypothesis truth judgments. However, often this unchanged ambient context is unstated, but implicitly assumed to be present.
Hypothetical judgments of this sort are very similar to the sequents which appear in sequent calculus, and are (as is evident) written with very similar notation. However, the rules of natural deduction are different from the rules of sequent calculus, as are its formal properties.
This treatment of hypothetical judgments applies also to type theories, where the individual judgments are typing judgments. In this case, the assumed judgments on the left of the $\vdash$ are generally restricted to be of the form $x:A$ with $x$ a variable (rather than an arbitrary term), and these assumed judgments are referred to as the context. When the judgment on the right of the $\vdash$ may involve variables that occur to its left, one speaks of generic judgments rather than “hypothetical” ones. Thus, a generic judgment is of the form
to be read as
In a context where we have a term $x$ of a type $A$, there is a term $b(x)$ of type $B$.
Thus, for instance, the introduction rule for the function type is
In natural deduction for dependent type theory, we can also have type judgments with hypotheses, such as
to be read as
For each $x$ in $A$ there is a type $B(x)$. Or: $B$ is a type in context $A$, a type dependent on $A$.
In a type theory with a type of types, this judgment could be written as $(x:A)\;\vdash\;(B(x):Type)$.
So far, we have been considering hypothetical judgments such as $A\vdash B$ and generic judgments such as $(x:A)\vdash (b(x):B)$ to be “atomic” judgments in a particular deductive system. In particular, the turnstile symbol $\vdash$ has been simply another symbol that we use to build judgments according to a particular syntax, analogous to the colon $:$. As remarked at deductive system, this usage of $\vdash$ is a priori completely unrelated to its use to indicate provability of theorems in a particular deductive system (such as a system of natural deduction), and therefore perhaps ought to be denoted by a different symbol.
However, it is also possible to incorporate some “knowledge” about the meaning of hypothetical and generic judgments into the deductive system, and thereby bring the two meanings of $\vdash$ back into alignment. See logical framework for a development of this idea.
The four classes of rules of natural deduction are close to being specifications of universal constructions in category theory. In categorical semantics one considers categories which are such that their objects are regarded as types and their generalized elements as terms, then the rules of natural deductions describe the possible construction of morphisms in that category.
(…)
(…)
The original source (which treated h-propositions in propositional logic and untyped predicate logic, both classical and intuitionistic) is
An introductory lecture using dependent type theory in intuitionistic logic is
A formalization of the general logical framework of natural deduction is discussed in section 3 of
A good account is at
The standard rules for type-formation, term introduction/elimination and computation in dependent type theory are listed for instance in part I of