The Sequent Calculus — Source and provenance

Source and provenance

All 10 files in the exact The Sequent Calculus source boundary appear line by line and are copied byte-for-byte for download. All 737 formulas link to exact source coordinates.

content/first-order-logic/sequent-calculus/sequent-calculus.tex

56 lines; SHA-256 8cbb6df83670a2586d10ef405c78ed4f75102f8d63903eef93e7ac2b8ea3b603. Open the preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
\documentclass[../../../include/open-logic-chapter]{subfiles}
\begin{document}
\iftag{FOL}
{\olchapter{fol}{seq}{The Sequent Calculus}}
{\olchapter{pl}{seq}{The Sequent Calculus}}
\begin{editorial}
This chapter presents Gentzen's standard sequent calculus LK for
classical first-order logic. It could use more examples and
exercises. To include or exclude material relevant to the sequent
calculus as a proof system, use the ``prfLK'' tag.
\end{editorial}
\olimport{rules-and-proofs}
\olimport{propositional-rules}
\iftag{FOL}{%
\olimport{quantifier-rules}
}{}
\olimport{structural-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/sequent-calculus/rules-and-proofs.tex

74 lines; SHA-256 a598b850cb425035d0c7a01b88bb491502c840fc76c2bd3dbe7e2dda5487d706. Open the preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: rules-and-proofs
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{seq}{rul}}
{\olfileid{pl}{seq}{rul}}
\olsection{Rules and \usetoken{P}{derivation}}
For the following, let $\Gamma, \Delta, \Pi, \Lambda$ represent finite
sequences of !!{sentence}s.
\begin{defn}[Sequent]
A \emph{sequent} is an expression of the form
\[
\Gamma \Sequent \Delta
\]
where $\Gamma$ and $\Delta$ are finite (possibly empty) sequences of
!!{sentence}s of the language $\Lang L$. $\Gamma$ is called the
\emph{antecedent}, while $\Delta$ is the \emph{succedent}.
\end{defn}
\begin{explain}
The intuitive idea behind a sequent is: if all of the !!{sentence}s in
the antecedent hold, then at least one of the !!{sentence}s in the
succedent holds. That is, if $\Gamma = \tuple{!A_1, \dots, !A_m}$ and
$\Delta = \tuple{!B_1, \dots, !B_n}$, then $\Gamma \Sequent \Delta$
holds iff
\[
(!A_1 \land \cdots \land !A_m) \lif (!B_1 \lor \cdots \lor
!B_n)
\]
holds. There are two special cases: where $\Gamma$ is empty and when
$\Delta$~is empty. When $\Gamma$ is empty, i.e., $m = 0$, $\quad
\Sequent \Delta$ holds iff $!B_1 \lor \dots \lor !B_n$ holds. When
$\Delta$ is empty, i.e., $n = 0$, $\Gamma \Sequent \quad$ holds iff
$\lnot(!A_1 \land \dots \land !A_m)$ does. We say a sequent is valid
iff the corresponding !!{sentence} is valid.
\end{explain}
If $\Gamma$ is a sequence of !!{sentence}s, we write $\Gamma, !A$ for
the result of appending $!A$ to the right end of~$\Gamma$ (and $!A,
\Gamma$ for the result of appending $!A$ to the left end
of~$\Gamma$). If $\Delta$ is a sequence of !!{sentence}s also, then $\Gamma,
\Delta$ is the concatenation of the two sequences.
\begin{defn}[Initial Sequent]
An \emph{initial sequent} is a sequent
\iftag{prvFalse,prvTrue}{of one of the following forms:
\begin{enumerate}
\item $!A \Sequent !A$
\tagitem{prvTrue}{$\quad \Sequent \ltrue$}{}
\tagitem{prvFalse}{$\lfalse \Sequent \quad$}{}
\end{enumerate}}
{of the form $!A \Sequent !A$} for any !!{sentence} $!A$ in the language.
\end{defn}
!!^{derivation}s in the sequent calculus are certain trees of
sequents, where the topmost sequents are initial sequents, and if a
sequent stands below one or two other sequents, it must follow
correctly by a rule of inference. The rules for $\Log{LK}$ are
divided into two main types: \emph{logical} rules and
\emph{structural} rules. The logical rules are named for the !!{main
operator} of the !!{sentence} containing $!A$ and/or $!B$ in the
lower sequent. Each one comes in two versions, one for inferring a
sequent with the !!{sentence} containing the !!{operator} on the left,
and one with the !!{sentence} on the right.
\end{document}

content/first-order-logic/sequent-calculus/propositional-rules.tex

88 lines; SHA-256 2a030e59a3a3156f61ff949e10a8a1470a0be80a419851fc56821aa458092ade. Open the preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: propositional-rules
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{seq}{prl}}
{\olfileid{pl}{seq}{prl}}
\olsection{Propositional Rules}
\subsection{Rules for $\lnot$}
\begin{defish}
\Axiom$ \Gamma \fCenter \Delta, !A $
\RightLabel{\LeftR{\lnot}}
\UnaryInf$ \lnot !A, \Gamma \fCenter \Delta$
\DisplayProof
\hfill
\Axiom$!A, \Gamma \fCenter \Delta$
\RightLabel{\RightR{\lnot}}
\UnaryInf$ \Gamma \fCenter \Delta, \lnot !A $
\DisplayProof
\end{defish}
\subsection{Rules for $\land$}
\begin{defish}\noindent
\begin{tabular}{l}
\Axiom$ !A, \Gamma \fCenter \Delta$
\RightLabel{\LeftR{\land}}
\UnaryInf$ !A \land !B, \Gamma \fCenter \Delta$
\DisplayProof
\\[3ex]
\Axiom$!B, \Gamma \fCenter \Delta$
\RightLabel{\LeftR{\land}}
\UnaryInf$!A \land !B, \Gamma \fCenter \Delta$
\DisplayProof
\end{tabular}
\hfill
\Axiom$\Gamma \fCenter \Delta, !A$
\Axiom$ \Gamma \fCenter \Delta, !B$
\RightLabel{\RightR{\land}}
\BinaryInf$ \Gamma \fCenter \Delta, !A \land !B $
\DisplayProof
\end{defish}
\subsection{Rules for $\lor$}
\begin{defish}
\Axiom$!A, \Gamma \fCenter \Delta$
\Axiom$!B, \Gamma \fCenter \Delta$
\RightLabel{\LeftR{\lor}}
\BinaryInf$!A \lor !B, \Gamma \fCenter \Delta$
\DisplayProof
\hfill
\begin{tabular}{r}
\Axiom$\Gamma \fCenter \Delta, !A$
\RightLabel{\RightR{\lor}}
\UnaryInf$ \Gamma \fCenter \Delta, !A \lor !B$
\DisplayProof
\\[3ex]
\Axiom$ \Gamma \fCenter \Delta, !B$
\RightLabel{\RightR{\lor}}
\UnaryInf$ \Gamma \fCenter \Delta, !A \lor !B$
\DisplayProof
\end{tabular}
\end{defish}
\subsection{Rules for $\lif$}
\begin{defish}
\Axiom$ \Gamma \fCenter \Delta, !A$
\Axiom$ !B, \Pi \fCenter \Lambda$
\RightLabel{\LeftR{\lif}}
\BinaryInf$ !A \lif !B, \Gamma, \Pi \fCenter \Delta, \Lambda$
\DisplayProof
\hfill
\Axiom$ !A, \Gamma \fCenter \Delta, !B$
\RightLabel{\RightR{\lif}}
\UnaryInf$ \Gamma \fCenter \Delta, !A \lif !B $
\DisplayProof
\end{defish}
\end{document}

content/first-order-logic/sequent-calculus/structural-rules.tex

