The Sequent Calculus — Source and provenance

Source and provenance

All fifteen authority files and all 1,974 lines are shown exactly and packaged byte-for-byte. Four printed anomalies at seven anchors remain unchanged and are disclosed rather than silently corrected. Open the exact accepted projected chapter transcript (SHA-256 f339a160535ba9a2f38803b95e4365b6c61e3d889b3392cb9307528e16b61de0). Technical source commit: 9620cc73f9c8e0ad003c514a5d3748f29611c4c0. AI production model: OpenAI Codex gpt-5.6-sol, Ultra. Source authorship remains with the credited Open Logic Project contributors.

Four preserved printed-source anomalies; seven exact anchors

The reader preserves the printed forms without silent correction and gives the accepted listener disclosure at every applicable surface.

TR020-SOURCE-NOTE-001: Each cited inference reorders formulas in the antecedent, but the printed rule label names right exchange. Preserve and speak the printed right-exchange label, then disclose that the changed side is the antecedent and that left exchange appears intended. Source anchors: line 86, line 104, line 125, line 147.
TR020-SOURCE-NOTE-002: The immediately preceding argument establishes validity of the conclusion with the conjunction on the left; this sentence instead names the premise sequent. Preserve the printed claim and disclose that the preceding argument appears to establish the conclusion sequent with A and B conjoined on the left. Source anchors: line 157.
TR020-SOURCE-NOTE-003: The proof discusses satisfaction of the right premise, but the printed expression is set difference rather than a sequent. Preserve and read the printed expression as capital Pi set difference capital Lambda, then disclose that capital Pi sequent arrow capital Lambda appears intended. Source anchors: line 288.
TR020-SOURCE-NOTE-004: The printed conclusion ends with a comma after capital Delta but supplies no following succedent formula. Preserve and speak the printed trailing comma as having no following formula, then disclose that it appears to be stray punctuation. Source anchors: line 70.

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

56 lines; SHA-256 8cbb6df83670a2586d10ef405c78ed4f75102f8d63903eef93e7ac2b8ea3b603. Open the byte-exact 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 byte-exact 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 byte-exact 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/quantifier-rules.tex

