rules-and-proofs.tex

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

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

\begin{document}

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

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

\begin{explain}
  Axiomatic !!{derivation}s are perhaps the simplest !!{derivation} system for
  logic. !!^a{derivation} is just a sequence of !!{formula}s.  To
  count as !!a{derivation}, every !!{formula} in the sequence must
  either be an instance of an axiom, or must follow from one or more
  !!{formula}s that precede it in the sequence by a rule of inference.
  !!^a{derivation} !!{derive}s its last !!{formula}.
\end{explain}

\begin{defn}[!!^{derivability}]
If $\Gamma$ is a set of !!{formula}s of $\Lang L$ then a
\emph{!!{derivation}} from~$\Gamma$ is a finite sequence $!A_1$,
\dots,~$!A_n$ of !!{formula}s where for each $i \le n$ one of the
following holds:
\begin{enumerate}
\item $!A_i \in \Gamma$; or
\item $!A_i$ is an axiom; or
\item $!A_i$ follows from some $!A_j$ (and $!A_k$) with $j < i$ (and
  $k < i$) by a rule of inference.
\end{enumerate}
\end{defn}

What counts as a correct !!{derivation} depends on which inference
rules we allow (and of course what we take to be axioms).  And an
inference rule is an if-then statement that tells us that, under
certain conditions, a step~$A_i$ in !!a{derivation} is a correct
inference step.

\begin{defn}[Rule of inference]
A \emph{rule of inference} gives a sufficient condition for what
counts as a correct inference step in !!a{derivation} from~$\Gamma$.
\end{defn}

For instance, since any one-element sequence $!A$ with $!A \in \Gamma$
trivially counts as !!a{derivation}, the following might be a very
simple rule of inference:
\begin{quote}
  If $!A \in \Gamma$, then $!A$ is always a correct inference step in
  any !!{derivation} from~$\Gamma$.
\end{quote}
Similarly, if $!A$ is one of the axioms, then $!A$ by itself is
!!a{derivation}, and so this is also a rule of inference:
\begin{quote}
  If $!A$ is an axiom, then $!A$ is a correct inference step.
\end{quote}
It gets more interesting if the rule of inference appeals to
!!{formula}s that appear before the step considered. The following
rule is called \emph{modus ponens:}
\begin{quote}
  If $!B \lif !A$ and $!B$ occur higher up in the !!{derivation},
  then~$!A$ is a correct inference step.
\end{quote}
If this is the only rule of inference, then our definition of
!!{derivation} above amounts to this: $!A_1$, \dots,~$!A_n$ is
!!a{derivation} iff for each $i \le n$ one of the following holds:
\begin{enumerate}
\item $!A_i \in \Gamma$; or
\item $!A_i$ is an axiom; or
\item for some $j < i$, $!A_j$ is $!B \lif !A_i$, and for some $k < i$,
  $!A_k$ is~$!B$.
\end{enumerate}
The last clause says that $!A_i$ follows from~$!A_j$ ($!B \lif !A_i$) and $!A_k$
($!B$) by modus ponens. If we can go from $1$ to~$n$, and
each time we find !!a{formula}~$!A_i$ that is either in~$\Gamma$, an
axiom, or which a rule of inference tells us that it is a correct
inference step, then the entire sequence counts as a correct
!!{derivation}.

\begin{defn}[!!^{derivability}]
A !!{formula}~$!A$ is \emph{!!{derivable}} from $\Gamma$, written
$\Gamma \Proves !A$, if there is !!a{derivation} from $\Gamma$ ending
in $!A$.
\end{defn}

\begin{defn}[Theorems]
!!^a{formula}~$!A$ is a \emph{theorem} if there is !!a{derivation}
of~$!A$ from the empty set.  We write $\Proves !A$ if $!A$ is a
theorem and $\Proves/ !A$ if it is not.
\end{defn}


\end{document}