80 lines; SHA-256 ea1ca77eca03ec566cc900b2399e95002b4cfc07eb3549a3f19da9ee23a09793. Open the preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: structural-rules
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{seq}{srl}}
{\olfileid{pl}{seq}{srl}}
\olsection{Structural Rules}
We also need a few rules that allow us to rearrange !!{sentence}s in
the left and right side of a sequent. Since the logical rules require
that the !!{sentence}s in the premise which the rule acts upon stand
either to the far left or to the far right, we need an ``exchange''
rule that allows us to move !!{sentence}s to the right position. It's
also important sometimes to be able to combine two identical
!!{sentence}s into one, and to add !!a{sentence} on either side.
\subsection{Weakening}
\begin{defish}
\Axiom$ \Gamma \fCenter \Delta $
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$ !A, \Gamma \fCenter \Delta$
\DisplayProof
\hfill
\Axiom$ \Gamma \fCenter \Delta$
\RightLabel{\RightR{\Weakening}}
\UnaryInf$ \Gamma \fCenter \Delta, !A$
\DisplayProof
\end{defish}
\subsection{Contraction}
\begin{defish}
\Axiom$ !A, !A, \Gamma \fCenter \Delta $
\RightLabel{\LeftR{\Contraction}}
\UnaryInf$ !A, \Gamma \fCenter \Delta$
\DisplayProof
\hfill
\Axiom$ \Gamma \fCenter \Delta, !A, !A$
\RightLabel{\RightR{\Contraction}}
\UnaryInf$ \Gamma \fCenter \Delta, !A$
\DisplayProof
\end{defish}
\subsection{Exchange}
\begin{defish}
\Axiom$ \Gamma, !A, !B, \Pi \fCenter \Delta $
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$ \Gamma, !B, !A, \Pi \fCenter \Delta$
\DisplayProof
\hfill
\Axiom$ \Gamma \fCenter \Delta, !A, !B, \Lambda$
\RightLabel{\RightR{\Exchange}}
\UnaryInf$ \Gamma \fCenter \Delta, !B, !A, \Lambda$
\DisplayProof
\end{defish}
A series of weakening, contraction, and exchange inferences will often
be indicated by double inference lines.
The following rule, called ``cut,'' is not strictly speaking
necessary, but makes it a lot easier to reuse and combine !!{derivation}s.
\begin{defish}
\[
\Axiom$ \Gamma \fCenter \Delta, !A$
\Axiom$ !A, \Pi \fCenter \Lambda $
\RightLabel{\Cut}
\BinaryInf$ \Gamma, \Pi \fCenter \Delta, \Lambda$
\DisplayProof
\]
\end{defish}
\end{document}

content/first-order-logic/sequent-calculus/derivations.tex

121 lines; SHA-256 0d47d6984b609f00edfec9acc49c85d33ac001609f10e5e501cbd96f3a5f63dd. Open the preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: derivations
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{seq}{der}}
{\olfileid{pl}{seq}{der}}
\olsection{\usetoken{P}{derivation}}
\begin{explain}
We've said what an initial sequent looks like, and we've given the
rules of inference. !!^{derivation}s in the sequent calculus are
inductively generated from these: each !!{derivation} either is an
initial sequent on its own, or consists of one or two !!{derivation}s
followed by an inference.
\end{explain}
\begin{defn}[$\Log{LK}$ !!{derivation}]
An \emph{$\Log{LK}$-!!{derivation}} of a sequent~$S$ is a finite tree
of sequents satisfying the following conditions:
\begin{enumerate}
\item The topmost sequents of the tree are initial sequents.
\item The bottommost sequent of the tree is~$S$.
\item Every sequent in the tree except $S$ is a premise of a correct
application of an inference rule whose conclusion stands directly
below that sequent in the tree.
\end{enumerate}
We then say that $S$ is the \emph{end-sequent} of the !!{derivation} and
that $S$ is \emph{!!{derivable} in $\Log{LK}$} (or $\Log{LK}$-!!{derivable}).
\end{defn}
\begin{ex}
Every initial sequent, e.g., $!C \Sequent !C$ is !!a{derivation}. We
can obtain a new !!{derivation} from this by applying, say, the
$\LeftR{\Weakening}$ rule,
\begin{prooftree}
\Axiom$ \Gamma \fCenter \Delta $
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$ !A, \Gamma \fCenter \Delta$
\end{prooftree}
The rule, however, is meant to be general: we can replace the $!A$ in
the rule with any !!{sentence}, e.g., also with~$!D$. If the premise
matches our initial sequent $!C \Sequent !C$, that means that both
$\Gamma$ and $\Delta$ are just~$!C$, and the conclusion would then be
$!D, !C \Sequent !C$. So, the following is !!a{derivation}:
\begin{prooftree}
\Axiom$ !C \fCenter !C $
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$ !D, !C \fCenter !C$
\end{prooftree}
We can now apply another rule, say $\LeftR{\Exchange}$, which allows
us to switch two !!{sentence}s on the left. So, the following is also
a correct !!{derivation}:
\begin{prooftree}
\Axiom$ !C \fCenter !C $
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$ !D, !C \fCenter !C$
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$ !C, !D \fCenter !C$
\end{prooftree}
In this application of the rule, which was given as
\begin{prooftree}
\Axiom$ \Gamma, !A, !B, \Pi \fCenter \Delta $
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$ \Gamma, !B, !A, \Pi \fCenter \Delta,$
\end{prooftree}
both $\Gamma$ and $\Pi$ were empty, $\Delta$ is $!C$, and the roles of
$!A$ and $!B$ are played by $!D$ and~$!C$, respectively. In much the
same way, we also see that
\begin{prooftree}
\Axiom$ !D \fCenter !D $
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$ !C, !D \fCenter !D$
\end{prooftree}
is !!a{derivation}. Now we can take these two !!{derivation}s, and combine
them using $\RightR{\land}$. That rule was
\begin{prooftree}
\Axiom$\Gamma \fCenter \Delta, !A$
\Axiom$ \Gamma \fCenter \Delta, !B$
\RightLabel{\RightR{\land}}
\BinaryInf$ \Gamma \fCenter \Delta, !A \land !B $
\end{prooftree}
In our case, the premises must match the last sequents of the
!!{derivation}s ending in the premises. That means that $\Gamma$ is
$!C, !D$, $\Delta$ is empty, $!A$ is $!C$ and $!B$ is $!D$. So the
conclusion, if the inference should be correct, is $!C, !D \Sequent !C
\land !D$.
\begin{prooftree}
\Axiom$ !C \fCenter !C $
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$ !D, !C \fCenter !C$
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$ !C, !D \fCenter !C$
\Axiom$ !D \fCenter !D $
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$ !C, !D \fCenter !D$
\RightLabel{\RightR{\land}}
\BinaryInf$ !C, !D \fCenter !C \land !D $
\end{prooftree}
Of course, we can also reverse the premises, then $!A$
would be $!D$ and $!B$ would be~$!C$.
\begin{prooftree}
\Axiom$ !D \fCenter !D $
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$ !C, !D \fCenter !D$
\Axiom$ !C \fCenter !C $
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$ !D, !C \fCenter !C$
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$ !C, !D \fCenter !C$
\RightLabel{\RightR{\land}}
\BinaryInf$ !C, !D \fCenter !D \land !C $
\end{prooftree}
\end{ex}
\end{document}

content/first-order-logic/sequent-calculus/proving-things.tex