104 lines; SHA-256 254abc98503c7370e046c43f8fec7cf7b5e9909be2959b0f1c513bb278d85b78. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: quantifier-rules
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{fol}{seq}{qrl}
\olsection{Quantifier Rules}
\subsection{Rules for $\lforall$}
\begin{defish}
\Axiom$ !A(t), \Gamma \fCenter \Delta$
\RightLabel{\LeftR{\lforall}}
\UnaryInf$ \lforall[x][!A(x)],\Gamma \fCenter \Delta$
\DisplayProof
\hfill
\Axiom$ \Gamma \fCenter \Delta, !A(a) $
\RightLabel{\RightR{\lforall}}
\UnaryInf$ \Gamma \fCenter \Delta, \lforall[x][!A(x)]$
\DisplayProof
\end{defish}
In \LeftR{\lforall}, $t$ is a closed term (i.e., one without
variables). In \RightR{\lforall}, $a$~is !!a{constant} which must not
occur anywhere in the lower sequent of the \RightR{\lforall} rule. We
call $a$ the \emph{eigenvariable} of the \RightR{\forall}
inference.\footnote{We use the term ``eigenvariable'' even though $a$
in the above rule is !!a{constant}. This has historical reasons.}
\subsection{Rules for $\lexists$}
\begin{defish}
\Axiom$ !A(a), \Gamma \fCenter \Delta $
\RightLabel{\LeftR{\lexists}}
\UnaryInf$ \lexists[x][!A(x)], \Gamma \fCenter \Delta$
\DisplayProof
\hfill
\Axiom$ \Gamma \fCenter \Delta, !A(t) $
\RightLabel{\RightR{\lexists}}
\UnaryInf$ \Gamma \fCenter \Delta, \lexists[x][!A(x)]$
\DisplayProof
\end{defish}
Again, $t$~is a closed term, and $a$~is !!a{constant} which does not
occur in the lower sequent of the \LeftR{\lexists} rule. We call $a$
the \emph{eigenvariable} of the \LeftR{\lexists} inference.
The condition that an eigenvariable not occur in the lower sequent of
the \RightR{\lforall} or \LeftR{\lexists} inference is called the
\emph{eigenvariable condition}.
\begin{explain}
Recall the convention that when $!A$ is !!a{formula} with the
!!{variable}~$x$ free, we indicate this by writing~$!A(x)$. In the
same context, $!A(t)$ then is short for~$\Subst{!A}{t}{x}$. So we
could also write the \RightR{\lexists} rule as:
\begin{prooftree}
\Axiom$\Gamma \fCenter \Delta, \Subst{!A}{t}{x}$
\RightLabel{\RightR{\lexists}}
\UnaryInf$\Gamma \fCenter \Delta, \lexists[x][!A]$
\end{prooftree}
Note that $t$ may already occur in~$!A$, e.g., $!A$~might
be~$\Atom{\Obj P}{t,x}$. Thus, inferring $\Gamma \Sequent \Delta,
\lexists[x][\Atom{\Obj P}{t,x}]$ from~$\Gamma \Sequent \Delta,
\Atom{\Obj P}{t,t}$ is a correct application
of~\RightR{\lexists}---you may ``replace'' one or more, and not
necessarily all, occurrences of~$t$ in the premise by the bound
!!{variable}~$x$. However, the eigenvariable conditions in
\RightR{\lforall} and~\LeftR{\lexists} require that the
!!{constant}~$a$ does not occur in~$!A$. So, you cannot correctly
infer $\Gamma \Sequent \Delta, \lforall[x][\Atom{\Obj P}{a,x}]$ from
$\Gamma \Sequent \Delta, \Atom{\Obj P}{a,a}$ using~$\RightR{\lforall}$.
\end{explain}
\begin{explain}
In \RightR{\lexists} and \LeftR{\lforall} there are no restrictions on
the term~$t$. On the other hand, in the \LeftR{\lexists} and
\RightR{\lforall} rules, the eigenvariable condition requires that the
!!{constant}~$a$ does not occur anywhere outside of~$!A(a)$ in the
upper sequent. It is necessary to ensure that the system is sound,
i.e., only !!{derive}s sequents that are valid. Without this
condition, the following would be allowed:
\begin{prooftree}
\Axiom$!A(a) \fCenter !A(a)$
\RightLabel{*\LeftR{\lexists}}
\UnaryInf$\lexists[x][!A(x)] \fCenter !A(a)$
\RightLabel{\RightR{\lforall}}
\UnaryInf$\lexists[x][!A(x)] \fCenter \lforall[x][!A(x)]$
\DisplayProof\bottomAlignProof
\qquad
\Axiom$!A(a) \fCenter !A(a)$
\RightLabel{*\RightR{\lforall}}
\UnaryInf$!A(a) \fCenter \lforall[x][!A(x)]$
\RightLabel{\LeftR{\lexists}}
\UnaryInf$\lexists[x][!A(x)] \fCenter \lforall[x][!A(x)]$
\end{prooftree}
However, $\lexists[x][!A(x)] \Sequent \lforall[x][!A(x)]$ is not valid.
\end{explain}
\end{document}

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

