Natural Deduction — Source and provenance

Source and provenance

All nine files in the exact Propositional Natural Deduction source boundary appear line by line and are copied byte-for-byte for offline inspection.

content/first-order-logic/natural-deduction/natural-deduction.tex

55 lines; SHA-256 8fa1e5a3e1211ce9c55e0ff66acbb8d5a6a9af360529d7775587a626fbe49b8e. Open the preserved source file.

% Part: first-order-logic
% Chapter: natural-deduction
\documentclass[../../../include/open-logic-chapter]{subfiles}
\begin{document}
\iftag{FOL}
{\olchapter{fol}{ntd}{Natural Deduction}}
{\olchapter{pl}{ntd}{Natural Deduction}}
\begin{editorial}
This chapter presents a natural deduction system in the style of
Gentzen/Prawitz.
To include or exclude material relevant to natural deduction as a
proof system, use the ``prfND'' tag.
\end{editorial}
\olimport{rules-and-proofs}
\olimport{propositional-rules}
\iftag{FOL}{%
\olimport{quantifier-rules}
}{}
\olimport{derivations}
\olimport{proving-things}
\iftag{FOL}{%
\olimport{proving-things-quant}
}{}
\olimport{proof-theoretic-notions}
\olimport{provability-consistency}
\olimport{provability-propositional}
\iftag{FOL}{%
\olimport{provability-quantifiers}
}{}
\olimport{soundness}
\iftag{FOL}{%
\olimport{identity}
\olimport{soundness-identity}
}{}
\OLEndChapterHook
\end{document}

content/first-order-logic/natural-deduction/rules-and-proofs.tex

52 lines; SHA-256 0556326eefd6fbb957243d9f94969fd23adefb4af69f80419d4a2818d53088f0. Open the preserved source file.

% 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}

content/first-order-logic/natural-deduction/propositional-rules.tex

120 lines; SHA-256 c22d2603cc9c4a79d630a4bc00b817c57c07b000e5d4bc443815e13b4f4cb515. Open the preserved source file.

% Part: first-order-logic
% Chapter: natural-deduction
% Section: propositional-rules
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{ntd}{prl}}
{\olfileid{pl}{ntd}{prl}}
\olsection{Propositional Rules}
\subsection{Rules for $\land$}
\begin{defish}
\AxiomC{$!A$}
\AxiomC{$!B$}
\RightLabel{\Intro{\land}}
\BinaryInfC{$!A \land !B$}
\DisplayProof
\hfill
\begin{tabular}{r}
\AxiomC{$!A \land !B$}
\RightLabel{\Elim{\land}}
\UnaryInfC{$!A$}
\DisplayProof
\\[3ex]
\AxiomC{$!A \land !B$}
\RightLabel{\Elim{\land}}
\UnaryInfC{$!B$}
\DisplayProof
\end{tabular}
\end{defish}
\subsection{Rules for $\lor$}
\begin{defish}
\begin{tabular}{r}
\AxiomC{$!A$}
\RightLabel{\Intro{\lor}}
\UnaryInfC{$!A \lor !B$}
\DisplayProof
\\[3ex]
\AxiomC{$!B$}
\RightLabel{\Intro{\lor}}
\UnaryInfC{$!A \lor !B$}
\DisplayProof
\end{tabular}
\hfill
\AxiomC{$!A \lor !B$}
\AxiomC{$\Discharge{!A}{n}$}
\DeduceC{$!C$}
\AxiomC{$\Discharge{!B}{n}$}
\DeduceC{$!C$}
\DischargeRule{\Elim{\lor}}{n}
\TrinaryInfC{$!C$}
\DisplayProof
\end{defish}
\subsection{Rules for $\lif$}
\begin{defish}
\AxiomC{$\Discharge{!A}{n}$}
\DeduceC{$!B$}
\DischargeRule{\Intro{\lif}}{n}
\UnaryInfC{$!A \lif !B$}
\DisplayProof
\hfill
\AxiomC{$!A \lif !B$}
\AxiomC{$!A$}
\RightLabel{\Elim{\lif}}
\BinaryInfC{$!B$}
\DisplayProof
\end{defish}
\subsection{Rules for $\lnot$}
\begin{defish}
\AxiomC{$\Discharge{!A}{n}$}
\noLine
\DeduceC{$\lfalse$}
\DischargeRule{\Intro{\lnot}}{n}
\UnaryInfC{$\lnot !A$}
\DisplayProof
\hfill
\AxiomC{$\lnot !A$}
\AxiomC{$!A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\DisplayProof
\end{defish}
\subsection{Rules for $\lfalse$}
\begin{defish}
\AxiomC{$\lfalse$}
\RightLabel{\FalseInt}
\UnaryInfC{$!A$}
\DisplayProof
\hfill
\AxiomC{$\Discharge{\lnot !A}{n}$}
\DeduceC{$\lfalse$}
\DischargeRule{\FalseCl}{n}
\UnaryInfC{$!A$}
\DisplayProof
\end{defish}
Note that $\Intro{\lnot}$ and $\FalseCl$ are very similar: The
difference is that $\Intro{\lnot}$ derives a negated
!!{sentence}~$\lnot !A$ but $\FalseCl$ a positive !!{sentence}~$!A$.
Whenever a rule indicates that some assumption may be discharged, we
take this to be a permission, but not a requirement. E.g., in the
$\Intro{\lif}$ rule, we may discharge any number of assumptions of the
form~$!A$ in the !!{derivation} of the premise~$!B$, including zero.
\end{document}

content/first-order-logic/natural-deduction/derivations.tex

110 lines; SHA-256 04cdbaa301a71243b78d880551ce2f8edbf6f059764eceacd5b8910f0459cb26. Open the preserved source file.

% 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}