342 lines; SHA-256 73fa9c16dcbd072ac535c251fa02fc78640b82381d57162817043a6ad578b18e. Open the preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: proving-things
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{seq}{pro}}
{\olfileid{pl}{seq}{pro}}
\olsection{Examples of \usetoken{P}{derivation}}
\begin{ex}
Give an $\Log{LK}$-!!{derivation} for the sequent $!A \land !B \Sequent !A$.
We begin by writing the desired end-sequent at the bottom of the
!!{derivation}.
\begin{prooftree}
\AxiomC{}
\UnaryInf$!A\land !B \fCenter !A$
\end{prooftree}
Next, we need to figure out what kind of inference could have a lower
sequent of this form. This could be a structural rule, but it is a
good idea to start by looking for a logical rule. The only logical
connective occurring in the lower sequent is $\land$,
so we're looking for an $\land$ rule, and since the $\land$ symbol
occurs in the antecedent, we're looking at the \LeftR{\land}
rule.
\begin{prooftree}
\AxiomC{}
\RightLabel{\LeftR{\land}}
\UnaryInf$!A\land !B \fCenter !A$
\end{prooftree}
There are two options for what could have been the upper sequent of
the \LeftR{\land} inference: we could have an upper sequent of $!A
\Sequent !A$, or of $!B \Sequent !A$. Clearly, $!A \Sequent !A$ is an
initial sequent (which is a good thing), while $!B \Sequent !A$ is not
derivable in general. We fill in the upper sequent:
\begin{prooftree}
\Axiom$!A \fCenter !A$
\RightLabel{\LeftR{\land}}
\UnaryInf$!A\land !B \fCenter !A$
\end{prooftree}
We now have a correct $\Log{LK}$-!!{derivation} of the sequent $!A
\land !B \Sequent !A$.
\end{ex}
\begin{ex}
Give an $\Log{LK}$-!!{derivation} for the sequent $\lnot !A \lor !B
\Sequent !A \lif !B$.
Begin by writing the desired end-sequent at the bottom of the !!{derivation}.
\begin{prooftree}
\AxiomC{}
\UnaryInf$\lnot !A \lor !B \fCenter !A \lif !B$
\end{prooftree}
To find a logical rule that could give us this end-sequent, we look at
the logical connectives in the end-sequent: $\lnot$, $\lor$, and
$\lif$. We only care at the moment about $\lor$ and $\lif$ because
they are !!{main operator}s of !!{sentence}s in the end-sequent,
while $\lnot$ is inside the scope of another connective, so we will
take care of it later. Our options for logical rules for the final
inference are therefore the \LeftR{\lor} rule and the \RightR{\lif}
rule. We could pick either rule, really, but let's pick the \RightR{\lif}
rule (if for no reason other than it allows us to put off
splitting into two branches). According to the form of \RightR{\lif}
inferences which can yield the lower sequent, this must look like:
\begin{prooftree}
\AxiomC{}
\UnaryInf$ !A, \lnot !A \lor !B \fCenter !B $
\RightLabel{\RightR{\lif}} \UnaryInf$ \lnot !A \lor !B \fCenter !A \lif !B $
\end{prooftree}
If we move $\lnot !A \lor !B$ to the outside of the antecedent, we can
apply the \LeftR{\lor} rule. According to the schema, this must split
into two upper sequents as follows:
\begin{prooftree}
\AxiomC{}
\UnaryInf$\lnot !A, !A \fCenter !B$
\AxiomC{}
\UnaryInf$!B, !A \fCenter !B$
\RightLabel{\LeftR{\lor}}
\BinaryInf$ \lnot !A \lor !B, !A \fCenter !B $
\RightLabel{\RightR{\Exchange}}
\UnaryInf$ !A, \lnot !A \lor !B \fCenter !B $
\RightLabel{\RightR{\lif}}
\UnaryInf$ \lnot !A \lor !B \fCenter !A \lif !B $
\end{prooftree}
Remember that we are trying to wind our way up to initial sequents; we
seem to be pretty close!{} The right branch is just one weakening and
one exchange away from an initial sequent and then it is done:
\begin{prooftree}
\AxiomC{}
\UnaryInf$\lnot !A, !A \fCenter !B$
\Axiom$!B \fCenter !B$
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$!A, !B \fCenter !B$
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$!B, !A \fCenter !B$
\RightLabel{\LeftR{\lor}}
\BinaryInf$\lnot !A \lor !B, !A \fCenter !B $
\RightLabel{\RightR{\Exchange}}
\UnaryInf$ !A, \lnot !A \lor !B \fCenter !B $
\RightLabel{\RightR{\lif}}
\UnaryInf$ \lnot !A \lor !B \fCenter !A \lif !B $
\end{prooftree}
Now looking at the left branch, the only logical connective in any
!!{sentence} is the $\lnot$ symbol in the antecedent !!{sentence}s, so
we're looking at an instance of the \LeftR{\lnot} rule.
\begin{prooftree}
\AxiomC{}
\UnaryInf$ !A \fCenter !B, !A$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$\lnot !A, !A \fCenter !B$
\Axiom$!B \fCenter !B$
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$!A, !B \fCenter !B$
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$!B, !A \fCenter !B$
\RightLabel{\LeftR{\lor}}
\BinaryInf$\lnot !A \lor !B, !A \fCenter !B $
\RightLabel{\RightR{\Exchange}}
\UnaryInf$ !A, \lnot !A \lor !B \fCenter !B $
\RightLabel{\RightR{\lif}}
\UnaryInf$ \lnot !A \lor !B \fCenter !A \lif !B $
\end{prooftree}
Similarly to how we finished off the right branch, we are just one
weakening and one exchange away from finishing off this left branch as well.
\begin{prooftree}
\Axiom$!A \fCenter !A$
\RightLabel{\RightR{\Weakening}}
\UnaryInf$ !A \fCenter !A, !B$
\RightLabel{\RightR{\Exchange}}
\UnaryInf$ !A \fCenter !B, !A$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$\lnot !A, !A \fCenter !B$
\Axiom$!B \fCenter !B$
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$!A, !B \fCenter !B$
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$!B, !A \fCenter !B$
\RightLabel{\LeftR{\lor}}
\BinaryInf$\lnot !A \lor !B, !A \fCenter !B $
\RightLabel{\RightR{\Exchange}}
\UnaryInf$ !A, \lnot !A \lor !B \fCenter !B $
\RightLabel{\RightR{\lif}}
\UnaryInf$ \lnot !A \lor !B \fCenter !A \lif !B $
\end{prooftree}
\end{ex}
\begin{ex}
Give an $\Log{LK}$-!!{derivation} of the sequent $\lnot !A \lor \lnot !B
\Sequent \lnot (!A \land !B)$
Using the techniques from above, we start by writing the desired
end-sequent at the bottom.
\begin{prooftree}
\AxiomC{}
\UnaryInf$ \lnot !A \lor \lnot !B \fCenter \lnot (!A \land !B) $
\end{prooftree}
The available main connectives of !!{sentence}s in the end-sequent are
the $\lor$ symbol and the $\lnot$ symbol. It would work to apply
either the \LeftR{\lor} or the \RightR{\lnot} rule here, but we start
with the \RightR{\lnot} rule because it avoids splitting up into two
branches for a moment:
\begin{prooftree}
\AxiomC{}
\UnaryInf$!A \land !B, \lnot !A \lor \lnot !B \fCenter $
\RightLabel{\RightR{\lnot}}
\UnaryInf$\lnot !A \lor \lnot !B \fCenter \lnot (!A \land !B)$
\end{prooftree}
Now we have a choice of whether to look at the \LeftR{\land} or the
\LeftR{\lor} rule. Let's see what happens when we apply the \LeftR{\land}
rule: we have a choice to start with either the sequent $!A,
\lnot !A \lor !B \Sequent \quad$ or the sequent $!B, \lnot !A
\lor !B \Sequent \quad$. Since the !!{derivation} is symmetric with
regards to $!A$ and $!B$, let's go with the former:
\begin{prooftree}
\AxiomC{}
\UnaryInf$!A, \lnot !A \lor \lnot !B \fCenter $
\RightLabel{\LeftR{\land}}
\UnaryInf$!A \land !B, \lnot !A \lor \lnot !B \fCenter $
\RightLabel{\RightR{\lnot}}
\UnaryInf$\lnot !A \lor \lnot !B \fCenter \lnot (!A \land !B)$
\end{prooftree}
Continuing to fill in the !!{derivation}, we see that we run into a problem:
\begin{prooftree}
\Axiom$!A \fCenter !A$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$ \lnot !A, !A \fCenter$
\AxiomC{}
\RightLabel{?}
\UnaryInf$!A \fCenter !B$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$ \lnot !B, !A \fCenter$
\RightLabel{\LeftR{\lor}}
\BinaryInf$\lnot !A \lor \lnot !B, !A \fCenter $
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$!A, \lnot !A \lor \lnot !B \fCenter $
\RightLabel{\LeftR{\land}}
\UnaryInf$!A \land !B, \lnot !A \lor \lnot !B \fCenter $
\RightLabel{\RightR{\lnot}}
\UnaryInf$\lnot !A \lor \lnot !B \fCenter \lnot (!A \land !B)$
\end{prooftree}
The top of the right branch cannot be reduced any further, and it
cannot be brought by way of structural inferences to an initial
sequent, so this is not the right path to take. So clearly, it was a
mistake to apply the \LeftR{\land} rule above. Going back to what we
had before and carrying out the \LeftR{\lor} rule instead, we get
\begin{prooftree}
\AxiomC{}
\UnaryInf$\lnot !A, !A \land !B \fCenter $
\AxiomC{}
\UnaryInf$\lnot !B, !A \land !B \fCenter $
\RightLabel{\LeftR{\lor}}
\BinaryInf$\lnot !A \lor \lnot !B, !A \land !B \fCenter $
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$!A \land !B, \lnot !A \lor \lnot !B \fCenter $
\RightLabel{\RightR{\lnot}}
\UnaryInf$\lnot !A \lor \lnot !B \fCenter \lnot (!A \land !B)$
\end{prooftree}
Completing each branch as we've done before, we get
\begin{prooftree}
\Axiom$ !A \fCenter!A$
\RightLabel{\LeftR{\land}}
\UnaryInf$!A \land !B \fCenter !A$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$\lnot !A, !A \land !B \fCenter $
\Axiom$ !B \fCenter !B$
\RightLabel{\LeftR{\land}}
\UnaryInf$!A \land !B \fCenter !B$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$\lnot !B, !A \land !B \fCenter $
\RightLabel{\LeftR{\lor}}
\BinaryInf$\lnot !A \lor \lnot !B, !A \land !B \fCenter $
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$!A \land !B, \lnot !A \lor \lnot !B \fCenter $
\RightLabel{\RightR{\lnot}}
\UnaryInf$\lnot !A \lor \lnot !B \fCenter \lnot (!A \land !B)$
\end{prooftree}
(We could have carried out the $\land$ rules lower than the $\lnot$
rules in these steps and still obtained a correct !!{derivation}).
\end{ex}
\begin{ex}
So far we haven't used the contraction rule, but it is sometimes
required. Here's an example where that happens. Suppose we want to
prove $\quad \Sequent !A \lor \lnot !A$. Applying $\RightR{\lor}$
backwards would give us one of these two !!{derivation}s:
\begin{prooftree}
\AxiomC{}
\UnaryInf$ \fCenter !A$
\RightLabel{\RightR{\lor}}
\UnaryInf$ \fCenter !A \lor \lnot !A$
\DisplayProof\qquad\bottomAlignProof
\AxiomC{}
\UnaryInf$!A \fCenter $
\RightLabel{\RightR{\lnot}}
\UnaryInf$ \fCenter \lnot !A$
\RightLabel{\RightR{\lor}}
\UnaryInf$ \fCenter !A \lor \lnot !A$
\end{prooftree}
Neither of these of course ends in an initial sequent. The trick is
to realize that the contraction rule allows us to combine two copies
of !!a{sentence} into one---and when we're searching for a proof,
i.e., going from bottom to top, we can keep a copy of $!A \lor \lnot
!A$ in the premise, e.g.,
\begin{prooftree}
\AxiomC{}
\UnaryInf$ \fCenter !A \lor \lnot !A, !A$
\RightLabel{\RightR{\lor}}
\UnaryInf$ \fCenter !A \lor \lnot !A, !A \lor \lnot !A$
\RightLabel{\RightR{\Contraction}}
\UnaryInf$ \fCenter !A \lor \lnot !A$
\end{prooftree}
Now we can apply $\RightR{\lor}$ a second time, and also get~$\lnot
!A$, which leads to a complete !!{derivation}.
\begin{prooftree}
\Axiom$!A \fCenter !A$
\RightLabel{\RightR{\lnot}}
\UnaryInf$\fCenter !A, \lnot !A$
\RightLabel{\RightR{\lor}}
\UnaryInf$\fCenter !A, !A \lor \lnot !A$
\RightLabel{\RightR{\Exchange}}
\UnaryInf$ \fCenter !A \lor \lnot !A, !A$
\RightLabel{\RightR{\lor}}
\UnaryInf$ \fCenter !A \lor \lnot !A, !A \lor \lnot !A$
\RightLabel{\RightR{\Contraction}}
\UnaryInf$ \fCenter !A \lor \lnot !A$
\end{prooftree}
\end{ex}
\begin{prob}
Give !!{derivation}s of the following sequents:
\begin{enumerate}
\item $!A \land (!B \land !C) \Sequent (!A \land !B) \land !C$.
\item $!A \lor (!B \lor !C) \Sequent (!A \lor !B) \lor !C$.
\item $!A \lif (!B \lif !C) \Sequent !B \lif (!A \lif !C)$.
\item $!A \Sequent \lnot\lnot !A$.
\end{enumerate}
\end{prob}
\begin{prob}
Give !!{derivation}s of the following sequents:
\begin{enumerate}
\item $(!A \lor !B) \lif !C \Sequent !A \lif !C$.
\item $(!A \lif !C) \land (!B \lif !C) \Sequent (!A \lor !B) \lif !C$.
\item $\Sequent \lnot(!A \land \lnot !A)$.
\item $!B \lif !A \Sequent \lnot !A \lif \lnot !B$.
\item $\Sequent (!A \lif \lnot !A) \lif \lnot !A$.
\item $\Sequent \lnot(!A \lif !B) \lif \lnot !B$.
\item $!A \lif !C \Sequent \lnot (!A \land \lnot !C)$.
\item $!A \land \lnot !C \Sequent \lnot (!A \lif !C)$.
\item $!A \lor !B, \lnot !B \Sequent !A$.
\item $\lnot !A \lor \lnot !B \Sequent \lnot(!A \land !B)$.
\item $\Sequent (\lnot !A \land \lnot !B) \lif\lnot(!A \lor !B)$.
\item $\Sequent \lnot(!A \lor !B) \lif (\lnot !A \land \lnot !B)$.
\end{enumerate}
\end{prob}
\begin{prob}
Give !!{derivation}s of the following sequents:
\begin{enumerate}
\item $\lnot(!A \lif !B) \Sequent !A$.
\item $\lnot(!A \land !B) \Sequent \lnot !A \lor \lnot !B$.
\item $!A \lif !B \Sequent \lnot !A \lor !B$.
\item $\Sequent \lnot \lnot !A \lif !A$.
\item $!A \lif !B, \lnot !A \lif !B \Sequent !B$.
\item $(!A \land !B) \lif !C \Sequent (!A \lif !C) \lor (!B \lif !C)$.
\item $(!A \lif !B) \lif !A \Sequent !A$.
\item $\Sequent (!A \lif !B) \lor (!B \lif !C)$.
\end{enumerate}
(These all require the $\RightR{\Contraction}$~rule.)
\end{prob}
\end{document}