80 lines; SHA-256 ea1ca77eca03ec566cc900b2399e95002b4cfc07eb3549a3f19da9ee23a09793. Open the byte-exact 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 byte-exact 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,$
TR020-SOURCE-NOTE-004: The printed conclusion ends with a comma after capital Delta but supplies no following succedent formula. Preserve and speak the printed trailing comma as having no following formula, then disclose that it appears to be stray punctuation.
\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 byte-exact 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}}
TR020-SOURCE-NOTE-001: Each cited inference reorders formulas in the antecedent, but the printed rule label names right exchange. Preserve and speak the printed right-exchange label, then disclose that the changed side is the antecedent and that left exchange appears intended.
\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}}
TR020-SOURCE-NOTE-001: Each cited inference reorders formulas in the antecedent, but the printed rule label names right exchange. Preserve and speak the printed right-exchange label, then disclose that the changed side is the antecedent and that left exchange appears intended.
\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}}
TR020-SOURCE-NOTE-001: Each cited inference reorders formulas in the antecedent, but the printed rule label names right exchange. Preserve and speak the printed right-exchange label, then disclose that the changed side is the antecedent and that left exchange appears intended.
\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}}
TR020-SOURCE-NOTE-001: Each cited inference reorders formulas in the antecedent, but the printed rule label names right exchange. Preserve and speak the printed right-exchange label, then disclose that the changed side is the antecedent and that left exchange appears intended.
\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/proving-things-quant.tex

110 lines; SHA-256 9c249f76aa00ddc5b64b68179b052d7df7e7ffa69be413de20796d98bd80389d. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: proving-things-quant
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{fol}{seq}{prq}
\olsection{\usetoken{P}{derivation} with Quantifiers}
\begin{ex}
Give an $\Log{LK}$-!!{derivation} of the sequent $\lexists[x][\lnot !A(x)]
\Sequent \lnot \lforall[x][!A(x)]$.
When dealing with quantifiers, we have to make sure not to violate the
eigenvariable condition, and sometimes this requires us to play around
with the order of carrying out certain inferences. In general, it
helps to try and take care of rules subject to the eigenvariable
condition first (they will be lower down in the finished proof). Also,
it is a good idea to try and look ahead and try to guess what the
initial sequent might look like. In our case, it will have to be
something like $!A(a) \Sequent !A(a)$. That means that when we are
``reversing'' the quantifier rules, we will have to pick the same
term---what we will call $a$---for both the $\lforall$ and the
$\lexists$ rule. If we picked different terms for each rule, we would
end up with something like $!A(a) \Sequent !A(b)$, which, of course,
is not derivable.
Starting as usual, we write
\begin{prooftree}
\AxiomC{}
\UnaryInf$\lexists[x][\lnot !A(x)] \fCenter \lnot \lforall[x][!A(x)]$
\end{prooftree}
We could either carry out the \LeftR{\exists} rule or the \RightR{\lnot}
rule. Since the \LeftR{\exists} rule is subject to the eigenvariable
condition, it's a good idea to take care of it sooner rather than
later, so we'll do that one first.
\begin{prooftree}
\AxiomC{}
\UnaryInf$ \lnot !A(a) \fCenter \lnot \lforall[x][!A(x)]$
\RightLabel{\LeftR{\lexists}}
\UnaryInf$ \lexists[x][\lnot !A(x)] \fCenter \lnot \lforall[x][!A(x)]$
\end{prooftree}
Applying the \LeftR{\lnot} and \RightR{\lnot} rules backwards, we get
\begin{prooftree}
\AxiomC{}
\UnaryInf$\lforall[x][!A(x)] \fCenter !A(a)$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$\lnot !A(a), \lforall[x][!A(x)] \fCenter $
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$\lforall[x][!A(x)], \lnot !A(a) \fCenter $
\RightLabel{\RightR{\lnot}}
\UnaryInf$ \lnot !A(a) \fCenter \lnot \lforall[x] !A(x)$
\RightLabel{\LeftR{\lexists}}
\UnaryInf$ \lexists[x] \lnot !A(x) \fCenter \lnot \lforall[x] !A(x)$
\end{prooftree}
At this point, our only option is to carry out the \LeftR{\forall}
rule. Since this rule is not subject to the eigenvariable restriction,
we're in the clear. Remember, we want to try and obtain an initial
sequent (of the form $!A(a) \Sequent !A(a)$), so we should choose $a$
as our argument for $!A$ when we apply the rule.
\begin{prooftree}
\Axiom$!A(a) \fCenter !A(a)$
\RightLabel{\LeftR{\lforall}}
\UnaryInf$\lforall[x][!A(x)] \fCenter !A(a)$
\RightLabel{\LeftR{\lnot}}
\UnaryInf$\lnot !A(a), \lforall[x][!A(x)] \fCenter $
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$\lforall[x][!A(x)], \lnot !A(a) \fCenter $
\RightLabel{\RightR{\lnot}}
\UnaryInf$ \lnot !A(a) \fCenter \lnot \lforall[x][!A(x)]$
\RightLabel{\LeftR{\lexists}}
\UnaryInf$ \lexists[x][ \lnot !A(x)] \fCenter \lnot \lforall[x][!A(x)]$
\end{prooftree}
It is important, especially when dealing with quantifiers, to double
check at this point that the eigenvariable condition has not been
violated. Since the only rule we applied that is subject to the
eigenvariable condition was \LeftR{\exists}, and the eigenvariable~$a$
does not occur in its lower sequent (the end-sequent), this is a
correct !!{derivation}.
\end{ex}
\begin{prob}
Give !!{derivation}s of the following sequents:
\begin{enumerate}
\item $\Sequent (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) \lif
\lforall[z][(!A(z) \land !B(z))]$.
\item $\Sequent (\lexists[x][!A(x)] \lor \lexists[y][!B(y)]) \lif
\lexists[z][(!A(z) \lor !B(z))]$.
\item $\lforall[x][(!A(x) \lif !B)] \Sequent \lexists[y][!A(y)] \lif !B$.
\item $\lforall[x][\lnot !A(x)] \Sequent \lnot\lexists[x][!A(x)]$.
\item $\Sequent \lnot\lexists[x][!A(x)] \lif \lforall[x][\lnot !A(x)]$.
\item $\Sequent \lnot\lexists[x][\lforall[y][((!A(x,y) \lif \lnot
!A(y,y)) \land (\lnot !A(y,y) \lif !A(x,y)))]]$.
\end{enumerate}
\end{prob}
\begin{prob}
Give !!{derivation}s of the following sequents:
\begin{enumerate}
\item $\Sequent \lnot\lforall[x][!A(x)] \lif \lexists[x][\lnot!A(x)]$.
\item $(\lforall[x][!A(x)] \lif !B) \Sequent \lexists[y][(!A(y) \lif !B)]$.
\item $\Sequent \lexists[x][(!A(x) \lif \lforall[y][!A(y)])]$.
\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 byte-exact 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 byte-exact 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 byte-exact 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/provability-quantifiers.tex

