# deduction

There are several ways to formally define what a deduction is, given a deductive system. We will explore some of them here.

## Deduction as a Sequence

Given a deductive system, a deduction from a set $\Delta$ of (well-formed) formulas   can be thought of as a finite sequence  of wff’s

 $A_{1},A_{2},\cdots,A_{n}$

such that $A_{i}$ is either an axiom, an element of $\Delta$, or as the result of an application of an inference rule $R$ to earlier wff’s $A_{i_{1}},\ldots,A_{i_{k}}$, where $i_{1},\ldots,i_{k}. If $A_{i}$ is an element of $\Delta$, we call $A_{i}$ an assumption or a hypothesis  . This way of presenting a deduction is said to be linear.

Deductions presented this way are also called deduction sequences or proof sequences. Deductions in Hilbert-style axiom systems are presented this way.

## Deduction as a Tree

Alternatively, a deduction can be thought of as a labeled rooted tree  . The nodes are labeled by formulas, and for each node with label, say $Y$, its immediate predecessors (children) are nodes whose labels are, say $X_{1},\ldots,X_{n}$ which are premises of some inference rule $R$. Deductions presented this way are also called deduction trees or proof trees. In a deduction tree, the labels of the leaves are either the axioms, or assumptions (from some set $\Delta$), and the label of the root of the tree is the conclusion of the deduction. Below is an example of a deduction tree:

 $\ignorespaces.25.25\leavevmode\hbox{\vrule height 0.0pt depth 0.0pt width 0.0% pt\kern 84.598679pt\hbox{\vrule height 6.999893pt depth 1.999969pt width 0.0pt% \hbox{\displaystyle{\hbox to 0.0pt{\kern-3.749943pt\hbox{\leavevmode\lower 2.% 499962pt\hbox{\leavevmode\immediate\special{PST: \pst@dict \ifPst@saveNodeCoors\ifx\relax\pst@number{\ht\pst@hbox}\pst@number{\dp% \pst@hbox}\pst@number{\wd\pst@hbox}\pst@number\pst@dima\pst@number\pst@dimb% \relax 0 0 \else gsave \pst@dict STV CP T end \pst@number{\ht\pst@hbox}% \pst@number{\dp\pst@hbox}\pst@number{\wd\pst@hbox}\pst@number\pst@dima% \pst@number\pst@dimb \tx@UserCoor grestore \fi\if\psk@NodeCoorPrefix /N-\pssucc.y exch def /N-\pssucc.x exch def \else/\psk@NodeCoorPrefix\pssucc y exch def /\psk@NodeCoorPrefix\pssucc x exch def \fi\fi\pst@nodedict{\pst@number{\ht\pst@hbox}\pst@number{\dp\pst@hbox}% \pst@number{\wd\pst@hbox}\pst@number\pst@dima\pst@number\pst@dimb} \ifx\psk@name\relax false \else\psk@name true \fi\pst@thenode 16 {\tx@InitRnode} \ifPst@showNode exch dup /NodeType ED exch NodeType 10 eq { 5 copy cvlit aload pop 20 string cvs (; ) 6 2 roll 20 string cvs (; ) 7 2 roll 20 string cvs (; ) 8 2% roll 20 string cvs (; ) 9 2 roll cvlit dup length 2 eq { aload pop exch 20 string cvs (; ) 11 2 roll 20 string cvs (, ) 12 2 roll (\string\n) 13 array astore concatstringarray } { 255 string cvs (; ) 10 2 roll (\string\n) 11 array astore concatstringarray } ifelse NodeFile exch writestring } if NodeType 14 eq { 5 copy /@@temp ED @@temp 4 -1 roll cvlit pop ( OvalNodePos ) (; ) 5 2 roll 20 string cvs (; ) 6 2 roll 20 string cvs (; ) 7 2 roll 20 string cvs (; ) 8 2% roll Y 20 string cvs (; ) 10 2 roll X 20 string cvs (, ) 12 2 roll (\string\n) 13 array astore concatstringarray tx@NodeDict begin NodeFile exch writestring end } if \fi\tx@NewNode end end}\hbox{\displaystyle{Z}}}}\hss}\ignorespaces}}\lower 56.905512pt\hbox t% o 0.0pt{\hss\hbox{\displaystyle{.75.75\vrule height 0.0pt depth 0.0pt width 0% .0pt\hbox{\vrule height 6.999893pt depth 1.999969pt width 0.0pt\hbox{% \displaystyle{\hbox to 0.0pt{\kern-3.749943pt\hbox{\leavevmode\lower 2.499962% pt\hbox{\leavevmode\immediate\special{PST: \pst@dict \ifPst@saveNodeCoors\ifx\relax\pst@number{\ht\pst@hbox}\pst@number{\dp% \pst@hbox}\pst@number{\wd\pst@hbox}\pst@number\pst@dima\pst@number\pst@dimb% \relax 0 0 \else gsave \pst@dict STV CP T end \pst@number{\ht\pst@hbox}% \pst@number{\dp\pst@hbox}\pst@number{\wd\pst@hbox}\pst@number\pst@dima% \pst@number\pst@dimb \tx@UserCoor grestore \fi\if\psk@NodeCoorPrefix /N-\pssucc.y exch def /N-\pssucc.x exch def \else/\psk@NodeCoorPrefix\pssucc y exch def /\psk@NodeCoorPrefix\pssucc x exch def \fi\fi\pst@nodedict{\pst@number{\ht\pst@hbox}\pst@number{\dp\pst@hbox}% \pst@number{\wd\pst@hbox}\pst@number\pst@dima\pst@number\pst@dimb} \ifx\psk@name\relax false \else\psk@name true \fi\pst@thenode 16 {\tx@InitRnode} \ifPst@showNode exch dup /NodeType ED exch NodeType 10 eq { 5 copy cvlit aload pop 20 string cvs (; ) 6 2 roll 20 string cvs (; ) 7 2 roll 20 string cvs (; ) 8 2% roll 20 string cvs (; ) 9 2 roll cvlit dup length 2 eq { aload pop exch 20 string cvs (; ) 11 2 roll 20 string cvs (, ) 12 2 roll (\string\n) 13 array astore concatstringarray } { 255 string cvs (; ) 10 2 roll (\string\n) 11 array astore concatstringarray } ifelse NodeFile exch writestring } if NodeType 14 eq { 5 copy /@@temp ED @@temp 4 -1 roll cvlit pop ( OvalNodePos ) (; ) 5 2 roll 20 string cvs (; ) 6 2 roll 20 string cvs (; ) 7 2 roll 20 string cvs (; ) 8 2% roll Y 20 string cvs (; ) 10 2 roll X 20 string cvs (, ) 12 2 roll (\string\n) 13 array astore concatstringarray tx@NodeDict begin NodeFile exch writestring end } if \fi\tx@NewNode end end}\hbox{\displaystyle{Y}}}}\hss}\leavevmode\immediate\special{PST: % \pst@dict gsave \tx@STV newpath \pst@code\space grestore end}\ignorespaces% \ignorespaces\ignorespaces}}\lower 56.905512pt\hbox to 0.0pt{\hss\hbox{% \displaystyle{\vrule height 6.999893pt depth 3.079953pt width 0.0pt\hbox to 0.% 0pt{\kern-5.849911pt\hbox{\leavevmode\lower 1.95997pt\hbox{\leavevmode% \immediate\special{PST: \pst@dict \ifPst@saveNodeCoors\ifx\relax\pst@number{\ht\pst@hbox}\pst@number{\dp% \pst@hbox}\pst@number{\wd\pst@hbox}\pst@number\pst@dima\pst@number\pst@dimb% \relax 0 0 \else gsave \pst@dict STV CP T end \pst@number{\ht\pst@hbox}% \pst@number{\dp\pst@hbox}\pst@number{\wd\pst@hbox}\pst@number\pst@dima% \pst@number\pst@dimb \tx@UserCoor grestore \fi\if\psk@NodeCoorPrefix /N-\pssucc.y exch def /N-\pssucc.x exch def \else/\psk@NodeCoorPrefix\pssucc y exch def /\psk@NodeCoorPrefix\pssucc x exch def \fi\fi\pst@nodedict{\pst@number{\ht\pst@hbox}\pst@number{\dp\pst@hbox}% \pst@number{\wd\pst@hbox}\pst@number\pst@dima\pst@number\pst@dimb} \ifx\psk@name\relax false \else\psk@name true \fi\pst@thenode 16 {\tx@InitRnode} \ifPst@showNode exch dup /NodeType ED exch NodeType 10 eq { 5 copy cvlit aload pop 20 string cvs (; ) 6 2 roll 20 string cvs (; ) 7 2 roll 20 string cvs (; ) 8 2% roll 20 string cvs (; ) 9 2 roll cvlit dup length 2 eq { aload pop exch 20 string cvs (; ) 11 2 roll 20 string cvs (, ) 12 2 roll (\string\n) 13 array astore concatstringarray } { 255 string cvs (; ) 10 2 roll (\string\n) 11 array astore concatstringarray } ifelse NodeFile exch writestring } if NodeType 14 eq { 5 copy /@@temp ED @@temp 4 -1 roll cvlit pop ( OvalNodePos ) (; ) 5 2 roll 20 string cvs (; ) 6 2 roll 20 string cvs (; ) 7 2 roll 20 string cvs (; ) 8 2% roll Y 20 string cvs (; ) 10 2 roll X 20 string cvs (, ) 12 2 roll (\string\n) 13 array astore concatstringarray tx@NodeDict begin NodeFile exch writestring end } if \fi\tx@NewNode end end}\hbox{\displaystyle{X_{1}}}}}\hss}\vrule height 6.999893pt depth 3.0799% 53pt width 0.0pt.75.75.85826772\kern 33.039352pt\hbox to 0.0pt{\kern-5.849911% pt\hbox{\leavevmode\lower 1.95997pt\hbox{\leavevmode\immediate\special{PST: % \pst@dict \ifPst@saveNodeCoors\ifx\relax\pst@number{\ht\pst@hbox}\pst@number{\dp% \pst@hbox}\pst@number{\wd\pst@hbox}\pst@number\pst@dima\pst@number\pst@dimb% \relax 0 0 \else gsave \pst@dict STV CP T end \pst@number{\ht\pst@hbox}% \pst@number{\dp\pst@hbox}\pst@number{\wd\pst@hbox}\pst@number\pst@dima% \pst@number\pst@dimb \tx@UserCoor grestore \fi\if\psk@NodeCoorPrefix /N-\pssucc.y exch def /N-\pssucc.x exch def \else/\psk@NodeCoorPrefix\pssucc y exch def /\psk@NodeCoorPrefix\pssucc x exch def \fi\fi\pst@nodedict{\pst@number{\ht\pst@hbox}\pst@number{\dp\pst@hbox}% \pst@number{\wd\pst@hbox}\pst@number\pst@dima\pst@number\pst@dimb} \ifx\psk@name\relax false \else\psk@name true \fi\pst@thenode 16 {\tx@InitRnode} \ifPst@showNode exch dup /NodeType ED exch NodeType 10 eq { 5 copy cvlit aload pop 20 string cvs (; ) 6 2 roll 20 string cvs (; ) 7 2 roll 20 string cvs (; ) 8 2% roll 20 string cvs (; ) 9 2 roll cvlit dup length 2 eq { aload pop exch 20 string cvs (; ) 11 2 roll 20 string cvs (, ) 12 2 roll (\string\n) 13 array astore concatstringarray } { 255 string cvs (; ) 10 2 roll (\string\n) 11 array astore concatstringarray } ifelse NodeFile exch writestring } if NodeType 14 eq { 5 copy /@@temp ED @@temp 4 -1 roll cvlit pop ( OvalNodePos ) (; ) 5 2 roll 20 string cvs (; ) 6 2 roll 20 string cvs (; ) 7 2 roll 20 string cvs (; ) 8 2% roll Y 20 string cvs (; ) 10 2 roll X 20 string cvs (, ) 12 2 roll (\string\n) 13 array astore concatstringarray tx@NodeDict begin NodeFile exch writestring end } if \fi\tx@NewNode end end}\hbox{\displaystyle{X_{2}}}}}\hss}\leavevmode\immediate\special{PST: % \pst@dict gsave \tx@STV newpath \pst@code\space grestore end}\ignorespaces% \ignorespaces\ignorespaces}}\hss}}\ignorespaces}}\hss}}\kern 84.598679pt}$