content/first-order-logic/sequent-calculus/proof-theoretic-notions.tex

170 lines; SHA-256 aea2dd5d73394a3cd97b72ada3e7d21aac0113cc4d995b54196a5506b1fa5a81. Open the preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: proof-theoretic-notions
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\begin{editorial}
This section collects the definitions of the provability relation and
consistency for natural deduction.
\end{editorial}
\iftag{FOL}
{\olfileid{fol}{seq}{ptn}}
{\olfileid{pl}{seq}{ptn}}
\olsection{Proof-Theoretic Notions}
\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 sequents. It was
an important discovery that these notions coincide. That they do is
the content of the \emph{soundness} and \emph{completeness theorem}.
\end{explain}
\begin{defn}[Theorems]
!!^a{sentence}~$!A$ is a \emph{theorem} if there is !!a{derivation}
in~$\Log{LK}$ of the sequent $\quad \Sequent !A$. 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$, iff there is a
finite subset~$\Gamma_0 \subseteq \Gamma$ and a sequence $\Gamma_0'$
of the !!{sentence}s in~$\Gamma_0$ such that $\Log{LK}$ !!{derive}s
$\Gamma_0' \Sequent !A$. If $!A$ is not !!{derivable} from $\Gamma$
we write $\Gamma \Proves/ !A$.
\end{defn}
Because of the contraction, weakening, and exchange rules, the order
and number of !!{sentence}s in~$\Gamma_0'$ does not matter: if a
sequent $\Gamma_0' \Sequent !A$ is !!{derivable}, then so is
$\Gamma_0'' \Sequent !A$ for any $\Gamma_0''$ that contains the same
!!{sentence}s as~$\Gamma_0'$. For instance, if $\Gamma_0 = \{!B, !C\}$
then both $\Gamma_0' = \tuple{!B, !B, !C}$ and $\Gamma_0'' =
\tuple{!C, !C, !B}$ are sequences containing just the !!{sentence}s
in~$\Gamma_0$. If a sequent containing one is !!{derivable}, so is the
other, e.g.:
\begin{prooftree}
\AxiomC{}
\Deduce$!B, !B, !C \fCenter !A$
\RightLabel{\LeftR{\Contraction}}
\UnaryInf$!B, !C \fCenter !A$
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$!C, !B \fCenter !A$
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$!C, !C, !B \fCenter !A$
\end{prooftree}
From now on we'll say that if $\Gamma_0$ is a finite set of
!!{sentence}s then $\Gamma_0 \Sequent !A$ is any sequent where the
antecedent is a sequence of !!{sentence}s in~$\Gamma_0$ and tacitly include
contractions, exchanges, and weakenings if necessary.
\begin{defn}[Consistency]
A set of sentences~$\Gamma$ is \emph{inconsistent} iff there is a
finite subset~$\Gamma_0 \subseteq \Gamma$ such that $\Log{LK}$
!!{derive}s $\Gamma_0 \Sequent \quad$. If $\Gamma$ is not
inconsistent, i.e., if for every finite $\Gamma_0 \subseteq \Gamma$,
$\Log{LK}$ does not !!{derive} $\Gamma_0 \Sequent \quad$, 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 initial sequent $!A \Sequent !A$ is !!{derivable}, and $\{!A\}
\subseteq \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}
Suppose $\Gamma \Proves !A$, i.e., there is a finite $\Gamma_0
\subseteq \Gamma$ such that $\Gamma_0 \Sequent !A$ is
!!{derivable}. Since $\Gamma \subseteq \Delta$, then $\Gamma_0$ is
also a finite subset of~$\Delta$. The !!{derivation} of $\Gamma_0
\Sequent !A$ thus also shows $\Delta \Proves !A$.
\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 finite $\Gamma_0 \subseteq \Gamma$
and !!a{derivation}~$\pi_0$ of $\Gamma_0 \Sequent !A$. If $\{!A\}
\cup \Delta \Proves !B$, then for some finite subset $\Delta_0
\subseteq \Delta$, there is !!a{derivation}~$\pi_1$ of $!A, \Delta_0
\Sequent !B$. Consider the following !!{derivation}:
\begin{prooftree}
\AxiomC{}
\RightLabel{$\pi_0$}
\Deduce$\Gamma_0 \fCenter !A$
\AxiomC{}
\RightLabel{$\pi_1$}
\Deduce$!A, \Delta_0 \fCenter !B$
\RightLabel{\Cut}
\BinaryInf$\Gamma_0, \Delta_0 \fCenter !B$
\end{prooftree}
Since $\Gamma_0 \cup \Delta_0 \subseteq \Gamma \cup \Delta$, this
shows $\Gamma \cup \Delta \Proves !B$.
\end{proof}
Note that this means that in particular 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}
$\Gamma$ is inconsistent iff $\Gamma \Proves {!A}$ for every
sentence~$!A$.
\end{prop}
\begin{proof}
Exercise.
\end{proof}
\begin{prob}
Prove \olref[fol][seq][ptn]{prop:incons}
\end{prob}
\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 finite subset
$\Gamma_0 \subseteq \Gamma$ such that the sequent $\Gamma_0
\Sequent !A$ has !!a{derivation}. Consequently, $\Gamma_0
\Proves !A$.
\item If $\Gamma$ is inconsistent, there is a finite
subset~$\Gamma_0 \subseteq \Gamma$ such that $\Log{LK}$
!!{derive}s $\Gamma_0 \Sequent \quad$. But then $\Gamma_0$ is a
finite subset of~$\Gamma$ that is inconsistent.
\end{enumerate}
\end{proof}
\end{document}