59 lines; SHA-256 eb63f32c87bbdbef776a65a4c1da758fd5671e47e3c4171f224d3214b31aa48f. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: provability-quantifiers
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{fol}{seq}{qpr}
\olsection{\usetoken{S}{derivability} and the Quantifiers}
\begin{explain}
The completeness theorem also requires that the sequent calculus
rules yield the facts about~$\Proves$ established in this
section.
\end{explain}
\begin{thm}
\ollabel{thm:strong-generalization} If $c$ is a constant not occurring
in $\Gamma$ or $!A(x)$ and $\Gamma \Proves !A(c)$, then $\Gamma
\Proves \lforall[x][!A(x)]$.
\end{thm}
\begin{proof}
Let $\pi_0$ be an $\Log{LK}$-!!{derivation} of $\Gamma_0 \Sequent !A(c)$
for some finite $\Gamma_0 \subseteq \Gamma$. By adding a
$\RightR{\lforall}$ inference, we obtain !!a{derivation} of $\Gamma_0 \Sequent
\lforall[x][!A(x)]$, since $c$ does not occur in $\Gamma$ or $!A(x)$
and thus the eigenvariable condition is satisfied.
\end{proof}
\begin{prop}
\ollabel{prop:provability-quantifiers}
\begin{tagenumerate}{prvEx,prvAll}
\tagitem{prvEx}{$!A(t) \Proves \lexists[x][!A(x)]$.}{}
\tagitem{prvAll}{$\lforall[x][!A(x)] \Proves !A(t)$.}{}
\end{tagenumerate}
\end{prop}
\begin{proof}
\begin{tagenumerate}{prvEx,prvAll}
\tagitem{prvEx}{The sequent $!A(t) \Sequent \lexists[x][!A(x)]$ is
!!{derivable}:
\begin{prooftree}
\Axiom$!A(t) \fCenter !A(t)$
\RightLabel{\RightR{\lexists}}
\UnaryInf$!A(t) \fCenter \lexists[x][!A(x)]$
\end{prooftree}}{}
\tagitem{prvAll}{The sequent $\lforall[x][!A(x)] \Sequent !A(t)$ is
!!{derivable}:
\begin{prooftree}
\Axiom$!A(t) \fCenter !A(t)$
\RightLabel{\LeftR{\lforall}}
\UnaryInf$\lforall[x][!A(x)] \fCenter !A(t)$
\end{prooftree}}{}
\end{tagenumerate}
\end{proof}
\end{document}

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