content/first-order-logic/natural-deduction/proving-things.tex

310 lines; SHA-256 ff58b86389a21dbc6f240f49e62d5fca0bdb4d3ba54e0d364792cdcddd34724f. Open the preserved source file.

% Part: first-order-logic
% Chapter: natural-deduction
% Section: proving-things
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{ntd}{pro}}
{\olfileid{pl}{ntd}{pro}}
\olsection{Examples of \usetoken{P}{derivation}}
\begin{ex}
Let's give !!a{derivation} of the !!{sentence} $(!A \land !B) \lif !A$.
We begin by writing the desired conclusion at the bottom of the
!!{derivation}.
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$(!A\land !B) \lif !A$}
\end{prooftree}
Next, we need to figure out what kind of inference could result in
!!a{sentence} of this form. The !!{main operator} of the
conclusion is $\lif$, so we'll try to arrive at the
conclusion using the \Intro{\lif} rule. It is best to write down
the assumptions involved and label the inference rules as you
progress, so it is easy to see whether all assumptions have been
!!{discharged} at the end of the proof.
\begin{prooftree}
\AxiomC{$\Discharge{!A \land !B}{1}$}
\DeduceC{$!A$}
\DischargeRule{\Intro{\lif}}{1}
\UnaryInfC{$(!A\land !B) \lif !A$}
\end{prooftree}
We now need to fill in the steps from the assumption $!A \land !B$ to $!A$.
Since we only have one connective to deal with, $\land$, we must
use the $\land$ elim rule. This gives us the following proof:
\begin{prooftree}
\AxiomC{$\Discharge{!A \land !B}{1}$}
\RightLabel{\Elim{\land}}
\UnaryInfC{$!A$}
\DischargeRule{\Intro{\lif}}{1}
\UnaryInfC{$(!A\land !B) \lif !A$}
\end{prooftree}
We now have a correct !!{derivation} of $(!A \land
!B) \lif !A$.
\end{ex}
\begin{ex}
Now let's give !!a{derivation} of $(\lnot !A \lor !B)
\lif (!A \lif !B)$.
We begin by writing the desired conclusion at the bottom of the
!!{derivation}.
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
\end{prooftree}
To find a logical rule that could give us this conclusion, we
look at the logical connectives in the conclusion: $\lnot$,
$\lor$, and $\lif$. We only care at the moment about the first
occurrence of $\lif$ because it is the !!{main operator} of the
!!{sentence} in the end-sequent, while $\lnot$, $\lor$ and the second
occurrence of $\lif$ are inside the scope of another connective, so we
will take care of those later. We therefore start with the
\Intro{\lif} rule. A correct application must look like this:
\begin{prooftree}
\AxiomC{$\Discharge{\lnot !A \lor !B}{1}$}
\DeduceC{$!A \lif !B$}
\DischargeRule{\Intro{\lif}}{1}
\UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
\end{prooftree}
This leaves us with two possibilities to continue. Either we can
keep working from the bottom up and look for another application
of the \Intro{\lif} rule, or we can work from the top down and apply a
\Elim{\lor} rule. Let us apply the latter. We will use the assumption
$\lnot !A \lor !B$ as the leftmost premise of \Elim{\lor}. For a valid
application of \Elim{\lor}, the other two premises must be identical
to the conclusion $!A \lif !B$, but each may be derived in turn from
another assumption, namely one of the two disjuncts of $\lnot !A \lor !B$.
So our !!{derivation} will look like this:
\begin{prooftree}
\AxiomC{$\Discharge{\lnot !A \lor !B}{1}$}
\AxiomC{$\Discharge{\lnot !A}{2}$}
\DeduceC{$!A \lif !B$}
\AxiomC{$\Discharge{!B}{2}$}
\DeduceC{$!A \lif !B$}
\DischargeRule{\Elim{\lor}}{2}
\TrinaryInfC{$!A \lif !B$}
\DischargeRule{\Intro{\lif}}{1}
\UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
\end{prooftree}
In each of the two branches on the right, we want to !!{derive} $!A
\lif !B$, which is best done using \Intro{\lif}.
\begin{prooftree}
\AxiomC{$\Discharge{\lnot !A \lor !B}{1}$}
\AxiomC{$\Discharge{\lnot !A}{2}, \Discharge{!A}{3}$}
\DeduceC{$!B$}
\DischargeRule{\Intro{\lif}}{3}
\UnaryInfC{$!A \lif !B$}
\AxiomC{$\Discharge{!B}{2}, \Discharge{!A}{4}$}
\DeduceC{$!B$}
\DischargeRule{\Intro{\lif}}{4}
\UnaryInfC{$!A \lif !B$}
\DischargeRule{\Elim{\lor}}{2}
\TrinaryInfC{$!A \lif !B$}
\DischargeRule{\Intro{\lif}}{1}
\UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
\end{prooftree}
For the two missing parts of the !!{derivation}, we need
!!{derivation}s of $!B$ from $\lnot !A$ and $!A$ in the middle, and
from $!A$ and $!B$ on the left. Let's take the former first. $\lnot
!A$ and $!A$ are the two premises of \Elim{\lnot}:
\begin{prooftree}
\AxiomC{$\Discharge{\lnot !A}{2}$}
\AxiomC{$\Discharge{!A}{3}$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\DeduceC{$!B$}
\end{prooftree}
By using \FalseInt, we can obtain $!B$ as a conclusion and
complete the branch.
\begin{prooftree}
\AxiomC{$\Discharge{\lnot !A \lor !B}{1}$}
\AxiomC{$\Discharge{\lnot !A}{2}$}
\AxiomC{$\Discharge{!A}{3}$}
\RightLabel{\Intro{\lfalse}}
\BinaryInfC{$\lfalse$}
\RightLabel{\FalseInt}
\UnaryInfC{$!B$}
\DischargeRule{\Intro{\lif}}{3}
\UnaryInfC{$!A \lif !B$}
\AxiomC{$\Discharge{!B}{2}, \Discharge{!A}{4}$}
\DeduceC{$!B$}
\DischargeRule{\Intro{\lif}}{4}
\UnaryInfC{$!A \lif !B$}
\DischargeRule{\Elim{\lor}}{2}
\TrinaryInfC{$!A \lif !B$}
\DischargeRule{\Intro{\lif}}{1}
\UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
\end{prooftree}
Let's now look at the rightmost branch. Here it's important to
realize that the definition of !!{derivation} \emph{allows assumptions
to be discharged} but \emph{does not require} them to be. In other
words, if we can derive $!B$ from one of the assumptions $!A$ and $!B$
without using the other, that's ok. And to !!{derive} $!B$ from~$!B$
is trivial: $!B$ by itself is such !!a{derivation}, and no inferences
are needed. So we can simply delete the assumption~$!A$.
\begin{prooftree}
\AxiomC{$\Discharge{\lnot !A \lor !B}{1}$}
\AxiomC{$\Discharge{\lnot !A}{2}$}
\AxiomC{$\Discharge{!A}{3}$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\RightLabel{\FalseInt}
\UnaryInfC{$!B$}
\DischargeRule{\Intro{\lif}}{3}
\UnaryInfC{$!A \lif !B$}
\AxiomC{$\Discharge{!B}{2}$}
\RightLabel{\Intro{\lif}}
\UnaryInfC{$!A \lif !B$}
\DischargeRule{\Elim{\lor}}{2}
\TrinaryInfC{$!A \lif !B$}
\DischargeRule{\Intro{\lif}}{1}
\UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
\end{prooftree}
Note that in the finished !!{derivation}, the rightmost \Intro{\lif}
inference does not actually discharge any assumptions.
\end{ex}
\begin{ex}
So far we have not needed the \FalseCl{} rule. It is special in that
it allows us to discharge an assumption that isn't a sub-!!{formula} of
the conclusion of the rule. It is closely related to the \FalseInt{}
rule. In fact, the \FalseInt{} rule is a special case of the
\FalseCl{} rule---there is a logic called ``intuitionistic logic'' in
which only \FalseInt{} is allowed. The \FalseCl{} rule is a last
resort when nothing else works. For instance, suppose we want to
!!{derive} $!A \lor \lnot !A$. Our usual strategy would be to attempt
to !!{derive} $!A \lor \lnot !A$ using $\Intro{\lor}$. But this would
require us to !!{derive} either $!A$ or $\lnot !A$ from no
assumptions, and this can't be done. \FalseCl{} to the rescue!
\begin{prooftree}
\AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
\DeduceC{$\lfalse$}
\DischargeRule{\FalseCl}{1}
\UnaryInfC{$!A \lor \lnot !A$}
\end{prooftree}
Now we're looking for !!a{derivation} of $\lfalse$ from $\lnot(!A \lor
\lnot !A)$. Since $\lfalse$ is the conclusion of $\Elim{\lnot}$ we
might try that:
\begin{prooftree}
\AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
\DeduceC{$\lnot !A$}
\AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
\DeduceC{$!A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\DischargeRule{\FalseCl}{1}
\UnaryInfC{$!A \lor \lnot !A$}
\end{prooftree}
Our strategy for finding !!a{derivation} of~$\lnot !A$ calls for an
application of~$\Intro{\lnot}$:
\begin{prooftree}
\AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}, \Discharge{!A}{2}$}
\DeduceC{$\lfalse$}
\DischargeRule{\Intro{\lnot}}{2}
\UnaryInfC{$\lnot !A$}
\AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
\DeduceC{$!A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\DischargeRule{\FalseCl}{1}
\UnaryInfC{$!A \lor \lnot !A$}
\end{prooftree}
Here, we can get $\lfalse$ easily by applying $\Elim{\lnot}$ to the
assumption $\lnot(!A \lor \lnot !A)$ and $!A \lor \lnot !A$ which
follows from our new assumption $!A$ by~$\Intro{\lor}$:
\begin{prooftree}
\AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
\AxiomC{$\Discharge{!A}{2}$}
\RightLabel{\Intro{\lor}}
\UnaryInfC{$!A \lor \lnot !A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\DischargeRule{\Intro{\lnot}}{2}
\UnaryInfC{$\lnot !A$}
\AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
\DeduceC{$!A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\DischargeRule{\FalseCl}{1}
\UnaryInfC{$!A \lor \lnot !A$}
\end{prooftree}
On the right side we use the same strategy, except we get $!A$ by~\FalseCl:
\begin{prooftree}
\AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
\AxiomC{$\Discharge{!A}{2}$}
\RightLabel{\Intro{\lor}}
\UnaryInfC{$!A \lor \lnot !A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\DischargeRule{\Intro{\lnot}}{2}
\UnaryInfC{$\lnot !A$}
\AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
\AxiomC{$\Discharge{\lnot !A}{3}$}
\RightLabel{\Intro{\lor}}
\UnaryInfC{$!A \lor \lnot !A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\DischargeRule{\FalseCl}{3}
\UnaryInfC{$!A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\DischargeRule{\FalseCl}{1}
\UnaryInfC{$!A \lor \lnot !A$}
\end{prooftree}
\end{ex}
\begin{prob}
Give !!{derivation}s that show the following:
\begin{enumerate}
\item $!A \land (!B \land !C) \Proves (!A \land !B) \land !C$.
\item $!A \lor (!B \lor !C) \Proves (!A \lor !B) \lor !C$.
\item $!A \lif (!B \lif !C) \Proves !B \lif (!A \lif !C)$.
\item $!A \Proves \lnot\lnot !A$.
\end{enumerate}
\end{prob}
\begin{prob}
Give !!{derivation}s that show the following:
\begin{enumerate}
\item $(!A \lor !B) \lif !C \Proves !A \lif !C$.
\item $(!A \lif !C) \land (!B \lif !C) \Proves (!A \lor !B) \lif !C$.
\item $\Proves \lnot(!A \land \lnot !A)$.
\item $!B \lif !A \Proves \lnot !A \lif \lnot !B$.
\item $\Proves (!A \lif \lnot !A) \lif \lnot !A$.
\item $\Proves \lnot(!A \lif !B) \lif \lnot !B$.
\item $!A \lif !C \Proves \lnot (!A \land \lnot !C)$.
\item $!A \land \lnot !C \Proves \lnot (!A \lif !C)$.
\item $!A \lor !B, \lnot !B \Proves !A$.
\item $\lnot !A \lor \lnot !B \Proves \lnot(!A \land !B)$.
\item $\Proves (\lnot !A \land \lnot !B) \lif\lnot(!A \lor !B)$.
\item $\Proves \lnot(!A \lor !B) \lif (\lnot !A \land \lnot !B)$.
\end{enumerate}
\end{prob}
\begin{prob}
Give !!{derivation}s that show the following:
\begin{enumerate}
\item $\lnot(!A \lif !B) \Proves !A$.
\item $\lnot(!A \land !B) \Proves \lnot !A \lor \lnot !B$.
\item $!A \lif !B \Proves \lnot !A \lor !B$.
\item $\Proves \lnot \lnot !A \lif !A$.
\item $!A \lif !B, \lnot !A \lif !B \Proves !B$.
\item $(!A \land !B) \lif !C \Proves (!A \lif !C) \lor (!B \lif !C)$.
\item $(!A \lif !B) \lif !A \Proves !A$.
\item $\Proves (!A \lif !B) \lor (!B \lif !C)$.
\end{enumerate}
(These all require the $\FalseCl$~rule.)
\end{prob}
\end{document}

content/first-order-logic/natural-deduction/proof-theoretic-notions.tex

159 lines; SHA-256 7e05743251dd0c5071685193a98c28baea1c77b06836f11e3f3e3aa6a6bd9198. Open the preserved source file.

% 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}

content/first-order-logic/natural-deduction/provability-consistency.tex

131 lines; SHA-256 9d967013e14c7f911bf612ddab65b22a2e5f8d90f182926741c0bf7cab5076bc. Open the preserved source file.

% Part: first-order-logic
% Chapter: natural-deduction
% Section: provability-consistency
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{ntd}{prv}}
{\olfileid{pl}{ntd}{prv}}
\olsection{\usetoken{S}{derivability} and Consistency}
We will now establish a number of properties of the !!{derivability}
relation. They are independently interesting, but each will play a
role in the proof of the completeness theorem.
\begin{prop}\ollabel{prop:provability-contr}
If $\Gamma \Proves !A$ and $\Gamma \cup \{!A\}$ is inconsistent,
then $\Gamma$ is inconsistent.
\end{prop}
\begin{proof}
Let the !!{derivation} of~$!A$ from~$\Gamma$ be~$\delta_1$ and the
!!{derivation} of~$\lfalse$ from $\Gamma \cup \{!A\}$
be~$\delta_2$. We can then !!{derive}:
\begin{prooftree}
\AxiomC{$\Gamma, \Discharge{!A}{1}$}
\RightLabel{$\delta_2$}
\DeduceC{$\lfalse$}
\DischargeRule{\Intro{\lnot}}{1}
\UnaryInfC{$\lnot !A$}
\AxiomC{$\Gamma$}
\RightLabel{$\delta_1$}
\DeduceC{$!A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\end{prooftree}
In the new !!{derivation}, the assumption~$!A$ is !!{discharged}, so it is
!!a{derivation} from~$\Gamma$.
\end{proof}
\begin{prop}
\ollabel{prop:prov-incons}
$\Gamma \Proves !A$ iff $\Gamma \cup \{\lnot !A\}$ is inconsistent.
\end{prop}
\begin{proof}
First suppose $\Gamma \Proves !A$, i.e., there is
!!a{derivation}~$\delta_0$ of~$!A$ from !!{undischarged}
assumptions~$\Gamma$. We obtain !!a{derivation} of $\lfalse$ from
$\Gamma \cup \{\lnot !A\}$ as follows:
\begin{prooftree}
\AxiomC{$\lnot !A$}
\AxiomC{$\Gamma$}
\RightLabel{$\delta_0$}
\DeduceC{$!A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\end{prooftree}
Now assume $\Gamma \cup \{\lnot !A\}$ is inconsistent, and let
$\delta_1$ be the corresponding !!{derivation} of~$\lfalse$ from
!!{undischarged} assumptions in~$\Gamma \cup \{\lnot !A\}$. We obtain
!!a{derivation} of~$!A$ from~$\Gamma$ alone by using~$\FalseCl$:
\begin{prooftree}
\AxiomC{$\Gamma, \Discharge{\lnot !A}{1}$}
\RightLabel{$\delta_1$}
\DeduceC{$\lfalse$}
\RightLabel{\FalseCl}
\DischargeRule{\FalseCl}{1}
\UnaryInfC{$!A$}
\end{prooftree}
\end{proof}
\begin{prob}
Prove that $\Gamma \Proves \lnot !A$ iff $\Gamma \cup \{!A\}$ is
inconsistent.
\end{prob}
\begin{prop}\ollabel{prop:explicit-inc}
If $\Gamma \Proves !A$ and $\lnot !A \in \Gamma$, then $\Gamma$ is
inconsistent.
\end{prop}
\begin{proof}
Suppose $\Gamma \Proves !A$ and $\lnot !A \in \Gamma$. Then there
is !!a{derivation}~$\delta$ of~$!A$ from~$\Gamma$. Consider this
simple application of the $\Elim{\lnot}$ rule:
\begin{prooftree}
\AxiomC{$\lnot !A$}
\AxiomC{$\Gamma$}
\RightLabel{$\delta$}
\DeduceC{$!A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\end{prooftree}
Since $\lnot !A \in \Gamma$, all !!{undischarged} assumptions are
in~$\Gamma$, this shows that $\Gamma \Proves \lfalse$.
\end{proof}
\begin{prop}\ollabel{prop:provability-exhaustive}
If $\Gamma \cup \{!A\}$ and $\Gamma \cup \{\lnot !A\}$ are both
inconsistent, then $\Gamma$ is inconsistent.
\end{prop}
\begin{proof}
There are !!{derivation}s $\delta_1$ and $\delta_2$ of~$\lfalse$ from
$\Gamma \cup \{ !A \}$ and $\lfalse$ from $\Gamma \cup \{ \lnot !A
\}$, respectively. We can then !!{derive}
\begin{prooftree}
\AxiomC{$\Gamma, \Discharge{\lnot !A}{2}$}
\RightLabel{$\delta_2$}
\DeduceC{$\lfalse$}
\DischargeRule{\Intro{\lnot}}{2}
\UnaryInfC{$\lnot \lnot !A$}
\AxiomC{$\Gamma, \Discharge{!A}{1}$}
\RightLabel{$\delta_1$}
\DeduceC{$\lfalse$}
\DischargeRule{\Intro{\lnot}}{1}
\UnaryInfC{$\lnot !A$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\end{prooftree}
Since the assumptions $!A$ and $\lnot !A$ are !!{discharged}, this is
!!a{derivation} of~$\lfalse$ from~$\Gamma$ alone. Hence $\Gamma$ is
inconsistent.
\end{proof}
\end{document}

content/first-order-logic/natural-deduction/provability-propositional.tex

133 lines; SHA-256 7be41cbf7877f1b7163f3cc9ad98867b4cf793b69f4a98e5734f731e3e802016. Open the preserved source file.

% Part: first-order-logic
% Chapter: natural-deduction
% Section: provability-propositional
% verification of properties of provability needed for maximally
% consistent sets in the completeness chapter.
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{ntd}{ppr}}
{\olfileid{pl}{ntd}{ppr}}
\olsection{\usetoken{S}{derivability} and the Propositional Connectives}
\begin{explain}
We establish that the !!{derivability} relation~$\Proves$ of natural
deduction is strong enough to establish some basic facts
involving the propositional connectives, such as that $!A \land !B
\Proves !A$ and $!A, !A \lif !B \Proves !B$ (modus ponens). These
facts are needed for the proof of the completeness theorem.
\end{explain}
\begin{prop}\ollabel{prop:provability-land}
\begin{enumerate}
\item \ollabel{prop:provability-land-left} Both $!A \land !B \Proves
!A$ and $!A \land !B \Proves !B$
\item \ollabel{prop:provability-land-right} $!A, !B \Proves !A \land !B$.
\end{enumerate}
\end{prop}
\begin{proof}
\begin{enumerate}
\item We can !!{derive} both
\begin{prooftree}
\AxiomC{$!A \land !B$}
\RightLabel{\Elim{\land}}
\UnaryInfC{$!A$}
\DisplayProof\qquad\bottomAlignProof
\AxiomC{$!A \land !B$}
\RightLabel{\Elim{\land}}
\UnaryInfC{$!B$}
\end{prooftree}
\item We can !!{derive}:
\begin{prooftree}
\AxiomC{$!A$}
\AxiomC{$!B$}
\RightLabel{\Intro{\land}}
\BinaryInfC{$!A \land !B$}
\end{prooftree}
\end{enumerate}
\end{proof}
\begin{prop}\ollabel{prop:provability-lor}
\begin{enumerate}
\item $!A \lor !B, \lnot !A, \lnot !B$ is inconsistent.
\item Both $!A \Proves !A \lor !B$ and $!B \Proves !A \lor !B$.
\end{enumerate}
\end{prop}
\begin{proof}
\begin{enumerate}
\item Consider the following !!{derivation}:
\begin{prooftree}
\AxiomC{$!A \lor !B$}
\AxiomC{$\lnot !A$}
\AxiomC{$\Discharge{!A}{1}$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\AxiomC{$\lnot !B$}
\AxiomC{$\Discharge{!B}{1}$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\DischargeRule{\Elim{\lor}}{1}
\TrinaryInfC{$\lfalse$}
\end{prooftree}
This is !!a{derivation} of~$\lfalse$ from !!{undischarged}
assumptions $!A \lor !B$, $\lnot !A$, and $\lnot !B$.
\item We can !!{derive} both
\begin{prooftree}
\AxiomC{$!A$}
\RightLabel{\Intro{\lor}}
\UnaryInfC{$!A \lor !B$}
\DisplayProof\qquad\bottomAlignProof
\AxiomC{$!B$}
\RightLabel{\Intro{\lor}}
\UnaryInfC{$!A \lor !B$}
\end{prooftree}
\end{enumerate}
\end{proof}
\begin{prop}\ollabel{prop:provability-lif}
\begin{enumerate}
\item \ollabel{prop:provability-lif-left} $!A, !A \lif !B \Proves !B$.
\item \ollabel{prop:provability-lif-right}
Both $\lnot !A \Proves !A \lif !B$ and $!B \Proves !A \lif !B$.
\end{enumerate}
\end{prop}
\begin{proof}
\begin{enumerate}
\item We can !!{derive}:
\begin{prooftree}
\AxiomC{$!A \lif !B$}
\AxiomC{$!A$}
\RightLabel{\Elim{\lif}}
\BinaryInfC{$!B$}
\end{prooftree}
\item This is shown by the following two !!{derivation}s:
\begin{prooftree}
\AxiomC{$\lnot !A$}
\AxiomC{$\Discharge{!A}{1}$}
\RightLabel{\Elim{\lnot}}
\BinaryInfC{$\lfalse$}
\RightLabel{\FalseInt}
\UnaryInfC{$!B$}
\DischargeRule{\Intro{\lif}}{1}
\UnaryInfC{$!A \lif !B$}
\DisplayProof\qquad\bottomAlignProof
\AxiomC{$!B$}
\RightLabel{\Intro{\lif}}
\UnaryInfC{$!A \lif !B$}
\end{prooftree}
Note that $\Intro{\lif}$ may, but does not have to, !!{discharge} the
assumption~$!A$.
\end{enumerate}
\end{proof}
\end{document}

content/first-order-logic/natural-deduction/soundness.tex

314 lines; SHA-256 e470b5e3a94dd4445dcedc0bbb2d4bb9c5520a3f79ea754f37e4ae1501376e35. Open the preserved source file.

% Part: first-order-logic
% Chapter: natural-deduction
% Section: soundness
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{ntd}{sou}}
{\olfileid{pl}{ntd}{sou}}
\olsection{Soundness}
\begin{explain}
!!^a{derivation} system, such as natural deduction, is \emph{sound}
if it cannot !!{derive} things that do not actually follow. Soundness is
thus a kind of guaranteed safety property for !!{derivation} systems.
Depending on which proof theoretic property is in question, we would
like to know for instance, that
\begin{enumerate}
\item every !!{derivable} !!{sentence} is \iftag{FOL}{valid}{a tautology};
\item if !!a{sentence} is !!{derivable} from some others, it is also a
consequence of them;
\item if a set of !!{sentence}s is inconsistent, it is unsatisfiable.
\end{enumerate}
These are important properties of !!a{derivation} system. If any of
them do not hold, the !!{derivation} system is deficient---it would
!!{derive} too much. Consequently, establishing the soundness of a
!!{derivation} system is of the utmost importance.
\end{explain}
\begin{thm}[Soundness]
\ollabel{thm:soundness}
If $!A$ is !!{derivable} from the !!{undischarged} assumptions
$\Gamma$, then $\Gamma \Entails !A$.
\end{thm}
\begin{proof}
Let $\delta$ be !!a{derivation} of $!A$. We proceed by
induction on the number of inferences in~$\delta$.
For the induction basis we show the claim if the number of inferences
is~$0$. In this case, $\delta$ consists only of a single
!!{sentence}~$!A$, i.e., an assumption. That assumption is
!!{undischarged}, since assumptions can only be !!{discharged} by
inferences, and there are no inferences. So, any
\iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$}
that satisfies all of the !!{undischarged} assumptions of the proof
also satisfies~$!A$.
Now for the inductive step. Suppose that $\delta$ contains~$n$
inferences. The premise(s) of the lowermost inference are !!{derive}d
using sub-!!{derivation}s, each of which contains fewer than~$n$
inferences. We assume the induction hypothesis: The premises of the
lowermost inference follow from the !!{undischarged} assumptions of
the sub-!!{derivation}s ending in those premises. We have to show
that the conclusion~$!A$ follows from the !!{undischarged} assumptions
of the entire proof.
We distinguish cases according to the type of the lowermost inference.
First, we consider the possible inferences with only one premise.
\begin{enumerate}
\item Suppose that the last inference is \Intro{\lnot}: The
!!{derivation} has the form
\begin{prooftree}
\AxiomC{$\Gamma, \Discharge{!A}{n}$}
\RightLabel{$\delta_1$}
\DeduceC{$\lfalse$}
\DischargeRule{\Intro{\lnot}}{n}
\UnaryInfC{$\lnot !A$}
\end{prooftree}
By inductive hypothesis, $\lfalse$ follows from the !!{undischarged}
assumptions $\Gamma \cup \{!A\}$ of~$\delta_1$. Consider
\iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We
need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\lnot !A}$. Suppose for reductio
that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, but
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lnot !A}$, i.e.,
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. This would mean that
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma \cup \{!A\}}$. This is
contrary to our inductive hypothesis. So,
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\lnot !A}$.
\item The last inference is \Elim{\land}: There are two variants: $!A$
or $!B$ may be inferred from the premise $!A \land !B$. Consider the
first case. The !!{derivation}~$\delta$ looks like this:
\begin{prooftree}
\AxiomC{$\Gamma$}
\RightLabel{$\delta_1$}
\DeduceC{$!A \land !B$}
\RightLabel{\Elim{\land}}
\UnaryInfC{$!A$}
\end{prooftree}
By inductive hypothesis, $!A \land !B$ follows from the
!!{undischarged} assumptions~$\Gamma$ of~$\delta_1$. Consider
!!a{structure}~\iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$}. We need to
show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. Suppose
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$. By our inductive
hypothesis ($\Gamma \Entails !A \land !B$), we know that
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$. By definition,
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$ iff
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ and
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$. (The case where $!B$ is
inferred from $!A \land !B$ is handled similarly.)
\item The last inference is \Intro{\lor}: There are two variants: $!A
\lor !B$ may be inferred from the premise~$!A$ or the
premise~$!B$. Consider the first case. The !!{derivation} has the form
\begin{prooftree}
\AxiomC{$\Gamma$}
\RightLabel{$\delta_1$}
\DeduceC{$!A$}
\RightLabel{\Intro{\lor}}
\UnaryInfC{$!A \lor !B$}
\end{prooftree}
By inductive hypothesis, $!A$ follows from the !!{undischarged}
assumptions~$\Gamma$ of~$\delta_1$. Consider
\iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We
need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lor !B}$. Suppose
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$; then
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ since $\Gamma \Entails !A$ (the
inductive hypothesis). So it must also be the case that
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lor !B}$. (The case where $!A
\lor !B$ is inferred from~$!B$ is handled similarly.)
\item The last inference is \Intro{\lif}: $!A \lif !B$ is inferred
from a subproof with assumption~$!A$ and conclusion~$!B$, i.e.,
\begin{prooftree}
\AxiomC{$\Gamma, \Discharge{!A}{n}$}
\RightLabel{$\delta_1$}
\DeduceC{$!B$}
\DischargeRule{\Intro{\lif}}{n}
\UnaryInfC{$!A \lif !B$}
\end{prooftree}
By inductive hypothesis, $!B$ follows from the !!{undischarged}
assumptions of~$\delta_1$, i.e., $\Gamma \cup \{!A\} \Entails
!B$. Consider
\iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. The
!!{undischarged} assumptions of~$\delta$ are just $\Gamma$, since
$!A$ is discharged at the last inference. So we need to show that
$\Gamma \Entails !A \lif !B$. For reductio, suppose that for some
\iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$},
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$ but
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A \lif !B}$. So,
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ and
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$. But by hypothesis, $!B$ is a
consequence of $\Gamma \cup \{!A\}$, i.e.,
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$, which is a contradiction. So,
$\Gamma \Entails !A \lif !B$.
\item The last inference is \FalseInt: Here, $\delta$ ends in
\begin{prooftree}
\AxiomC{$\Gamma$}
\RightLabel{$\delta_1$}
\DeduceC{$\lfalse$}
\RightLabel{\FalseInt}
\UnaryInfC{$!A$}
\end{prooftree}
By induction hypothesis, $\Gamma \Entails \lfalse$. We have to show
that $\Gamma \Entails !A$. Suppose not; then for
some~$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ we have
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$ and
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A}$. But we always have
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lfalse}$, so this would mean
that $\Gamma \Entails/ \lfalse$, contrary to the induction
hypothesis.
\item The last inference is \FalseCl: Exercise.
\iftag{FOL}{
\item The last inference is \Intro{\lforall}: Then $\delta$ has the form
\begin{prooftree}
\AxiomC{$\Gamma$}
\RightLabel{$\delta_1$}
\DeduceC{$!A(a)$}
\RightLabel{\Intro{\lforall}}
\UnaryInfC{$\lforall[x][!A(x)]$}
\end{prooftree}
The premise $!A(a)$ is a consequence of the !!{undischarged}
assumptions $\Gamma$ by induction hypothesis. Consider some
structure, $\Struct{M}$, such that $\Sat{M}{\Gamma}$. We need to
show that $\Sat{M}{\lforall[x][!A(x)]}$. Since $\lforall[x][!A(x)]$
is !!a{sentence}, this means we have to show that for every variable
assignment~$s$, $\Sat{M}{!A(x)}[s]$
(\olref[syn][ass]{prop:sat-quant}). Since $\Gamma$ consists entirely
of sentences, $\Sat{M}{!B}[s]$ for all $!B \in \Gamma$ by
\olref[syn][sat]{defn:satisfaction}. Let $\Struct{M'}$ be like
$\Struct{M}$ except that $\Assign{a}{M'} = s(x)$. Since $a$ does
not occur in~$\Gamma$, $\Sat{M'}{\Gamma}$ by
\olref[syn][ext]{cor:extensionality-sent}. Since $\Gamma \Entails
!A(a)$, $\Sat{M'}{!A(a)}$. Since $!A(a)$ is !!a{sentence},
$\Sat{M'}{!A(a)}[s]$ by
\olref[syn][ass]{prop:sentence-sat-true}. $\Sat{M'}{!A(x)}[s]$ iff
$\Sat{M'}{!A(a)}$ by \olref[syn][ext]{prop:ext-formulas} (recall
that $!A(a)$ is just $\Subst{!A(x)}{a}{x}$). So,
$\Sat{M'}{!A(x)}[s]$. Since $a$ does not occur in~$!A(x)$, by
\olref[syn][ext]{prop:extensionality}, $\Sat{M}{!A(x)}[s]$. But $s$
was an arbitrary variable assignment, so
$\Sat{M}{\lforall[x][!A(x)]}$.
\item The last inference is \Intro{\lexists}: Exercise.
\item The last inference is \Elim{\forall}: Exercise.
}{}
\end{enumerate}
Now let's consider the possible inferences with several premises:
\Elim{\lor}, \Intro{\land}, \iftag{FOL}{\Elim{\lif}, and
\Elim{\lexists}}{and \Elim{\lif}}.
\begin{enumerate}
\item The last inference is \Intro{\land}. $!A \land !B$ is inferred
from the premises $!A$ and $!B$ and $\delta$ has the form
\begin{prooftree}
\AxiomC{$\Gamma_1$}
\RightLabel{$\delta_1$}
\DeduceC{$!A$}
\AxiomC{$\Gamma_2$}
\RightLabel{$\delta_2$}
\DeduceC{$!B$}
\RightLabel{\Intro{\land}}
\BinaryInfC{$!A \land !B$}
\end{prooftree}
By induction hypothesis, $!A$ follows from the !!{undischarged}
assumptions~$\Gamma_1$ of~$\delta_1$ and $!B$ follows from the
!!{undischarged} assumptions~$\Gamma_2$ of~$\delta_2$. The
!!{undischarged} assumptions of~$\delta$ are $\Gamma_1 \cup
\Gamma_2$, so we have to show that $\Gamma_1 \cup \Gamma_2 \Entails
!A \land !B$. Consider
\iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}
with $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup \Gamma_2}$. Since
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1}$, it must be the case that
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ as $\Gamma_1 \Entails !A$, and
since $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_2}$,
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ since $\Gamma_2 \Entails
!B$. Together, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$.
\item The last inference is \Elim{\lor}: Exercise.
\item The last inference is \Elim{\lif}. $!B$ is inferred from the
premises $!A \lif !B$ and~$!A$. The !!{derivation}~$\delta$ looks like this:
\begin{prooftree}
\AxiomC{$\Gamma_1$}
\RightLabel{$\delta_1$}
\DeduceC{$!A \lif !B$}
\AxiomC{$\Gamma_2$}
\RightLabel{$\delta_2$}
\DeduceC{$!A$}
\RightLabel{\Elim{\lif}}
\BinaryInfC{$!B$}
\end{prooftree}
By induction hypothesis, $!A \lif !B$ follows from the
!!{undischarged} assumptions~$\Gamma_1$ of~$\delta_1$ and $!A$
follows from the !!{undischarged} assumptions~$\Gamma_2$
of~$\delta_2$. Consider
\iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We
need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup
\Gamma_2}$, then $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$. Suppose
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup \Gamma_2}$. Since
$\Gamma_1 \Entails !A \lif !B$, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A
\lif !B}$. Since $\Gamma_2 \Entails !A$, we have
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. This means that
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ (For if
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$, since
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$, we'd have
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A \lif !B}$,
contradicting~$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lif !B}$).
\item The last inference is \Elim{\lnot}: Exercise.
\tagitem{FOL}{The last inference is \Elim{\lexists}: Exercise.}{}
\end{enumerate}
\end{proof}
\tagprob{FOL}
\begin{prob}
Complete the proof of \olref[fol][ntd][sou]{thm:soundness}.
\end{prob}
\tagendprob
\tagprob{notFOL}
\begin{prob}
Complete the proof of \olref[pl][ntd][sou]{thm:soundness}.
\end{prob}
\tagendprob
\begin{cor}
\ollabel{cor:weak-soundness}
If $\Proves !A$, then $!A$ is \iftag{FOL}{valid}{a tautology}.
\end{cor}
\begin{cor}
\ollabel{cor:consistency-soundness}
If $\Gamma$ is satisfiable, then it is consistent.
\end{cor}
\begin{proof}
We prove the contrapositive. Suppose that $\Gamma$ is not consistent.
Then $\Gamma \Proves \lfalse$, i.e., there is !!a{derivation} of
$\lfalse$ from !!{undischarged} assumptions in~$\Gamma$. By
\olref{thm:soundness}, any
\iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$}
that satisfies $\Gamma$ must satisfy $\lfalse$. Since
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lfalse}$ for every
\iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$},
no \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} can satisfy $\Gamma$,
i.e., $\Gamma$ is not satisfiable.
\end{proof}
\end{document}