content/first-order-logic/sequent-calculus/provability-consistency.tex

127 lines; SHA-256 3e784d39f38d393203a7623b34e8fcad64e3299c102ee2ef96a812b5e6c8c229. Open the preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: provability-consistency
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{seq}{prv}}
{\olfileid{pl}{seq}{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}
There are finite $\Gamma_0$ and $\Gamma_1 \subseteq \Gamma$ such that
$\Log{LK}$ !!{derive}s $\Gamma_0 \Sequent !A$ and $!A, \Gamma_1
\Sequent \quad$. Let the $\Log{LK}$-!!{derivation} of $\Gamma_0 \Sequent
!A$ be~$\pi_0$ and the $\Log{LK}$-!!{derivation} of $\Gamma_1, !A
\Sequent \quad$ be~$\pi_1$. We can then !!{derive}
\begin{prooftree}
\AxiomC{}
\RightLabel{$\pi_0$}
\Deduce$ \Gamma_0 \fCenter !A $
\AxiomC{}
\RightLabel{$\pi_1$}
\Deduce$!A, \Gamma_1 \fCenter $
\RightLabel{\Cut}
\BinaryInf$ \Gamma_0,\Gamma_1 \fCenter $
\end{prooftree}
Since $\Gamma_0 \subseteq \Gamma$ and $\Gamma_1 \subseteq \Gamma$,
$\Gamma_0 \cup \Gamma_1 \subseteq \Gamma$, hence $\Gamma$~is inconsistent.
\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}~$\pi_0$ of $\Gamma \Sequent !A$. By adding a
$\LeftR{\lnot}$ rule, we obtain !!a{derivation} of~$\lnot !A, \Gamma
\Sequent \quad$, i.e., $\Gamma \cup \{\lnot !A\}$ is inconsistent.
If $\Gamma \cup \{\lnot !A\}$ is inconsistent, there is
!!a{derivation}~$\pi_1$ of $\lnot !A, \Gamma \Sequent \quad$. The
following is !!a{derivation} of $\Gamma \Sequent !A$:
\begin{prooftree}
\Axiom$!A \fCenter !A$
\RightLabel{\RightR{\lnot}}
\UnaryInf$\fCenter !A, \lnot !A$
\AxiomC{}
\RightLabel{$\pi_1$}
\Deduce$\lnot !A, \Gamma \fCenter$
\RightLabel{\Cut}
\BinaryInf$\Gamma \fCenter !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}~$\pi$ of a sequent $\Gamma_0 \Sequent !A$. The
sequent $\lnot !A, \Gamma_0 \Sequent \quad$ is also !!{derivable}:
\begin{prooftree}
\AxiomC{}
\RightLabel{$\pi$}
\Deduce$\Gamma_0 \fCenter !A$
\Axiom$!A \fCenter !A$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$\lnot !A, !A \fCenter$
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$!A, \lnot !A \fCenter$
\RightLabel{\Cut}
\BinaryInf$\Gamma_0, \lnot !A \fCenter$
\end{prooftree}
Since $\lnot !A \in \Gamma$ and $\Gamma_0 \subseteq \Gamma$, this
shows that $\Gamma$ is inconsistent.
\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 finite sets $\Gamma_0 \subseteq \Gamma$ and $\Gamma_1
\subseteq \Gamma$ and $\Log{LK}$-!!{derivation}s $\pi_0$ and $\pi_1$
of $!A, \Gamma_0 \Sequent \quad$ and $\lnot !A, \Gamma_1 \Sequent
\quad$, respectively. We can then !!{derive}
\begin{prooftree}
\AxiomC{}
\RightLabel{$\pi_0$}
\Deduce$ !A, \Gamma_0 \fCenter $
\RightLabel{\RightR{\lnot}}
\UnaryInf$ \Gamma_0 \fCenter \lnot !A$
\AxiomC{}
\RightLabel{$\pi_1$}
\Deduce$\lnot !A, \Gamma_1 \fCenter $
\RightLabel{\Cut}
\BinaryInf$ \Gamma_0, \Gamma_1 \fCenter $
\end{prooftree}
Since $\Gamma_0 \subseteq \Gamma$ and $\Gamma_1 \subseteq \Gamma$,
$\Gamma_0 \cup \Gamma_1 \subseteq \Gamma$. Hence $\Gamma$ is
inconsistent.
\end{proof}
\end{document}