384 lines; SHA-256 d9f6180bee35f29553144b6eca5a1eb1916e0262dcdc8c30f50193a53d8001fa. Open the byte-exact 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
TR020-SOURCE-NOTE-002: The immediately preceding argument establishes validity of the conclusion with the conjunction on the left; this sentence instead names the premise sequent. Preserve the printed claim and disclose that the preceding argument appears to establish the conclusion sequent with A and B conjoined on the left.
\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,
TR020-SOURCE-NOTE-003: The proof discusses satisfaction of the right premise, but the printed expression is set difference rather than a sequent. Preserve and read the printed expression as capital Pi set difference capital Lambda, then disclose that capital Pi sequent arrow capital Lambda appears intended.
\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}

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

77 lines; SHA-256 f9abed3c3d8c2079b2be27fdcb551c8f1987d1b4db18ece56d4c9e1a7b066856. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: equality
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{fol}{seq}{ide}
\olsection{\usetoken{P}{derivation} with \usetoken{S}{identity}}
!!^{derivation}s with !!{identity} require additional initial sequents
and inference rules.
\begin{defn}[Initial sequents for $\eq$]
If $t$ is a closed term, then ${} \Sequent \eq[t][t]$ is an initial sequent.
\end{defn}
The rules for $\eq$ are ($t_1$ and $t_2$ are closed terms):
\begin{defish}
\Axiom$ \eq[t_1][t_2], \Gamma \fCenter \Delta, !A(t_1) $
\RightLabel{$\eq$}
\UnaryInf$\eq[t_1][t_2], \Gamma \fCenter \Delta, !A(t_2)$
\DisplayProof
\hfill
\Axiom$\eq[t_1][t_2], \Gamma \fCenter \Delta, !A(t_2) $
\RightLabel{$\eq$}
\UnaryInf$\eq[t_1][t_2], \Gamma \fCenter \Delta, !A(t_1)$
\DisplayProof
\end{defish}
\begin{ex}
If $s$ and $t$ are closed terms, then $\eq[s][t], !A(s)
\Proves !A(t)$:
\begin{prooftree}
\Axiom$ !A(s) \fCenter !A(s)$
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$\eq[s][t], !A(s) \fCenter !A(s)$
\RightLabel{$\eq$}
\UnaryInf$\eq[s][t], !A(s) \fCenter !A(t)$
\end{prooftree}
This may be familiar as the principle of substitutability of
identicals, or Leibniz' Law.
$\Log{LK}$ proves that $\eq$ is symmetric and transitive:
\begin{prooftree}
\Axiom$ \fCenter \eq[t_1][t_1] $
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$ \eq[t_1][t_2] \fCenter \eq[t_1][t_1] $
\RightLabel{$\eq$}
\UnaryInf$ \eq[t_1][t_2] \fCenter \eq[t_2][t_1]$
\DisplayProof\qquad\bottomAlignProof
\Axiom$ \eq[t_1][t_2] \fCenter \eq[t_1][t_2] $
\RightLabel{\LeftR{\Weakening}}
\UnaryInf$\eq[t_2][t_3], \eq[t_1][t_2] \fCenter \eq[t_1][t_2] $
\RightLabel{$\eq$}
\UnaryInf$\eq[t_2][t_3], \eq[t_1][t_2] \fCenter \eq[t_1][t_3]$
\RightLabel{\LeftR{\Exchange}}
\UnaryInf$\eq[t_1][t_2], \eq[t_2][t_3] \fCenter \eq[t_1][t_3]$
\end{prooftree}
In the !!{derivation} on the left, the !!{formula}~$\eq[x][t_1]$ is our
$!A(x)$. On the right, we take $!A(x)$ to be~$\eq[t_1][x]$.
\end{ex}
\begin{prob}
Give !!{derivation}s of the following sequents:
\begin{enumerate}
\item $\Sequent \lforall[x][\lforall[y][((x = y \land !A(x)) \lif !A(y))]]$
\item $\lexists[x][!A(x)] \land \lforall[y][\lforall[z][((!A(y) \land
!A(z)) \lif y = z)]] \Sequent
\lexists[x][(!A(x) \land \lforall[y][(!A(y) \lif y = x)])]$
\end{enumerate}
\end{prob}
\end{document}

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