Here, $X_{1}$ and $X_{2}$ are assumptions and $Y$ the corresponding conclusion of some (binary) rule $R$, and $Y$ is the assumption and $Z$ is the conclusion of some (unary) rule $S$. Inference rules may be specified as labels of the edges.

Deductions in deduction systems such as natural deduction or sequent calculus are presented this way. In those systems, the edges of the trees are replaced by horizontal lines, dividing premises and conclusions, and rules are sometimes specified next to the lines, in the following fashion:

$X_{1}$         $X_{2}$   $R$                $Y$                $S$                $Z$

## Deducibility Relation

Given a deductive system $D$, if $B$ is the conclusion of a deduction from a set $\Delta$, we write

 $\Delta\vdash_{D}B.$

If $\Gamma$ is another set of wff’s, we also write $\Delta,\Gamma\vdash_{D}B$ to mean $\Delta\cup\Gamma\vdash_{D}B$. In addition  , if $\Gamma=\{A_{1},\ldots,A_{n}\}$, we write

 $A_{1},\ldots,A_{n}\vdash_{D}B\qquad\mbox{and}\qquad\Delta,A_{1},\ldots,A_{n}% \vdash_{D}B$

to mean $\Gamma\vdash_{D}B$ and $\Delta\cup\Gamma\vdash_{D}B$ respectively. Furthermore, we may also remove the subscript $D$ and write

 $\Delta\vdash B$

if no confusion arises. When $\Delta\vdash B$, we also say that $B$ is deducible from $\Delta$. The turnstile symbol $\vdash$ is also called the deducibility relation.

If a formula $A$ is deducible from $\varnothing$, we say that $A$ is a theorem  (of the corresponding deductive system). In symbol, we write

 $\vdash_{D}A\qquad\mbox{or}\qquad\vdash A.$

A property of $\vdash$ is the following:

if $\vdash A$ and $A\vdash B$, then $\vdash B$.

In other words, if $A$ is a theorem, and $B$ can be deduced from $A$, then $B$ is also a theorem, which conforms with our intuition. More generally, we have

if $\Delta\vdash A$ and $\Gamma,A\vdash B$, then $\Delta,\Gamma\vdash B$.

Remark. We refrain from calling a deduction a proof. As we have seen earlier, deductions are mathematical abstractions of proofs. So they are mathematical constructed, viewed either as sequences or trees (of formulas). On the other hand, in the literature, “proof” is usually reserved to be used in the meta-language, as in the “proof” of Fermat’s Last Theorem, etc…

## References

• 1 A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, 2nd Edition, Cambridge University Press, 2000
• 2 D. Dalen, , 4th Edition, Springer, 2008
 Title deduction Canonical name Deduction Date of creation 2013-03-22 19:12:53 Last modified on 2013-03-22 19:12:53 Owner CWoo (3771) Last modified by CWoo (3771) Numerical id 12 Author CWoo (3771) Entry type Definition Classification msc 03F03 Classification msc 03B99 Classification msc 03B22 Synonym proof tree Synonym proof sequence Synonym hypothesis Defines deduction tree Defines deduction sequence Defines deducible Defines deducibility relation Defines assumption