content/first-order-logic/sequent-calculus/provability-propositional.tex

138 lines; SHA-256 13dd017159225b5fc9bcaa38c927fda407264d59c1305ebfd49329a85f5b9fa8. Open the preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% 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}{seq}{ppr}}
{\olfileid{pl}{seq}{ppr}}
\olsection{\usetoken{S}{derivability} and the Propositional Connectives}
\begin{explain}
We establish that the !!{derivability} relation~$\Proves$ of the
sequent calculus 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 Both sequents $!A \land !B \Sequent !A$ and $!A \land !B \Sequent
!B$ are !!{derivable}:
\begin{prooftree}
\Axiom$!A \fCenter !A$
\RightLabel{\LeftR{\land}}
\UnaryInf$!A \land !B \fCenter !A$
\DisplayProof\qquad\bottomAlignProof
\Axiom$!B \fCenter !B$
\RightLabel{\LeftR{\land}}
\UnaryInf$!A \land !B \fCenter !B$
\end{prooftree}
\item Here is !!a{derivation} of the sequent $!A, !B \Sequent !A \land !B$:
\begin{prooftree}
\Axiom$!A \fCenter !A$
\Axiom$!B \fCenter !B$
\RightLabel{\RightR{\land}}
\BinaryInf$!A, !B \fCenter !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 We give !!a{derivation} of the sequent $!A \lor !B, \lnot !A,
\lnot !B \Sequent$:
\begin{prooftree}
\Axiom$!A \fCenter !A$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$\lnot !A, !A \fCenter$
\doubleLine
\UnaryInf$!A, \lnot !A, \lnot !B \fCenter$
\Axiom$!B \fCenter !B$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$\lnot !B, !B \fCenter$
\doubleLine
\UnaryInf$!B, \lnot !A, \lnot !B \fCenter$
\RightLabel{\LeftR{\lor}}
\BinaryInf$ !A \lor !B, \lnot !A, \lnot !B \fCenter $
\end{prooftree}
(Recall that double inference lines indicate several weakening,
contraction, and exchange inferences.)
\item Both sequents $!A \Sequent !A \lor !B$ and $!B \Sequent !A
\lor !B$ have !!{derivation}s:
\begin{prooftree}
\Axiom$!A \fCenter !A$
\RightLabel{\RightR{\lor}}
\UnaryInf$!A \fCenter !A \lor !B$
\DisplayProof\qquad\bottomAlignProof
\Axiom$!B \fCenter !B$
\RightLabel{\RightR{\lor}}
\UnaryInf$!B \fCenter !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 The sequent $!A \lif !B, !A \Sequent !B$ is !!{derivable}:
\begin{prooftree}
\Axiom$!A \fCenter !A$
\Axiom$!B \fCenter !B$
\RightLabel{\LeftR{\lif}}
\BinaryInf$!A \lif !B, !A \fCenter !B$
\end{prooftree}
\item Both sequents $\lnot !A \Sequent !A \lif !B$ and $!B
\Sequent !A \lif !B$ are !!{derivable}:
\begin{prooftree}
\Axiom$!A \fCenter !A$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$\lnot !A, !A \fCenter$
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$!A, \lnot !A \fCenter$
\RightLabel{\RightR{\Weakening}}
\UnaryInf$!A, \lnot !A \fCenter !B$
\RightLabel{\RightR{\lif}}
\UnaryInf$\lnot !A \fCenter !A \lif !B$
\DisplayProof\qquad\bottomAlignProof
\Axiom$!B \fCenter !B$
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$!A, !B \fCenter !B$
\RightLabel{\RightR{\lif}}
\UnaryInf$!B \fCenter !A \lif !B$
\end{prooftree}
\end{enumerate}
\end{proof}
\end{document}

content/first-order-logic/sequent-calculus/soundness.tex

