% Part: first-order-logic
% Chapter: natural-deduction
% Section: rules-and-proofs

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

\begin{document}

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

\olsection{Rules and \usetoken{P}{derivation}}

\begin{explain}
Natural deduction systems are meant to closely parallel the informal
reasoning used in mathematical proof (hence it is somewhat
``natural''). Natural deduction proofs begin with assumptions.
Inference rules are then applied. Assumptions are ``!!{discharged}''
by the \Intro{\lnot}, \Intro{\lif}, \iftag{FOL}{\Elim{\lor} and
  \Elim{\lexists}}{ and \Elim{\lor}} inference rules, and the label of
the !!{discharged} assumption is placed beside the inference for
clarity.
\end{explain}

\begin{defn}[Assumption]
An \emph{assumption} is any !!{sentence}
in the topmost position of any branch.
\end{defn}

!!^{derivation}s in natural deduction are certain trees of
!!{sentence}s, where the topmost !!{sentence}s are assumptions, and if
!!a{sentence} stands below one, two, or three other sequents, it must
follow correctly by a rule of inference. The !!{sentence}s at the top
of the inference are called the \emph{premises} and the !!{sentence}
below the \emph{conclusion} of the inference.  The rules come in
pairs, an introduction and an elimination rule for each
!!{operator}. They introduce !!a{operator} in the conclusion or
remove !!a{operator} from a premise of the rule.  Some of the rules
allow an assumption of a certain type to be \emph{!!{discharged}}. To
indicate which assumption is !!{discharged} by which inference, we
also assign labels to both the assumption and the inference.  This is
indicated by writing the assumption as ``$\Discharge{!A}{n}$.''

% Only include this sentence is on of \land, lor, lif or lnot is defined.

\iftag{notprvNot,notprvAnd,notprvOr,notprvIf}{}%
	{It is customary to consider rules for all the !!{operator}s $\land$, $\lor$, $\lif$, $\lnot$, and $\lfalse$, even if some of those are defined.}



\end{document}