You are here
Homederivations in natural deduction
Primary tabs
derivations in natural deduction
Derivations, or deductions, for natural deduction systems, unlike the axiom systems, which are finite sequences of wellformed formulas (wff’s) in a logic, are finite tress of wff’s. More precisely, they are rooted tress whose vertices are labeled by wff’s of the logic. For example,
$\pstree[treemode=U,radius=3pt,levelsep=7ex]{\Tc{3pt}~{}[tnpos=b,tndepth=0pt,% radius=4pt]{A\to A}}{\pstree{\TC~{}[tnpos=r]{A}}{\pstree{\TC~{}[tnpos=r]{A% \land A}}{\TC~{}[tnpos=l]{A}\TC~{}[tnpos=r]{A}}}}$ 
is a labeled rooted tree, whose root is labeled by the wff $A\to A$. In natural deduction, the trees are presented a little bit differently, replacing each edge with a horizontal bar separating the neighboring vertices. Thus, the tree above looks like \prooftree \AxiomC$A$ \AxiomC$A$ \BinaryInfC$A\land A$ \UnaryInfC$A$ \UnaryInfC$A\to A$
Derivations are defined recursively: from atomic formulas as singlevertex trees via rules of inference of the system. To see how this is done exactly, recall that a rule of inference generally takes the following form:
$\infer[R]{Y}{X_{1}\quad\cdots\quad X_{i}\quad\cdots\quad\infer*{X_{j}}{[A_{j}]% }\quad\cdots\quad X_{n}}$ 
where $R$ is the name of the rule, and the $X_{k}$’s, $A_{k}$’s, and $Y$ are wff’s of the logic. Each $X_{k}$ is a premise, and $Y$ is the conclusion. Some of the premises (like $X_{j}$ above) have optional assumptions ($A_{j}$) which can be cancelled or discharged once the conclusion is reached. Just exactly what “cancelled” or “discharged” means will be clear shortly.
Now we are ready for the formal definition of derivations.
Definition. A labeled rooted tree over a natural deduction system is a rooted tree whose labels are of the form $A$ or $[A]$, where $A$ is a wff of the logical system.
Definition. The set $\mathbb{D}$ of derivations of a natural deduction system the smallest set of labeled rooted trees over the wff’s of system, such that
1. for each propositional variable $p$, a onevertex tree with label $p$ is in $\mathbb{D}$
2. for every inference rule $R$ where

$X_{1},\ldots,X_{n}$ are premises

$Y$ is the conclusion

a subset $\mathcal{X}$ (may be empty) of the premises where each $X\in\mathcal{X}$ has an optional assumption $A_{X}$ that can be discharged when conclusion $Y$ is reached
if $T_{1},\ldots,T_{n}$ are in $\mathdd{D}$ where each $X_{i}$ is the label of the root of $T_{i}$, then the rooted tree $T$, obtained by
(a) transforming each of the trees $T$ whose root has label $X\in\mathcal{X}$ to a tree such that some (or none) of the leaves in $T$ with label $A_{X}$ are converted to leaves with label $[A_{X}]$,
(b) then combining the resulting trees, as well as the rest of the other trees by joining their roots to a new vertex as the root of $T$, with label is $Y$
is also in $\mathbb{D}$. Graphically, $T$ can be represented \prooftree \alwaysNoLine\AxiomC$T_{1}$ \UnaryInfC$X_{1}$ \AxiomC$\cdots$ \AxiomC[$A_{{X_{n}}}$] \UnaryInfC$T_{n}$ \UnaryInfC$X_{n}$ \alwaysSingleLine\TrinaryInfC$Y$

For example, using the following rule of inference in classical propositional logic, called $\to I$
$\infer[\to I]{A\to B}{\infer*{B}{[A]}}$ 
we have the following derivations
$\infer{p\to q}{q}\qquad\qquad\infer{q\to(p\to q)}{\infer{p\to q}{[q]}}$ 
The first one is a derivation because $q$ is a propositional variable by $(a)$, and since the rule does not require the presence of an assumption (it is optional), the whole tree is a derivation by $(b)$. As a result, by $(b)$ once more, the second one is also a derivation, where the label $q$ of the leaf (top vertex) has been changed to $[q]$.
From now on, if no confusion arises, the vertices of a derivation are identified with their labels.
Definition. Given a derivation $T$ in a natural deduction logical system, the assumptions of $T$ are leaves of the form $A$, and discharged assumptions of $T$ if they are of the form $[A]$. The conclusion of $T$ is the root of $T$. If $\Sigma$ is a set of wff’s and $A$ a wff, we write
$\Sigma\vdash A$ 
if there is a derivation $T$ whose assumptions are elements of $\Sigma$, and whose conclusion is $A$. We say that $A$ is derivable from $\Sigma$. The symbol $\vdash$ is the derivability relation between sets of wff’s and wff’s. We say that $A$ is a theorem (of the logical system) if it is derivable from the empty set, and write
$\vdash A.$ 
In other words, $A$ is a theorem if there is a derivation of $A$ whose assumptions are all discharged. For example, from the two derivations above, we see that $q\vdash p\to q$ and $\vdash q\to(p\to q)$.
Mathematics Subject Classification
03F03 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections