% Part: first-order-logic
% Chapter: natural-deduction
% Section: derivations

\documentclass[../../../include/open-logic-section]{subfiles}

\begin{document}

\iftag{FOL}
      {\olfileid{fol}{ntd}{der}}
      {\olfileid{pl}{ntd}{der}}

\olsection{\usetoken{P}{derivation}}

\begin{explain}
We've said what an assumption is, and we've given the rules of
inference.  !!^{derivation}s in natural deduction are inductively
generated from these: each !!{derivation} either is an assumption
on its own, or consists of one, two, or three !!{derivation}s followed
by a correct inference.
\end{explain}

\begin{defn}[!!^{derivation}]
\Article{derivation} \emph{!!{derivation}} of !!a{sentence}~$!A$ from
assumptions~$\Gamma$ is a finite tree of !!{sentence}s satisfying the
following conditions:
\begin{enumerate}
\item The topmost !!{sentence}s of the tree are either in $\Gamma$ or
  are !!{discharged} by an inference in the tree.
\item The bottommost !!{sentence} of the tree is~$!A$.
\item Every !!{sentence} in the tree except the sentence~$!A$ at
  the bottom is a premise of a correct application of an inference
  rule whose conclusion stands directly below that !!{sentence} in the
  tree.
\end{enumerate}
We then say that $!A$ is the \emph{conclusion} of the !!{derivation}
and $\Gamma$ its !!{undischarged} assumptions.

If !!a{derivation} of $!A$ from~$\Gamma$ exists, we say that $!A$ is
\emph{!!{derivable}} from~$\Gamma$, or in symbols: $\Gamma \Proves
!A$. If there is !!a{derivation} of~$!A$ in which every assumption is
!!{discharged}, we write~$\Proves !A$.
\end{defn}

\begin{ex}
Every assumption on its own is !!a{derivation}. So, e.g., $!A$ by
itself is !!a{derivation}, and so is $!B$ by itself.  We can obtain a
new !!{derivation} from these by applying, say, the $\Intro{\land}$
rule,
\begin{prooftree}
\AxiomC{$!A$}
\AxiomC{$!B$}
\RightLabel{\Intro{\land}}
\BinaryInfC{$!A \land !B$}
\end{prooftree}
These rules are meant to be general: we can replace the $!A$ and~$!B$
in it with any !!{sentence}s, e.g., by $!C$ and~$!D$. Then the
conclusion would be $!C \land !D$, and so
\begin{prooftree}
\AxiomC{$!C$}
\AxiomC{$!D$}
\RightLabel{\Intro{\land}}
\BinaryInfC{$!C \land !D$}
\end{prooftree}
is a correct !!{derivation}. Of course, we can also switch the
assumptions, so that $!D$ plays the role of~$!A$ and $!C$ that
of~$!B$. Thus,
\begin{prooftree}
\AxiomC{$!D$}
\AxiomC{$!C$}
\RightLabel{\Intro{\land}}
\BinaryInfC{$!D \land !C$}
\end{prooftree}
is also a correct !!{derivation}.

We can now apply another rule, say, $\Intro{\lif}$, which allows us to
conclude a conditional and allows us to !!{discharge} any assumption
that is identical to the antecedent of that conditional. So both of
the following would be correct !!{derivation}s:
\begin{prooftree}
\AxiomC{$\Discharge{!C}{1}$}
\AxiomC{$!D$}
\RightLabel{\Intro{\land}}
\BinaryInfC{$!C \land !D$}
\DischargeRule{\Intro{\lif}}{1}
\UnaryInfC{$!C \lif (!C \land !D)$}
\DisplayProof\bottomAlignProof
\AxiomC{$!C$}
\AxiomC{$\Discharge{!D}{1}$}
\RightLabel{\Intro{\land}}
\BinaryInfC{$!C \land !D$}
\DischargeRule{\Intro{\lif}}{1}
\UnaryInfC{$!D \lif (!C \land !D)$}
\end{prooftree}
They show, respectively, that $!D \Proves !C \lif (!C \land !D)$ and
$!C \Proves !D \lif (!C \land !D)$.

Remember that discharging of assumptions is a permission, not a
requirement: we don't have to discharge the assumptions. In
particular, we can apply a rule even if the assumptions are not
present in the !!{derivation}. For instance, the following is legal, even
though there is no assumption~$!A$ to be !!{discharged}:
\begin{prooftree}
  \AxiomC{$!B$}
  \DischargeRule{\Intro{\lif}}{1}
  \UnaryInfC{$!A \lif !B$}
\end{prooftree}
\end{ex}

\end{document}