44 lines; SHA-256 da0c929628dc2c252d9d48d2fff02439e26c7a984db958943aa6cd55bb4ffeb5. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: sequent-calculus
% Section: soundness-identity
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{fol}{seq}{sid}
\olsection{Soundness with \usetoken{S}{identity}}
\begin{prop}
$\Log{LK}$ with initial sequents and rules for identity is sound.
\end{prop}
\begin{proof}
Initial sequents of the form ${} \Sequent \eq[t][t]$ are valid, since
for every !!{structure}~$\Struct M$, $\Sat{M}{\eq[t][t]}$. (Note that
we assume the term $t$ to be closed, i.e., it contains no variables,
so variable assignments are irrelevant).
Suppose the last inference in !!a{derivation} is $=$. Then the premise
is $\eq[t_1][t_2], \Gamma \Sequent \Delta, !A(t_1)$ and the conclusion
is $\eq[t_1][t_2], \Gamma \Sequent \Delta, !A(t_2)$. Consider
!!a{structure}~$\Struct M$. We need to show that the conclusion is
valid, i.e., if $\Sat{M}{\eq[t_1][t_2]}$ and $\Sat{M}{\Gamma}$, then
either $\Sat{M}{!C}$ for some $!C \in \Delta$ or $\Sat{M}{!A(t_2)}$.
By induction hypothesis, the premise is valid. This means that if
$\Sat{M}{\eq[t_1][t_2]}$ and $\Sat{M}{\Gamma}$ either (a) for some $!C
\in \Delta$, $\Sat{M}{!C}$ or (b) $\Sat{M}{!A(t_1)}$. In case (a) we
are done. Consider case (b). Let $s$ be a variable assignment with
$s(x) = \Value{t_1}{M}$. By \olref[syn][ass]{prop:sentence-sat-true},
$\Sat{M}{!A(t_1)}[s]$. Since $\varAssign{s}{s}{x}$, by
\olref[syn][ext]{prop:ext-formulas}, $\Sat{M}{!A(x)}[s]$. since
$\Sat{M}{\eq[t_1][t_2]}$, we have $\Value{t_1}{M} = \Value{t_2}{M}$,
and hence $s(x) = \Value{t_2}{M}$. By applying
\olref[syn][ext]{prop:ext-formulas} again, we also have
$\Sat{M}{!A(t_2)}[s]$. By \olref[syn][ass]{prop:sentence-sat-true},
$\Sat{M}{!A(t_2)}$.
\end{proof}
\end{document}