% Part: first-order-logic
% Chapter: natural-deduction
% Section: proof-theoretic-notions

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

\begin{document}

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

\olsection{Proof-Theoretic Notions}

\begin{editorial}
This section collects the definitions the provability relation
and consistency for natural deduction.
\end{editorial}

\begin{explain}
Just as we've defined a number of important semantic notions
(validity, entailment, satisfiability), we now define corresponding
\emph{proof-theoretic notions}.  These are not defined by appeal to
satisfaction of !!{sentence}s in !!{structure}s, but by appeal to the
!!{derivability} or !!{nonderivability} of certain !!{sentence}s from
others.  It was an important discovery that these notions coincide.
That they do is the content of the \emph{soundness} and
\emph{completeness theorems}.
\end{explain}


\begin{defn}[Theorems]
A !!{sentence}~$!A$ is a \emph{theorem} if there is !!a{derivation}
of~$!A$ in natural deduction in which all assumptions are
!!{discharged}.  We write $\Proves !A$ if $!A$ is a theorem and
$\Proves/ !A$ if it is not.
\end{defn}

\begin{defn}[!!^{derivability}]
!!^a{sentence} $!A$ is \emph{!!{derivable} from} a set of
!!{sentence}s~$\Gamma$, $\Gamma \Proves !A$, if there is a
!!{derivation} with conclusion~$!A$ and in which every assumption
is either !!{discharged} or is in~$\Gamma$. If $!A$ is not
!!{derivable} from $\Gamma$ we write $\Gamma \Proves/ !A$.
\end{defn}

\begin{defn}[Consistency]
A set of !!{sentence}s~$\Gamma$ is \emph{inconsistent} iff $\Gamma
\Proves \lfalse$.  If $\Gamma$ is not inconsistent, i.e., if
$\Gamma \Proves/ \lfalse$, we say it is \emph{consistent}.
\end{defn}

\begin{prop}[Reflexivity]
\ollabel{prop:reflexivity}
If $!A \in \Gamma$, then $\Gamma \Proves !A$.
\end{prop}

\begin{proof}
The assumption $!A$ by itself is !!a{derivation} of~$!A$ where every
!!{undischarged} assumption (i.e., $!A$) is in~$\Gamma$.
\end{proof}
  

\begin{prop}[Monotonicity]
\ollabel{prop:monotonicity}
If $\Gamma \subseteq \Delta$ and $\Gamma \Proves !A$, then $\Delta
\Proves !A$.
\end{prop}

\begin{proof}
Any !!{derivation} of $!A$ from $\Gamma$ is also !!a{derivation} of
$!A$ from~$\Delta$.
\end{proof}

\begin{prop}[Transitivity]
\ollabel{prop:transitivity}
If $\Gamma \Proves !A$ and $\{!A\} \cup \Delta \Proves
!B$, then $\Gamma \cup \Delta \Proves !B$.
\end{prop}

\begin{proof}
If $\Gamma \Proves !A$, there is !!a{derivation}~$\delta_0$ of~$!A$
with all !!{undischarged} assumptions in~$\Gamma$.  If $\{!A\} \cup
\Delta \Proves !B$, then there is !!a{derivation}~$\delta_1$ of~$!B$
with all !!{undischarged} assumptions in~$\{!A\} \cup \Delta$.
Now consider:
\begin{prooftree}
  \AxiomC{$\Delta, \Discharge{!A}{1}$}
  \RightLabel{$\delta_1$}
  \DeduceC{$!B$}
  \DischargeRule{\Intro{\lif}}{1}
  \UnaryInfC{$!A \lif !B$}
  \AxiomC{$\Gamma$}
  \RightLabel{$\delta_0$}
  \DeduceC{$!A$}
  \RightLabel{\Elim{\lif}}
  \BinaryInfC{$!B$}
\end{prooftree}
The !!{undischarged} assumptions are now all among $\Gamma \cup
\Delta$, so this shows $\Gamma \cup \Delta \Proves !B$.
\end{proof}

When $\Gamma = \{!A_1, !A_2, \ldots, !A_k\}$ is a finite set we may use the simplified notation $!A_1,!A_2,\ldots,!A_k \Proves !B$ for $\Gamma \Proves !B$, in particular $!A \Proves !B$ means that $\{!A\} \Proves !B$.

Note that if $\Gamma \Proves !A$ and $!A
\Proves !B$, then $\Gamma \Proves !B$. It follows also that if $!A_1,
\dots, !A_n \Proves !B$ and $\Gamma \Proves !A_i$ for each~$i$, then
$\Gamma \Proves !B$.

\begin{prop}
\ollabel{prop:incons}
The following are equivalent. 
    \begin{enumerate}
      \item \( \Gamma \) is inconsistent.
      \item \( \Gamma \Proves {!A} \) for every !!{sentence}~\( {!A} \).
      \item \( \Gamma \Proves {!A} \) and \( \Gamma \Proves \lnot {!A} \) for some !!{sentence}~\( {!A} \).
    \end{enumerate}
\end{prop}

\begin{proof}
Exercise.
\end{proof}

\tagprob{FOL}
\begin{prob}
Prove \olref[fol][ntd][ptn]{prop:incons}
\end{prob}
\tagendprob

\tagprob{notFOL}
\begin{prob}
Prove \olref[pl][ntd][ptn]{prop:incons}
\end{prob}
\tagendprob

\begin{prop}[Compactness]
  \ollabel{prop:proves-compact}
  \begin{enumerate}
  \item If $\Gamma \Proves !A$ then there is a finite subset $\Gamma_0
    \subseteq \Gamma$ such that $\Gamma_0 \Proves !A$.
  \item If every finite subset of~$\Gamma$ is
    consistent, then $\Gamma$ is consistent.
  \end{enumerate}
\end{prop}

\begin{proof}
  \begin{enumerate}
    \item If $\Gamma \Proves !A$, then there is
      !!a{derivation}~$\delta$ of~$!A$ from~$\Gamma$. Let $\Gamma_0$
      be the set of !!{undischarged} assumptions of~$\delta$.  Since
      any !!{derivation} is finite, $\Gamma_0$ can only contain
      finitely many !!{sentence}s.  So, $\delta$ is !!a{derivation}
      of~$!A$ from a finite~$\Gamma_0 \subseteq \Gamma$.
    \item This is the contrapositive of (1) for the special case $!A
      \ident \lfalse$.
  \end{enumerate}
\end{proof}

\end{document}