384 lines; SHA-256 d9f6180bee35f29553144b6eca5a1eb1916e0262dcdc8c30f50193a53d8001fa. Open the preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: soundness.tex
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{seq}{sou}}
{\olfileid{pl}{seq}{sou}}
\olsection{Soundness}
\begin{explain}
!!^a{derivation} system, such as the sequent calculus, is \emph{sound}
if it cannot !!{derive} things that do not actually hold. 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}~$!A$ 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.
Because all these proof-theoretic properties are defined via
!!{derivability} in the sequent calculus of certain sequents, proving
(1)--(3) above requires proving something about the semantic
properties of !!{derivable} sequents. We will first define what it
means for a sequent to be \emph{valid}, and then show that every
!!{derivable} sequent is valid. (1)--(3) then follow as corollaries
from this result.
\end{explain}
\begin{defn}
\iftag{FOL}{!!^a{structure}~$\Struct
M$}{!!^a{valuation}~$\pAssign{v}$} \emph{satisfies} a sequent
$\Gamma \Sequent \Delta$ iff either
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A}$ for some $!A \in \Gamma$ or
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ for some $!A \in \Delta$.
A sequent is \emph{valid} iff every \iftag{FOL}{!!{structure}~$\Struct
M$}{!!{valuation}~$\pAssign{v}$} satisfies it.
\end{defn}
\begin{thm}[Soundness]
\ollabel{thm:sequent-soundness} If $\Log{LK}$ !!{derive}s $\Theta
\Sequent \Xi$, then $\Theta \Sequent \Xi$ is valid.
\end{thm}
\begin{proof}
Let $\pi$ be !!a{derivation} of $\Theta \Sequent \Xi$. We proceed by
induction on the number of inferences~$n$ in~$\pi$.
If the number of inferences is~$0$, then $\pi$ consists only of an
initial sequent. Every initial sequent $!A \Sequent !A$ is obviously
valid, since for every \iftag{FOL}{$\Struct M$}{$\pAssign{v}$}, either
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A}$ or
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$.
If the number of inferences is greater than~0, we distinguish cases
according to the type of the lowermost inference. By induction
hypothesis, we can assume that the premises of that inference are
valid, since the number of inferences in the !!{derivation} of any premise is
smaller than~$n$.
First, we consider the possible inferences with only one premise.
\begin{enumerate}
\item The last inference is a weakening. Then $\Theta \Sequent \Xi$
is either $!A, \Gamma \Sequent \Delta$ (if the last inference is
\LeftR{\Weakening}) or $\Gamma \Sequent \Delta, !A$ (if it's
\RightR{\Weakening}), and the !!{derivation} ends in one of
\begin{prooftree}
\AxiomC{}
\Deduce$\Gamma \fCenter \Delta$
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$!A, \Gamma \fCenter \Delta$
\DisplayProof\qquad\bottomAlignProof
\AxiomC{}
\Deduce$\Gamma \fCenter \Delta$
\RightLabel{\RightR{\Weakening}}
\UnaryInf$\Gamma \fCenter \Delta, !A$
\end{prooftree}
By induction hypothesis, $\Gamma \Sequent \Delta$ is valid, i.e.,
for every
\iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$},
either there is some $!C \in \Gamma$ such that
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$ or there is some $!C \in
\Delta$ such that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$.
If $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$ for some $!C \in \Gamma$,
then $!C \in \Theta$ as well since $\Theta = !A, \Gamma$, and so
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$ for some $!C \in \Theta$.
Similarly, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$ for some $!C \in
\Delta$, as $!C \in \Xi$, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$ for
some $!C \in \Xi$. Consequently, $\Theta \Sequent \Xi$ is valid.
\item The last inference is \LeftR{\lnot}: Then the premise of the
last inference is $\Gamma \Sequent \Delta, !A$ and the conclusion is
$\lnot !A, \Gamma \Sequent \Delta$, i.e., the !!{derivation} ends in
\begin{prooftree}
\AxiomC{}
\Deduce$\Gamma \fCenter \Delta, !A$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$\lnot !A, \Gamma \fCenter \Delta$
\end{prooftree}
and $\Theta = \lnot !A, \Gamma$ while $\Xi = \Delta$.
The induction hypothesis tells us that $\Gamma \Sequent \Delta, !A$
is valid, i.e., for every \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$},
either (a) for some $!C \in \Gamma$,
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$, or (b) for some $!C \in
\Delta$, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$, or (c)
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. We want to show that $\Theta
\Sequent \Xi$ is also valid. Let \iftag{FOL}{$\Struct{M}$ be
!!a{structure}}{$\pAssign{v}$ be !!a{valuation}}. If (a) holds,
then there is $!C \in \Gamma$ so that
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$, but $!C \in \Theta$ as
well. If (b) holds, there is $!C \in \Delta$ such that
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$, but $!C \in \Xi$ as
well. Finally, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$, then
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lnot !A}$. Since $\lnot !A \in
\Theta$, there is $!C \in \Theta$ such that
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$. Consequently, $\Theta
\Sequent \Xi$ is valid.
\item The last inference is \RightR{\lnot}: Exercise.
\item The last inference is \LeftR{\land}: There are two variants: $!A
\land !B$ may be inferred on the left from $!A$ or from $!B$ on the
left side of the premise. In the first case, the $\pi$ ends in
\begin{prooftree}
\AxiomC{}
\Deduce$!A, \Gamma \fCenter \Delta$
\RightLabel{\LeftR{\land}}
\UnaryInf$!A \land !B, \Gamma \fCenter \Delta$
\end{prooftree}
and $\Theta = !A \land !B, \Gamma$ while $\Xi = \Delta$. Consider
\iftag{FOL}{!!a{structure}~$\Struct
M$}{!!a{valuation}~$\pAssign{v}$}. Since by induction hypothesis,
$!A, \Gamma \Sequent \Delta$ is valid, (a)
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A}$, (b)
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$ for some $!C \in \Gamma$, or
(c)~$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$ for some $!C \in \Delta$.
In case (a), $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A \land !B}$, so
there is $!C \in \Theta$ (namely, $!A \land !B$) such that
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$. In case (b), there is $!C
\in \Gamma$ such that $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$, and
$!C \in \Theta$ as well. In case (c), there is $!C \in \Delta$ such
that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$, and $!C \in \Xi$ as well
since $\Xi = \Delta$. So in each case, \iftag{FOL}{$\Struct
M$}{$\pAssign{v}$} satisfies $!A \land !B, \Gamma \Sequent
\Delta$. Since \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} was
arbitrary, $\Gamma \Sequent \Delta$ is valid. The case where $!A
\land !B$ is inferred from $!B$ is handled the same, changing $!A$
to $!B$.
\item The last inference is \RightR{\lor}: There are two variants: $!A
\lor !B$ may be inferred on the right from $!A$ or from $!B$ on the
right side of the premise. In the first case, $\pi$ ends in
\begin{prooftree}
\AxiomC{}
\Deduce$\Gamma \fCenter \Delta, !A$
\RightLabel{\RightR{\lor}}
\UnaryInf$\Gamma \fCenter \Delta, !A \lor !B$
\end{prooftree}
Now $\Theta = \Gamma$ and $\Xi = \Delta, !A \lor !B$. Consider
\iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}.
Since $\Gamma \Sequent \Delta, !A$ is valid, (a)
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$, (b)
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$ for some $!C \in \Gamma$, or
(c)~$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$ for some $!C \in \Delta$.
In case (a), $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lor !B}$. In case
(b), there is $!C \in \Gamma$ such that
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$. In case (c), there is $!C
\in \Delta$ such that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$. So in
each case, \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} satisfies
$\Gamma \Sequent \Delta, !A \lor !B$, i.e., $\Theta \Sequent \Xi$.
Since \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} was arbitrary,
$\Theta \Sequent \Xi$ is valid. The case where $!A \lor !B$ is
inferred from $!B$ is handled the same, changing $!A$ to $!B$.
\item The last inference is \RightR{\lif}: Then $\pi$ ends in
\begin{prooftree}
\AxiomC{}
\Deduce$!A, \Gamma \fCenter \Delta, !B$
\RightLabel{\RightR{\lif}}
\UnaryInf$\Gamma \fCenter \Delta, !A \lif !B$
\end{prooftree}
Again, the induction hypothesis says that the premise is valid; we
want to show that the conclusion is valid as well. Let
\iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} be arbitrary. Since $!A,
\Gamma \Sequent \Delta, !B$ is valid, at least one of the following
cases obtains: (a) $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A}$, (b)
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$, (c)
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$ for some~$~!C \in \Gamma$, or
(d) $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$ for some $!C \in \Delta$.
In cases (a) and (b), $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lif !B}$
and so there is a $!C \in \Delta, !A \lif !B$ such that
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$. In case (c), for some $!C \in
\Gamma$, $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$. In case (d), for
some $!C \in \Delta$, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$. In each
case, \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} satisfies $\Gamma
\Sequent \Delta, !A \lif !B$. Since
\iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} was arbitrary, $\Gamma
\Sequent \Delta, !A \lif !B$ is valid. \iftag{FOL}{%
\item The last inference is \LeftR{\lforall}: Then there is
!!a{formula}~$!A(x)$ and a closed term~$t$ such that $\pi$ ends in
\begin{prooftree}
\AxiomC{}
\Deduce$!A(t), \Gamma \fCenter \Delta$
\RightLabel{\LeftR{\lforall}}
\UnaryInf$\lforall[x][!A(x)], \Gamma \fCenter \Delta$
\end{prooftree}
We want to show that the conclusion $\lforall[x][!A(x)], \Gamma
\Sequent \Delta$ is valid. Consider !!a{structure}~$\Struct M$.
Since the premise $!A(t), \Gamma \Sequent \Delta$ is valid, (a)
$\Sat/{M}{!A(t)}$, (b) $\Sat/{M}{!C}$ for some $!C \in \Gamma$, or
(c)~$\Sat{M}{!C}$ for some $!C \in \Delta$. In case (a), by
\olref[syn][sem]{prop:quant-terms}, if
$\Sat{M}{\lforall[x][!A(x)]}$, then $\Sat{M}{!A(t)}$. Since
$\Sat/{M}{!A(t)}$, $\Sat/{M}{\lforall[x][!A(x)]}$ . In case (b) and
(c), $\Struct{M}$ also satisfies $\lforall[x][!A(x)], \Gamma
\Sequent \Delta$. Since $\Struct M$ was arbitrary,
$\lforall[x][!A(x)], \Gamma \Sequent \Delta$ is valid.
\item The last inference is \RightR{\lexists}: Exercise.
\item The last inference is \RightR{\lforall}: Then there is
!!a{formula}~$!A(x)$ and !!a{constant}~$a$ such that $\pi$ ends in
\begin{prooftree}
\AxiomC{}
\Deduce$\Gamma \fCenter \Delta, !A(a)$
\RightLabel{\RightR{\lforall}}
\UnaryInf$\Gamma \fCenter \Delta, \lforall[x][!A(x)]$
\end{prooftree}
where the eigenvariable condition is satisfied, i.e., $a$ does not
occur in $!A(x)$, $\Gamma$, or $\Delta$. By induction hypothesis,
the premise of the last inference is valid. We have to show that
the conclusion is valid as well, i.e., that for any
!!{structure}~$\Struct M$, (a) $\Sat{M}{\lforall[x][!A(x)]}$, (b)
$\Sat/{M}{!C}$ for some $!C \in \Gamma$, or (c)~$\Sat{M}{!C}$ for
some $!C \in \Delta$.
Suppose $\Struct{M}$ is an arbitrary !!{structure}. If (b) or (c)
holds, we are done, so suppose neither holds: for all $!C \in
\Gamma$, $\Sat{M}{!C}$, and for all $!C \in \Delta$,
$\Sat/{M}{!C}$. We have to show that (a) holds, i.e.,
$\Sat{M}{\lforall[x][!A(x)]}$. By
\olref[syn][ass]{prop:sat-quant}, if suffices to show that
$\Sat{M}{!A(x)}[s]$ for all variable assignments~$s$. So let $s$ be
an arbitrary variable assignment. Consider the
structure~$\Struct{M'}$ which is just like~$\Struct{M}$ except
$\Assign{a}{M'} = s(x)$. By
\olref[syn][ext]{cor:extensionality-sent}, for any $!C \in \Gamma$,
$\Sat{M'}{!C}$ since $a$ does not occur in~$\Gamma$, and for any
$!C \in \Delta$, $\Sat/{M'}{!C}$. But the premise is valid, so
$\Sat{M'}{!A(a)}$. By \olref[syn][ass]{prop:sentence-sat-true},
$\Sat{M'}{!A(a)}[s]$, since $!A(a)$ is a sentence. Now $\varAssign{s}{s}{x}$
with $s(x) = \Value{a}{M'}[s]$, since we've defined $\Struct{M'}$ in
just this way. So \olref[syn][ext]{prop:ext-formulas} applies, and
we get $\Sat{M'}{!A(x)}[s]$. Since $a$ does not occur in~$!A(x)$, by
\olref[syn][ext]{prop:extensionality}, $\Sat{M}{!A(x)}[s]$. Since
$s$ was arbitrary, we've completed the proof that
$\Sat{M}{!A(x)}[s]$ for all variable assignments.
\item The last inference is \LeftR{\lexists}: Exercise.
}{}
\end{enumerate}
Now let's consider the possible inferences with two premises.
\begin{enumerate}
\item The last inference is a cut: then $\pi$ ends in
\begin{prooftree}
\AxiomC{}
\Deduce$\Gamma \fCenter \Delta, !A$
\AxiomC{}
\Deduce$!A, \Pi \fCenter \Lambda$
\RightLabel{\Cut}
\BinaryInf$\Gamma, \Pi \fCenter \Delta, \Lambda$
\end{prooftree}
Let \iftag{FOL}{$\Struct{M}$ be !!a{structure}}{$\pAssign{v}$ be
!!a{valuation}}. By induction hypothesis, the premises are valid,
so \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} satisfies both premises.
We distinguish two cases: (a) $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A}$
and (b) $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. In case (a), in order
for \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} to satisfy the left
premise, it must satisfy $\Gamma \Sequent \Delta$. But then it also
satisfies the conclusion. In case (b), in order for
\iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} to satisfy the right
premise, it must satisfy $\Pi \setminus \Lambda$. Again,
\iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} satisfies the conclusion.
\item The last inference is \RightR{\land}. Then $\pi$ ends in
\begin{prooftree}
\AxiomC{}
\Deduce$\Gamma \fCenter \Delta, !A$
\AxiomC{}
\Deduce$\Gamma \fCenter \Delta, !B$
\RightLabel{\RightR{\land}}
\BinaryInf$\Gamma \fCenter \Delta, !A \land !B$
\end{prooftree}
Consider \iftag{FOL}{!!a{structure}~$\Struct
M$}{!!a{valuation}~$\pAssign{v}$}. If
\iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} satisfies $\Gamma \Sequent
\Delta$, we are done. So suppose it doesn't. Since $\Gamma \fCenter
\Delta, !A$ is valid by induction hypothesis,
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. Similarly, since $\Gamma
\Sequent \Delta, !B$ is valid,
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$. But then
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$.
\item The last inference is \LeftR{\lor}: Exercise.
\item The last inference is \LeftR{\lif}. Then $\pi$ ends in
\begin{prooftree}
\AxiomC{}
\Deduce$\Gamma \fCenter \Delta, !A$
\AxiomC{}
\Deduce$!B, \Pi \fCenter \Lambda$
\RightLabel{\LeftR{\lif}}
\BinaryInf$!A \lif !B, \Gamma, \Pi \fCenter \Delta, \Lambda$
\end{prooftree}
Again, consider
\iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}
and suppose \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} doesn't satisfy
$\Gamma, \Pi \Sequent \Delta, \Lambda$. We have to show that
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A \lif !B}$. If
\iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} doesn't satisfy $\Gamma,
\Pi \Sequent \Delta, \Lambda$, it satisfies neither $\Gamma \Sequent
\Delta$ nor $\Pi \Sequent \Lambda$. Since, $\Gamma \Sequent \Delta,
!A$ is valid, we have $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. Since
$!B, \Pi \Sequent \Lambda$ is valid, we have
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$. But then
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A \lif !B}$, which is what we
wanted to show.
\end{enumerate}
\end{proof}
\tagprob{FOL}
\begin{prob}
Complete the proof of \olref[fol][seq][sou]{thm:sequent-soundness}.
\end{prob}
\tagendprob
\tagprob{notFOL}
\begin{prob}
Complete the proof of \olref[pl][seq][sou]{thm:sequent-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:entailment-soundness}
If $\Gamma \Proves !A$ then $\Gamma \Entails !A$.
\end{cor}
\begin{proof}
If $\Gamma \Proves !A$ then for some finite subset $\Gamma_0 \subseteq
\Gamma$, there is !!a{derivation} of $\Gamma_0 \Sequent !A$. By
\olref{thm:sequent-soundness}, every
\iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$}
either makes some $!B \in \Gamma_0$ false or makes $!A$ true. Hence,
if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$ then also
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$.
\end{proof}
\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 there is a finite $\Gamma_0 \subseteq \Gamma$ and !!a{derivation}
of $\Gamma_0 \Sequent \quad$. By \olref{thm:sequent-soundness},
$\Gamma_0 \Sequent \quad$ is valid. In other words, for every
\iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$},
there is $!C \in \Gamma_0$ so that
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$, and since $\Gamma_0
\subseteq \Gamma$, that $!C$ is also in~$\Gamma$. Thus, no
\iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} satisfies~$\Gamma$, and
$\Gamma$ is not satisfiable.
\end{proof}
\end{document}