Tableaux — Source and provenance

Source and provenance

All nine authority files and all 1,517 lines are shown exactly and copied byte-for-byte. Reader corrections are disclosures only; the source text below is not altered.

Seven disclosed reader corrections

The frozen source remains unchanged. These reviewed reader interventions are visible wherever the affected material is presented.

TR012-SOURCE-FORMULA-001: The frozen source first writes Gamma sub one as C sub one through C sub n, then uses C sub one through C sub m in the next display. The reader preserves both indices and discloses the mismatch.
TR012-SOURCE-FORMULA-006: The frozen exercise accidentally groups not B inside the preceding signed-formula argument. The reader preserves the printed source and explicitly presents the intended three separate signed assumptions.
TR012-SOURCE-FORMULA-007: The reader preserves the printed D-sub-m subset relation as source MathML and explicitly identifies it as malformed. A separate reader projection gives the finite-family inclusion required by the surrounding derivability argument.
TR012-SOURCE-PROOF-005: The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering.
TR012-SOURCE-PROSE-002: The reader removes the duplicated word in the source phrase 'left left.'
TR012-SOURCE-PROSE-003: The reader corrects the source phrase 'we can applying' to 'we can apply.'
TR012-SOURCE-TABLEAU-004: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.

content/first-order-logic/tableaux/tableaux.tex

54 lines; SHA-256 eaf9e7719e1e71efb2b82fa80bae67063790e30ef901686a065a23536e253098. Open the byte-exact preserved source file.

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

content/first-order-logic/tableaux/rules-and-proofs.tex

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

% Part: first-order-logic
% Chapter: tableaux
% Section: rules-and-proofs
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{tab}{rul}}
{\olfileid{pl}{tab}{rul}}
\olsection{Rules and \usetoken{P}{tableau}}
!!^a{tableau} is a systematic survey of the possible ways
!!a{sentence} can be true or false in !!a{structure}. The building
blocks of a tableau are !!{signed formula}s: !!{sentence}s plus a
truth value ``sign,'' either $\True$ or~$\False$. These signed
!!{formula}s are arranged in a (downward growing) tree.
\begin{defn}
A \emph{!!{signed formula}} is a pair consisting of a truth value
and !!a{sentence}, i.e., either:
\[
\sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.
\]
\end{defn}
Intuitively, we might read $\sFmla{\True}{!A}$ as ``$!A$ might be
true'' and $\sFmla{\False}{!A}$ as ``$!A$ might be false'' (in some
!!{structure}).
Each !!{signed formula} in the tree is either an \emph{assumption}
(which are listed at the very top of the tree), or it is obtained from
!!a{signed formula} above it by one of a number of rules of
inference. There are two rules for each possible !!{main operator} of
the preceding !!{formula}, one for the case where the sign is~$\True$,
and one for the case where the sign is~$\False$. Some rules allow the
tree to branch, and some only add !!{signed formula}s to the branch.
A rule may be (and often must be) applied not to the immediately
preceding !!{signed formula}, but to any !!{signed formula} in the
branch from the root to the place the rule is applied.
A branch is \emph{closed} when it contains both $\sFmla{\True}{!A}$
and $\sFmla{\False}{!A}$. A closed !!{tableau} is one where every branch
is closed. Under the intuitive interpretation, any branch describes a
joint possibility, but $\sFmla{\True}{!A}$ and $\sFmla{\False}{!A}$
are not jointly possible. In other words, if a branch is closed, the
possibility it describes has been ruled out. In particular, that means
that a closed !!{tableau} rules out all possibilities of simultaneously
making every assumption of the form $\sFmla{\True}{!A}$ true and every
assumption of the form~$\sFmla{\False}{!A}$ false.
A closed !!{tableau} \emph{for $!A$} is a closed !!{tableau} with
root~$\sFmla{\False}{!A}$. If such a closed !!{tableau} exists, all
possibilities for~$!A$ being false have been ruled out; i.e., $!A$
must be true in every !!{structure}.
\end{document}

content/first-order-logic/tableaux/propositional-rules.tex

93 lines; SHA-256 0e0a8d69ddabb157d54f03e7ff21416fb0c818e481343f4ac00ee4ba1d5bf151. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: tableaux
% Section: propositional-rules
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{tab}{prl}}
{\olfileid{pl}{tab}{prl}}
\olsection{Propositional Rules}
\subsection{Rules for $\lnot$}
\begin{defish}
\AxiomC{\sFmla{\True}{\lnot !A}}
\RightLabel{\TRule{\True}{\lnot}}
\UnaryInfC{\sFmla{\False}{!A}}
\DisplayProof
\hfill
\AxiomC{\sFmla{\False}{\lnot !A}}
\RightLabel{\TRule{\False}{\lnot}}
\UnaryInfC{\sFmla{\True}{!A}}
\DisplayProof
\end{defish}
\subsection{Rules for $\land$}
\begin{defish}\noindent
\AxiomC{\sFmla{\True}{!A \land !B}}
\RightLabel{\TRule{\True}{\land}}
\UnaryInfC{\sFmla{\True}{!A}}
\noLine
\UnaryInfC{\sFmla{\True}{!B}}
\DisplayProof
\hfill
\AxiomC{\sFmla{\False}{!A \land !B}}
\RightLabel{\TRule{\False}{\land}}
\UnaryInfC{$\sFmla{\False}{!A} \quad \mid \quad \sFmla{\False}{!B}$}
\DisplayProof
\end{defish}
\subsection{Rules for $\lor$}
\begin{defish}
\AxiomC{\sFmla{\True}{!A \lor !B}}
\RightLabel{\TRule{\True}{\lor}}
\UnaryInfC{$\sFmla{\True}{!A} \quad \mid \quad \sFmla{\True}{!B}$}
\DisplayProof
\hfill
\AxiomC{\sFmla{\False}{!A \lor !B}}
\RightLabel{\TRule{\False}{\lor}}
\UnaryInfC{\sFmla{\False}{!A}}
\noLine
\UnaryInfC{\sFmla{\False}{!B}}
\DisplayProof
\end{defish}
\subsection{Rules for $\lif$}
\begin{defish}
\AxiomC{\sFmla{\True}{!A \lif !B}}
\RightLabel{\TRule{\True}{\lif}}
\UnaryInfC{$\sFmla{\False}{!A} \quad \mid \quad \sFmla{\True}{!B}$}
\DisplayProof
\hfill
\AxiomC{\sFmla{\False}{!A \lif !B}}
\RightLabel{\TRule{\False}{\lif}}
\UnaryInfC{\sFmla{\True}{!A}}
\noLine
\UnaryInfC{\sFmla{\False}{!B}}
\DisplayProof
\end{defish}
\subsection{The Cut Rule}
\begin{defish}
\AxiomC{}
\RightLabel{\Cut}
\UnaryInfC{$\sFmla{\True}{!A} \quad \mid \quad \sFmla{\False}{!A}$}
\DisplayProof
\end{defish}
The \Cut{} rule is not applied ``to'' a previous !!{signed formula}; rather,
it allows every branch in !!a{tableau} to be split in two, one branch
containing $\sFmla{\True}{!A}$, the other~$\sFmla{\False}{!A}$. It is
not necessary---any set of !!{signed formula}s with a closed
!!{tableau} has one not using \Cut---but it allows us to combine
!!{tableau}s in a convenient way.
\end{document}

content/first-order-logic/tableaux/derivations.tex

96 lines; SHA-256 3f3e041127342c4f2565632d33c855fcb7a87964d63beb38bd8313c8a71ad294. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: tableaux
% Section: derivations
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{tab}{der}}
{\olfileid{pl}{tab}{der}}
\olsection{\usetoken{P}{tableau}}
\begin{explain}
We've said what an assumption is, and we've given the rules of
inference. !!^{tableau}s are inductively generated from these: each
!!{tableau} either is a single branch consisting of one or more
assumptions, or it results from !!a{tableau} by applying one of the
rules of inference on a branch.
\end{explain}
\begin{defn}[!!^{tableau}]
!!^a{tableau} for assumptions $\sFmla{S_1}{!A_1}$, \dots,
$\sFmla{S_n}{!A_n}$ (where each $S_i$ is either $\True$ or~$\False$) is
a finite tree of !!{signed formula}s satisfying the following conditions:
\begin{enumerate}
\item The $n$ topmost !!{signed formula}s of the tree are
$\sFmla{S_i}{!A_i}$, one below the other.
\item Every !!{signed formula} in the tree that is not one of the
assumptions results from a correct application of an inference rule
to !!a{signed formula} in the branch above it.
\end{enumerate}
A branch of !!a{tableau} is \emph{closed} iff it contains both
$\sFmla{\True}{!A}$ and~$\sFmla{\False}{!A}$, and \emph{open}
otherwise. !!^a{tableau} in which every branch is closed is a
\emph{closed !!{tableau}} (for its set of assumptions). If !!a{tableau} is
not closed, i.e., if it contains at least one open branch, it is
\emph{open}.
\end{defn}
\begin{ex}
Every set of assumptions on its own is !!a{tableau}, but it will
generally not be closed. (Obviously, it is closed only if the
assumptions already contain a pair of !!{signed formula}s
$\sFmla{\True}{!A}$ and~$\sFmla{\False}{!A}$.)
From !!a{tableau} (open or closed) we can obtain a new, larger one by
applying one of the rules of inference to !!a{signed formula}~$!A$
in it. The rule will append one or more !!{signed formula}s to the end of
any branch containing the occurrence of~$!A$ to which we apply the
rule.
For instance, consider the assumption $\sFmla{\True}{!A \land \lnot
!A}$. Here is the (open) !!{tableau} consisting of just that
assumption:
\begin{center}
\begin{tableau}{}
[\sFmla{\True}{\formula{A} \land \lnot \formula{A}}, just=\TAss]
\end{tableau}{}
\end{center}
We obtain a new !!{tableau} from it by applying the $\TRule{\True}{\land}$
rule to the assumption. That rule allows us to add two new lines to
the !!{tableau}, $\sFmla{\True}{!A}$ and $\sFmla{\True}{\lnot !A}$:
\begin{center}
\begin{tableau}{}
[\sFmla{\True}{\formula{A} \land \lnot \formula{A}}, just=\TAss
[\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\land}[1]},
[\sFmla{\True}{\lnot \formula{A}}, just={\TRule{\True}{\land}[1]}
]
]
]
\end{tableau}{}
\end{center}
When we write down !!{tableau}s, we record the rules we've applied
on the right (e.g., $\TRule{\True}{\land} 1$ means that the
!!{signed formula} on that line is the result of applying the
$\TRule{\True}{\land}$ rule to the !!{signed formula} on line~$1$).
This new !!{tableau} now contains additional !!{signed formula}s,
but to only one ($\sFmla{\True}{\lnot !A}$) can we apply a rule (in
this case, the $\TRule{\True}{\lnot}$ rule). This results in the closed
!!{tableau}
\begin{center}
\begin{tableau}{}
[\sFmla{\True}{\formula{A} \land \lnot \formula{A}}, just=\TAss
[\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\land}[1]}
[\sFmla{\True}{\lnot \formula{A}}, just={\TRule{\True}{\land}[1]}
[\sFmla{\False}{\formula{A}}, just={\TRule{\True}{\lnot}[3]}, close]
]
]
]
\end{tableau}{}
\end{center}
\end{ex}
\end{document}

content/first-order-logic/tableaux/proving-things.tex

460 lines; SHA-256 ba6a2d3c2f7c7504daa17942290c75084bbfab92663a492557ca6530a175d914. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: tableaux
% Section: proving-things
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{tab}{pro}}
{\olfileid{pl}{tab}{pro}}
\olsection{Examples of \usetoken{P}{tableau}}
\begin{ex}
Let's find a closed !!{tableau} for the !!{sentence} $(!A \land !B) \lif !A$.
We begin by writing the corresponding assumption at the top of the
!!{tableau}.
\begin{oltableau}
[\sFmla{\False}{(\formula{A} \land \formula{B}) \lif \formula{A}},
just = \TAss]
\end{oltableau}
There is only one assumption, so only one !!{signed formula} to which
we can apply a rule. (For every !!{signed formula}, there is always at
most one rule that can be applied: it's the rule for the corresponding
sign and !!{main operator} of the !!{sentence}.) In this case, this
means, we must apply $\TRule{\False}{\lif}$.
\begin{oltableau}
[\sFmla{\False}{(\formula{A} \land \formula{B}) \lif \formula{A}},
checked, just = \TAss
[\sFmla{\True}{\formula{A} \land \formula{B}},
just={\TRule{\False}{\lif}[1]}
[\sFmla{\False}{\formula{A}}, just={\TRule{\False}{\lif}[1]}]
]
]
\end{oltableau}
To keep track of which !!{signed formula}s we have applied their
corresponding rules to, we write a checkmark next to the
sentence. However, \emph{only} write a checkmark if the rule has been
applied to all open branches. Once !!a{signed formula} has had the
corresponding rule applied in every open branch, we will not have to
return to it and apply the rule again. In this case, there is only one
branch, so the rule only has to be applied once. (Note that checkmarks
are only a convenience for constructing tableaux and are not
officially part of the syntax of tableaux.)
There is one new !!{signed formula} to which we can apply a rule: the
$\sFmla{\True}{!A \land !B}$ on line~$2$. Applying the
$\TRule{\True}{\land}$ rule results in:
\begin{oltableau}
[\sFmla{\False}{(\formula{A} \land \formula{B}) \lif \formula{A}},
checked, just = \TAss
[\sFmla{\True}{\formula{A} \land \formula{B}},
just={\TRule{\False}{\lif}[1]}, checked
[\sFmla{\False}{\formula{A}}, just={\TRule{\False}{\lif}[1]}
[\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\land}[2]}
[\sFmla{\True}{\formula{B}}, just={\TRule{\True}{\land}[2]}, close
]
]
]
]
]
\end{oltableau}
Since the branch now contains both $\sFmla{\True}{!A}$ (on line~$4$)
and $\sFmla{\False}{!A}$ (on line~$3$), the branch is closed. Since it
is the only branch, the !!{tableau} is closed. We have found
a closed !!{tableau} for~$(!A \land !B) \lif !A$.
\end{ex}
\begin{ex}
Now let's find a closed !!{tableau} for $(\lnot !A \lor !B) \lif (!A
\lif !B)$.
We begin with the corresponding assumption:
\begin{oltableau}
[\sFmla{\False}{(\lnot \formula{A} \lor \formula{B}) \lif
(\formula{A} \lif \formula{B})}, just=\TAss]
\end{oltableau}
The one !!{signed formula} in this !!{tableau} has !!{main operator}~$\lif$
and sign~$\False$, so we apply the $\TRule{\False}{\lif}$ rule to it
to obtain:
\begin{oltableau}
[\sFmla{\False}{(\lnot \formula{A} \lor \formula{B})
\lif (\formula{A} \lif \formula{B})}, just=\TAss, checked
[\sFmla{\True}{\lnot \formula{A} \lor \formula{B}},
just={\TRule{\False}{\lif}[1]}
[\sFmla{\False}{(\formula{A} \lif \formula{B})},
just={\TRule{\False}{\lif}[1]}
]
]
]
\end{oltableau}
We now have a choice as to whether to apply~$\TRule{\True}{\lor}$ to
line~$2$ or $\TRule{\False}{\lif}$ to line~$3$. It actually doesn't
matter which order we pick, as long as each !!{signed formula} has its
corresponding rule applied in every branch. So let's pick the first
one. The $\TRule{\True}{\lor}$ rule allows the !!{tableau} to branch,
and the two conclusions of the rule will be the new !!{signed formula}s
added to the two new branches. This results in:
\begin{oltableau}
[\sFmla{\False}{(\lnot \formula{A} \lor \formula{B}) \lif
(\formula{A} \lif \formula{B})}, just=\TAss, checked
[\sFmla{\True}{\lnot \formula{A} \lor \formula{B}},
just={\TRule{\False}{\lif}[1]}, checked
[\sFmla{\False}{(\formula{A} \lif \formula{B})},
just={\TRule{\False}{\lif}[1]}
[\sFmla{\True}{\lnot \formula{A}}, just={\TRule{\True}{\lor}[2]}]
[\sFmla{\True}{\formula{B}}, just={\TRule{\True}{\lor}[2]}]
]
]
]
\end{oltableau}
We have not applied the $\TRule{\False}{\lif}$ rule to line~$3$ yet:
let's do that now. To save time, we apply it to both branches.
Recall that we write a checkmark next to !!a{signed formula} only if
we have applied the corresponding rule in every open branch. So it's a
good idea to apply a rule at the end of every branch that contains the
!!{signed formula} the rule applies to. That way we won't have to
return to that !!{signed formula} lower down in the various branches.
\begin{oltableau}
[\sFmla{\False}{(\lnot \formula{A} \lor \formula{B}) \lif
(\formula{A} \lif \formula{B})}, just=\TAss, checked
[\sFmla{\True}{\lnot \formula{A} \lor \formula{B}},
just={\TRule{\False}{\lif}[1]}, checked
[\sFmla{\False}{(\formula{A} \lif \formula{B})},
just={\TRule{\False}{\lif}[1]}, checked
[\sFmla{\True}{\lnot \formula{A}}, just={\TRule{\True}{\lor}[2]}
[\sFmla{\True}{\formula{A}}, just={\TRule{\False}{\lif}[3]}
[\sFmla{\False}{\formula{B}}, just={\TRule{\False}{\lif}[3]}]
]
]
[\sFmla{\True}{\formula{B}}, just={\TRule{\True}{\lor}[2]}
[\sFmla{\True}{\formula{A}}, just={\TRule{\False}{\lif}[3]}
[\sFmla{\False}{\formula{B}}, just={\TRule{\False}{\lif}[3]}, close]
]
]
]
]
]
\end{oltableau}
The right branch is now closed. On the left branch, we can still apply
the $\TRule{\True}{\lnot}$ rule to line~$4$. This results
in~$\sFmla{\False}{!A}$ and closes the left branch:
\begin{oltableau}
[\sFmla{\False}{(\lnot \formula{A} \lor \formula{B}) \lif
(\formula{A} \lif \formula{B})}, just=\TAss, checked
[\sFmla{\True}{\lnot \formula{A} \lor \formula{B}},
just={\TRule{\False}{\lif}[1]}, checked
[\sFmla{\False}{(\formula{A} \lif \formula{B})},
just={\TRule{\False}{\lif}[1]}, checked
[\sFmla{\True}{\lnot \formula{A}}, just={\TRule{\True}{\lor}[2]}
[\sFmla{\True}{\formula{A}}, just={\TRule{\False}{\lif}[3]}
[\sFmla{\False}{\formula{B}}, just={\TRule{\False}{\lif}[3]}
[\sFmla{\False}{\formula{A}},
just={\TRule{\True}{\lnot}[4]}, close]
]
]
]
[\sFmla{\True}{\formula{B}}, just={\TRule{\True}{\lor}[2]}
[\sFmla{\True}{\formula{A}}, just={\TRule{\False}{\lif}[3]}
[\sFmla{\False}{\formula{B}},
just={\TRule{\False}{\lif}[3]}, close]
]
]
]
]
]
\end{oltableau}
\end{ex}
\begin{ex}
We can give !!{tableau}s for any number of !!{signed formula}s as
assumptions. Often it is also necessary to apply more than one rule
that allows branching; and in general !!a{tableau} can have any number
of branches. For instance, consider !!a{tableau} for
$\{\sFmla{\True}{!A \lor (!B \land !C)}, \sFmla{\False}{(!A \lor !B) \land (!A
\lor !C)}\}$. We start by applying the $\TRule{\True}{\lor}$ to the
first assumption:
\begin{oltableau}
[\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
just=\TAss, checked
[\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
(\formula{A} \lor \formula{C})}, just=\TAss
[\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\lor}[1]}]
[\sFmla{\True}{\formula{B} \land \formula{C}},
just={\TRule{\True}{\lor}[1]}]
]
]
\end{oltableau}
Now we can apply the $\TRule{\False}{\land}$ rule to line~$2$. We do
this on both branches simultaneously, and can therefore check off
line~$2$:
\begin{oltableau}
[\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
just=\TAss, checked
[\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
(\formula{A} \lor \formula{C})}, just=\TAss, checked
[\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\lor}[1]}
[\sFmla{\False}{\formula{A} \lor \formula{B}},
just={\TRule{\False}{\land}[2]}]
[\sFmla{\False}{\formula{A} \lor \formula{C}},
just={\TRule{\False}{\land}[2]}]
]
[\sFmla{\True}{\formula{B} \land \formula{C}},
just={\TRule{\True}{\lor}[1]}
[\sFmla{\False}{\formula{A} \lor \formula{B}},
just={\TRule{\False}{\land}[2]}]
[\sFmla{\False}{\formula{A} \lor \formula{C}},
just={\TRule{\False}{\land}[2]}]
]
]
]
\end{oltableau}
Now we can apply $\TRule{\False}{\lor}$ to all the branches containing
$!A \lor !B$:
\begin{oltableau}
[\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
just=\TAss, checked
[\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
(\formula{A} \lor \formula{C})}, just=\TAss, checked
[\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\lor}[1]}
[\sFmla{\False}{\formula{A} \lor \formula{B}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}}, just={\TRule{\False}{\lor}[4]}
[\sFmla{\False}{\formula{B}},
just={\TRule{\False}{\lor}[4]}, close]
]
]
[\sFmla{\False}{\formula{A} \lor \formula{C}},
just={\TRule{\False}{\land}[2]}]
]
[\sFmla{\True}{\formula{B} \land \formula{C}},
just={\TRule{\True}{\lor}[1]}
[\sFmla{\False}{\formula{A} \lor \formula{B}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}}, just={\TRule{\False}{\lor}[4]}
[\sFmla{\False}{\formula{B}},
just={\TRule{\False}{\lor}[4]}]
]
]
[\sFmla{\False}{\formula{A} \lor \formula{C}},
just={\TRule{\False}{\land}[2]}]
]
]
]
\end{oltableau}
The leftmost branch is now closed. Let's now apply
$\TRule{\False}{\lor}$ to $!A \lor !C$:
\begin{oltableau}
[\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
just=\TAss, checked
[\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
(\formula{A} \lor \formula{C})}, just=\TAss, checked
[\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\lor}[1]}
[\sFmla{\False}{\formula{A} \lor \formula{B}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}},
just={\TRule{\False}{\lor}[4]}
[\sFmla{\False}{\formula{B}},
just={\TRule{\False}{\lor}[4]}, close]
]
]
[\sFmla{\False}{\formula{A} \lor \formula{C}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}},
just={\TRule{\False}{\lor}[4]}, move by=2
[\sFmla{\False}{\formula{C}},
just={\TRule{\False}{\lor}[4]}, close]
]
]
]
[\sFmla{\True}{\formula{B} \land \formula{C}},
just={\TRule{\True}{\lor}[1]}
[\sFmla{\False}{\formula{A} \lor \formula{B}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}},
just={\TRule{\False}{\lor}[4]}
[\sFmla{\False}{\formula{B}},
just={\TRule{\False}{\lor}[4]}
]
]
]
[\sFmla{\False}{\formula{A} \lor \formula{C}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}},
just={\TRule{\False}{\lor}[4]}, move by=2
[\sFmla{\False}{\formula{C}},
just={\TRule{\False}{\lor}[4]}]
]
]
]
]
]
\end{oltableau}
Note that we moved the result of applying $\TRule{\False}{\lor}$ a
second time below for clarity. In this instance it would not have been
needed, since the justifications would have been the same.
Two branches remain open, and $\sFmla{\True}{!B \land !C}$ on line~$3$
remains unchecked. We apply $\TRule{\True}{\land}$ to it to obtain a
closed !!{tableau}:
\begin{oltableau}
[\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
just=\TAss, checked
[\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
(\formula{A} \lor \formula{C})}, just=\TAss, checked
[\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\lor}[1]}
[\sFmla{\False}{\formula{A} \lor \formula{B}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}},
just={\TRule{\False}{\lor}[4]}
[\sFmla{\False}{\formula{B}},
just={\TRule{\False}{\lor}[4]}, close]
]
]
[\sFmla{\False}{\formula{A} \lor \formula{C}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}},
just={\TRule{\False}{\lor}[4]}
[\sFmla{\False}{\formula{C}},
just={\TRule{\False}{\lor}[4]}, close]
]
]
]
[\sFmla{\True}{\formula{B} \land \formula{C}},
just={\TRule{\True}{\lor}[1]}, checked
[\sFmla{\False}{\formula{A} \lor \formula{B}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}},
just={\TRule{\False}{\lor}[4]}
[\sFmla{\False}{\formula{B}},
just={\TRule{\False}{\lor}[4]}
[\sFmla{\True}{\formula{B}},
just={\TRule{\True}{\land}[3]}
[\sFmla{\True}{\formula{C}},
just={\TRule{\True}{\land}[3]},close
]
]
]
]
]
[\sFmla{\False}{\formula{A} \lor \formula{C}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}},
just={\TRule{\False}{\lor}[4]}
[\sFmla{\False}{\formula{C}},
just={\TRule{\False}{\lor}[4]}
[\sFmla{\True}{\formula{B}},
just={\TRule{\True}{\land}[3]}
[\sFmla{\True}{\formula{C}},
just={\TRule{\True}{\land}[3]},close
]
]
]
]
]
]
]
]
\end{oltableau}
For comparison, here's a closed !!{tableau} for the same set of
assumptions in which the rules are applied in a different order:
\begin{oltableau}
[\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
just=\TAss, checked
[\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
(\formula{A} \lor \formula{C})}, just=\TAss, checked
[\sFmla{\False}{\formula{A} \lor \formula{B}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}},
just={\TRule{\False}{\lor}[3]}
[\sFmla{\False}{\formula{B}},
just={\TRule{\False}{\lor}[3]}
[\sFmla{\True}{\formula{A}},
just={\TRule{\True}{\lor}[1]},close
]
[\sFmla{\True}{\formula{B} \land \formula{C}},
just={\TRule{\True}{\lor}[1]}, checked
[\sFmla{\True}{\formula{B}},
just={\TRule{\True}{\land}[6]}
[\sFmla{\True}{\formula{C}},
just={\TRule{\True}{\land}[6]},close
]
]
]
]
]
]
[\sFmla{\False}{\formula{A} \lor \formula{C}},
just={\TRule{\False}{\land}[2]}, checked
[\sFmla{\False}{\formula{A}},
just={\TRule{\False}{\lor}[3]}
[\sFmla{\False}{\formula{C}},
just={\TRule{\False}{\lor}[3]}
[\sFmla{\True}{\formula{A}},
just={\TRule{\True}{\lor}[1]},close
]
[\sFmla{\True}{\formula{B} \land \formula{C}},
just={\TRule{\True}{\lor}[1]}, checked
[\sFmla{\True}{\formula{B}},
just={\TRule{\True}{\land}[6]}
[\sFmla{\True}{\formula{C}},
just={\TRule{\True}{\land}[6]},close
]
]
]
]
]
]
]
]
\end{oltableau}
\end{ex}
\begin{prob}
Give closed !!{tableau}s of the following:
\begin{enumerate}
\item $\sFmla{\True}{!A \land (!B \land !C)}, \sFmla{\False}{(!A \land !B) \land !C}$.
\item $\sFmla{\True}{!A \lor (!B \lor !C)}, \sFmla{\False}{(!A \lor !B) \lor !C}$.
\item $\sFmla{\True}{!A \lif (!B \lif !C)}, \sFmla{\False}{!B \lif (!A \lif !C)}$.
\item $\sFmla{\True}{!A}, \sFmla{\False}{\lnot\lnot !A}$.
\end{enumerate}
\end{prob}
\begin{prob}
Give closed !!{tableau}s of the following:
\begin{enumerate}
\item $\sFmla{\True}{(!A \lor !B) \lif !C}, \sFmla{\False}{!A \lif !C}$.
\item $\sFmla{\True}{(!A \lif !C) \land (!B \lif !C)}, \sFmla{\False}{(!A \lor !B) \lif !C}$.
\item $\sFmla{\False}{\lnot(!A \land \lnot !A)}$.
\item $\sFmla{\True}{!B \lif !A}, \sFmla{\False}{\lnot !A \lif \lnot !B}$.
\item $\sFmla{\False}{(!A \lif \lnot !A) \lif \lnot !A}$.
\item $\sFmla{\False}{\lnot(!A \lif !B) \lif \lnot !B}$.
\item $\sFmla{\True}{!A \lif !C}, \sFmla{\False}{\lnot (!A \land \lnot !C)}$.
\item $\sFmla{\True}{!A \land \lnot !C}, \sFmla{\False}{\lnot (!A \lif !C)}$.
\item $\sFmla{\True}{!A \lor !B, \lnot !B}, \sFmla{\False}{!A}$.
TR012-SOURCE-FORMULA-006: The frozen exercise accidentally groups not B inside the preceding signed-formula argument. The reader preserves the printed source and explicitly presents the intended three separate signed assumptions.
\item $\sFmla{\True}{\lnot !A \lor \lnot !B}, \sFmla{\False}{\lnot(!A \land !B)}$.
\item $\sFmla{\False}{(\lnot !A \land \lnot !B) \lif\lnot(!A \lor !B)}$.
\item $\sFmla{\False}{\lnot(!A \lor !B) \lif (\lnot !A \land \lnot !B)}$.
\end{enumerate}
\end{prob}
\begin{prob}
Give closed !!{tableau}s of the following:
\begin{enumerate}
\item $\sFmla{\True}{\lnot(!A \lif !B)}, \sFmla{\False}{!A}$.
\item $\sFmla{\True}{\lnot(!A \land !B)}, \sFmla{\False}{\lnot !A \lor \lnot !B}$.
\item $\sFmla{\True}{!A \lif !B}, \sFmla{\False}{\lnot !A \lor !B}$.
\item $\sFmla{\False}{\lnot \lnot !A \lif !A}$.
\item $\sFmla{\True}{!A \lif !B}, \sFmla{\True}{\lnot !A \lif !B}, \sFmla{\False}{!B}$.
\item $\sFmla{\True}{(!A \land !B) \lif !C}, \sFmla{\False}{(!A \lif !C) \lor (!B \lif !C)}$.
\item $\sFmla{\True}{(!A \lif !B) \lif !A}, \sFmla{\False}{!A}$.
\item $\sFmla{\False}{(!A \lif !B) \lor (!B \lif !C)}$.
\end{enumerate}
\end{prob}
\end{document}

content/first-order-logic/tableaux/proof-theoretic-notions.tex

190 lines; SHA-256 bad25c1ba9db9de17f7c2ff5fffa2c4f9f00aa13d23c197e5337fe759d6fdd39. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: tableaux
% Section: proof-theoretic-notions
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{tab}{ptn}}
{\olfileid{pl}{tab}{ptn}}
\olsection{Proof-Theoretic Notions}
\begin{editorial}
This section collects the definitions of the provability relation
and consistency for tableaux.
\end{editorial}
\begin{explain}
Just as we've defined a number of important semantic notions
(validity, entailment, satisfiability), we now define corresponding
\emph{proof-theoretic notions}. These are not defined by appeal to
satisfaction of !!{sentence}s in !!{structure}s, but by appeal to the
existence of certain closed !!{tableau}x. It was an important
discovery that these notions coincide. That they do is the content of
the \emph{soundness} and \emph{completeness theorems}.
\end{explain}
\begin{defn}[Theorems]
A !!{sentence}~$!A$ is a \emph{theorem} if there is a closed
!!{tableau} for~$\sFmla{\False}{!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 set $\{!B_1, \dots, !B_n\} \subseteq \Gamma$
and a closed !!{tableau} for the set
\[
\{
\sFmla{\False}{!A},
\sFmla{\True}{!B_1}, \dots,
\sFmla{\True}{!B_n}
\}.
\]
If $!A$ is not !!{derivable} from $\Gamma$ we write $\Gamma \Proves/
!A$.
\end{defn}
\begin{defn}[Consistency]
A set of !!{sentence}s~$\Gamma$ is \emph{inconsistent} iff there is a
finite set $\{!B_1, \dots, !B_n\} \subseteq \Gamma$ and a closed
!!{tableau} for the set
\[
\{
\sFmla{\True}{!B_1}, \dots,
\sFmla{\True}{!B_n}
\}.
\]
If $\Gamma$ is not inconsistent, 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}
If $!A \in \Gamma$, $\{!A\}$ is a finite subset of~$\Gamma$ and the !!{tableau}
\begin{oltableau}
[\sFmla{\False}{\formula{A}}, just = \TAss
[\sFmla{\True}{\formula{A}}, just = \TAss,close]
]
\end{oltableau}
is closed.
\end{proof}
\begin{prop}[Monotonicity]
\ollabel{prop:monotonicity}
If $\Gamma \subseteq \Delta$ and $\Gamma \Proves !A$, then $\Delta
\Proves !A$.
\end{prop}
\begin{proof}
Any finite subset of~$\Gamma$ is also a finite subset of~$\Delta$.
\end{proof}
\begin{prop}[Transitivity]
\ollabel{prop:transitivity}
If $\Gamma \Proves !A$ and $\{!A\} \cup
\Delta \Proves !B$, then $\Gamma \cup \Delta \Proves !B$.
\end{prop}
\begin{proof}
If $\{!A\} \cup \Delta \Proves !B$, then there is a finite subset $\Delta_0 =
\{!C_1, \dots, !C_n\} \subseteq \Delta$ such that
\begin{align*}
\{\sFmla{\False}{!B}, & \sFmla{\True}{!A}, \sFmla{\True}{!C_1},
\dots, \sFmla{\True}{!C_n}\}
\intertext{has a closed !!{tableau}. If $\Gamma \Proves !A$ then there
are $!D_1$, \dots, $!D_m \subseteq \Gamma$ such that}
TR012-SOURCE-FORMULA-007: The reader preserves the printed D-sub-m subset relation as source MathML and explicitly identifies it as malformed. A separate reader projection gives the finite-family inclusion required by the surrounding derivability argument.
\{\sFmla{\False}{!A}, & \sFmla{\True}{!D_1},
\dots, \sFmla{\True}{!D_m}\}
\end{align*}
has a closed !!{tableau}.
Now consider the !!{tableau} with assumptions
\[
\sFmla{\False}{!B},
\sFmla{\True}{!C_1}, \dots, \sFmla{\True}{!C_n},
\sFmla{\True}{!D_1}, \dots, \sFmla{\True}{!D_m}.
\]
Apply the \Cut{} rule on~$!A$. This generates two branches, one has
$\sFmla{\True}{!A}$ in it, the other $\sFmla{\False}{!A}$. Thus,
on the one branch, all of
\[
\{\sFmla{\False}{!B}, \sFmla{\True}{!A},
\sFmla{\True}{!C_1}, \dots, \sFmla{\True}{!C_n}\}
\]
are available. Since there is a closed !!{tableau} for these
assumptions, we can attach it to that branch; every branch through
$\sFmla{\True}{!A}$ closes. On the other branch, all of
\[
\{\sFmla{\False}{!A}, \sFmla{\True}{!D_1}, \dots,
\sFmla{\True}{!D_m}\}
\]
are available, so we can also complete the other side to obtain a
closed !!{tableau}. 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}
\tagprob{FOL}
\begin{prob}
Prove \olref[fol][tab][ptn]{prop:incons}
\end{prob}
\tagendprob
\tagprob{notFOL}
\begin{prob}
Prove \olref[pl][tab][ptn]{prop:incons}
\end{prob}
\tagendprob
\begin{prop}[Compactness]
\ollabel{prop:proves-compact}
\begin{enumerate}
\item If $\Gamma \Proves !A$ then there is a finite subset $\Gamma_0
\subseteq \Gamma$ such that $\Gamma_0 \Proves !A$.
\item If every finite subset of~$\Gamma$ is
consistent, then $\Gamma$ is consistent.
\end{enumerate}
\end{prop}
\begin{proof}
\begin{enumerate}
\item If $\Gamma \Proves !A$, then there is a finite subset
$\Gamma_0 = \{!B_1, \dots, !B_n\}$ and a closed !!{tableau} for
\[
\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
\]
This !!{tableau} also shows $\Gamma_0 \Proves !A$.
\item If $\Gamma$ is inconsistent, then for some finite subset
$\Gamma_0 = \{!B_1, \dots, !B_n\}$ there is a closed !!{tableau}
for
\[
\{\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
\]
This closed !!{tableau} shows that $\Gamma_0$ is inconsistent.
\end{enumerate}
\end{proof}
\end{document}

content/first-order-logic/tableaux/provability-consistency.tex

150 lines; SHA-256 6d159d1c93f6b4bb24cf3d16e7f18096e15881679ef5f64db5b25cee57cccdef. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: tableaux
% Section: provability-consistency
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{tab}{prv}}
{\olfileid{pl}{tab}{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 = \{!B_1, \dots, !B_n\}$ and $\Gamma_1
=\{!C_1, \dots, !C_n\} \subseteq \Gamma$ such that
TR012-SOURCE-FORMULA-001: The frozen source first writes Gamma sub one as C sub one through C sub n, then uses C sub one through C sub m in the next display. The reader preserves both indices and discloses the mismatch.
\begin{align*}
\{\sFmla{\False}{!A}, &
\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\} \\
\{\sFmla{\True}{!A}, &
\sFmla{\True}{!C_1}, \dots, \sFmla{\True}{!C_m}\}
TR012-SOURCE-FORMULA-001: The frozen source first writes Gamma sub one as C sub one through C sub n, then uses C sub one through C sub m in the next display. The reader preserves both indices and discloses the mismatch.
\end{align*}
have closed !!{tableau}s. Using the \Cut{} rule on $!A$ we can
combine these into a single closed !!{tableau} that shows $\Gamma_0
\cup \Gamma_1$ is inconsistent. 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 closed !!{tableau} for
\[
\{\sFmla{\False}{!A},
\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
\]
Using the $\TRule{\True}{\lnot}$ rule, this can be turned into a
closed !!{tableau} for
\[
\{\sFmla{\True}{\lnot !A},
\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}.
\]
On the other hand, if there is a closed !!{tableau} for the latter, we
can turn it into a closed !!{tableau} of the former by removing every
formula that results from \TRule{\True}{\lnot} applied to the first
assumption~$\sFmla{\True}{\lnot !A}$ as well as that assumption, and
adding the assumption $\sFmla{\False}{!A}$. For if a branch was closed
before because it contained the conclusion of \TRule{\True}{\lnot}
applied to $\sFmla{\True}{\lnot !A}$, i.e., $\sFmla{\False}{!A}$, the
corresponding branch in the new !!{tableau} is also closed. If a
branch in the old tableau was closed because it contained the
assumption $\sFmla{\True}{\lnot !A}$ as well as $\sFmla{\False}{\lnot
!A}$ we can turn it into a closed branch by applying
$\TRule{\False}{\lnot}$ to $\sFmla{\False}{\lnot !A}$ to obtain
$\sFmla{\True}{!A}$. This closes the branch since we added
$\sFmla{\False}{!A}$ as an assumption.
\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
are $!B_1$, \dots, $!B_n \in \Gamma$ such that \
\[
\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
\]
has a closed tableau. Replace the assumption \sFmla{\False}{!A} by
TR012-SOURCE-PROOF-005: The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering.
\sFmla{\True}{\lnot !A}, and insert the conclusion of
TR012-SOURCE-PROOF-005: The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering.
\TRule{\True}{\lnot} applied to \sFmla{\False}{!A} after the
TR012-SOURCE-PROOF-005: The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering.
assumptions. Any !!{sentence} in the !!{tableau} justified by appeal
TR012-SOURCE-PROOF-005: The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering.
to line~$1$ in the old !!{tableau} is now justified by appeal to
TR012-SOURCE-PROOF-005: The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering.
line~$n+1$. So if the old !!{tableau} was closed, the new one is.
TR012-SOURCE-PROOF-005: The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering.
It shows that $\Gamma$ is inconsistent, since all assumptions are
in~$\Gamma$.
\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}
If there are $!B_1$, \dots, $!B_n \in \Gamma$ and $!C_1$, \dots,
$!C_m \in \Gamma$ such that
\begin{align*}
\{\sFmla{\True}{!A}, &
\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\} \text{ and}\\
\{\sFmla{\True}{\lnot !A}, &
\sFmla{\True}{!C_1}, \dots, \sFmla{\True}{!C_m}\}
\end{align*}
both have closed !!{tableau}s, we can construct a single, combined
!!{tableau} that shows that $\Gamma$ is inconsistent by using as
assumptions $\sFmla{\True}{!B_1}$, \dots, $\sFmla{\True}{!B_n}$
together with $\sFmla{\True}{!C_1}$, \dots, $\sFmla{\True}{!C_m}$,
followed by an application of the \Cut{} rule. This yields two
branches, one starting with $\sFmla{\True}{!A}$, the other with
$\sFmla{\False}{!A}$.
On the left left side, add the part of the first
TR012-SOURCE-PROSE-002: The reader removes the duplicated word in the source phrase 'left left.'
!!{tableau} below its assumptions. Here, every rule application is still
correct, since each of the assumptions of the first !!{tableau},
including $\sFmla{\True}{!A}$, is available. Thus, every branch
below $\sFmla{\True}{!A}$ closes.
On the right side, add the part of the second !!{tableau} below its
assumption, with the results of any applications
of~$\TRule{\True}{\lnot}$ to $\sFmla{\True}{\lnot !A}$ removed. The
conclusion of $\TRule{\True}{\lnot}$ to $\sFmla{\True}{\lnot !A}$ is
$\sFmla{\False}{!A}$, which is nevertheless available, as it is the
conclusion of the \Cut{} rule on the right side of the combined !!{tableau}.
If a branch in the second tableau was closed because it contained
the assumption $\sFmla{\True}{\lnot !A}$ (which no longer appears as
an assumption in the combined !!{tableau}) as well as
$\sFmla{\False}{\lnot !A}$, we can applying $\TRule{\False}{\lnot}$
TR012-SOURCE-PROSE-003: The reader corrects the source phrase 'we can applying' to 'we can apply.'
to $\sFmla{\False}{\lnot !A}$ to obtain $\sFmla{\True}{!A}$. Now the
corresponding branch in the combined !!{tableau} also closes,
because it contains the right-hand conclusion of the \Cut{} rule,
$\sFmla{\False}{!A}$. If a branch in the second !!{tableau} closed
for any other reason, the corresponding branch in the combined
!!{tableau} also closes, since any !!{signed formula}s other than
$\sFmla{\True}{\lnot !A}$ occurring on the branch in the old, second
!!{tableau} also occur on the corresponding branch in the combined
!!{tableau}.
\end{proof}
\end{document}

content/first-order-logic/tableaux/provability-propositional.tex

175 lines; SHA-256 5df9f0cf1b10689babb2051daad6426e2abee00e55001f14a896d1a37ae30446. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: tableaux
% 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}{tab}{ppr}}
{\olfileid{pl}{tab}{ppr}}
\olsection{\usetoken{S}{derivability} and the Propositional Connectives}
\begin{explain}
We establish that the !!{derivability} relation~$\Proves$ of
tableaux 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 $\{\sFmla{\False}{!A}, \sFmla{\True}{!A \land !B}\}$ and
$\{\sFmla{\False}{!B}, \sFmla{\True}{!A \land !B}\}$ have closed
!!{tableau}s
\begin{oltableau}{}
[\sFmla{\False}{\formula{A}}, just=\TAss
[\sFmla{\True}{\formula{A} \land \formula{B}}, just=\TAss
[\sFmla{\True{\formula{A}}},just={\TRule{\True}{\land}[2]}
TR012-SOURCE-TABLEAU-004: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.
[\sFmla{\True{\formula{B}}},just={\TRule{\True}{\land}[2]}, close
TR012-SOURCE-TABLEAU-004: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.
]
]
]
]
\end{oltableau}
\begin{oltableau}{}
[\sFmla{\False}{\formula{B}}, just=\TAss
[\sFmla{\True}{\formula{A} \land \formula{B}}, just=\TAss
[\sFmla{\True{\formula{A}}},just={\TRule{\True}{\land}[2]}
TR012-SOURCE-TABLEAU-004: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.
[\sFmla{\True{\formula{B}}},just={\TRule{\True}{\land}[2]}, close
TR012-SOURCE-TABLEAU-004: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.
]
]
]
]
\end{oltableau}
\item Here is a closed !!{tableau} for $\{\sFmla{\True}{!A},
\sFmla{\True}{!B}, \sFmla{\False}{!A \land !B}\}$:
\begin{oltableau}
[\sFmla{\False}{\formula{A} \land \formula{B}}, just = \TAss
[\sFmla{\True}{\formula{A}}, just = \TAss
[\sFmla{\True}{\formula{B}}, just=\TAss
[\sFmla{\False}{\formula{A}}, just = {\TRule{\False}{\land}[1]}, close]
[\sFmla{\False}{\formula{B}}, just = {\TRule{\False}{\land}[1]}, close]
]
]
]
\end{oltableau}
\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 closed !!{tableau} of $\{\sFmla{\True}{!A \lor !B},
\sFmla{\True}{\lnot !A}, \sFmla{\True}{\lnot !B}\}$:
\begin{oltableau}
[\sFmla{\True}{\formula{A} \lor \formula{B}}, just = \TAss
[\sFmla{\True}{\lnot \formula{A}}, just = \TAss
[\sFmla{\True}{\lnot \formula{B}}, just = \TAss
[\sFmla{\False}{\formula{A}}, just = {\TRule{\True}{\lnot}[2]}
[\sFmla{\False}{\formula{B}}, just = {\TRule{\True}{\lnot}[3]}
[\sFmla{\True}{\formula{A}}, just = {\TRule{\True}{\lor}[1]}, close]
[\sFmla{\True}{\formula{B}}, just = {\TRule{\True}{\lor}[1]}, close]
]
]
]
]
]
\end{oltableau}
\item Both $\{\sFmla{\False}{!A \lor !B}, \sFmla{\True}{!A}\}$ and
$\{\sFmla{\False}{!A \lor !B}, \sFmla{\True}{!B}\}$ have closed
!!{tableau}s:
\begin{oltableau}{}
[\sFmla{\False}{\formula{A} \lor \formula{B}}, just=\TAss
[\sFmla{\True}{\formula{A}}, just=\TAss
[\sFmla{\False{\formula{A}}},just={\TRule{\False}{\lor}[1]}
TR012-SOURCE-TABLEAU-004: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.
[\sFmla{\False{\formula{B}}},just={\TRule{\False}{\lor}[1]}, close
TR012-SOURCE-TABLEAU-004: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.
]
]
]
]
\end{oltableau}
\begin{oltableau}{}
[\sFmla{\False}{\formula{A} \lor \formula{B}}, just=\TAss
[\sFmla{\True}{\formula{B}}, just=\TAss
[\sFmla{\False{\formula{A}}},just={\TRule{\False}{\lor}[1]}
TR012-SOURCE-TABLEAU-004: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.
[\sFmla{\False{\formula{B}}},just={\TRule{\False}{\lor}[1]}, close
TR012-SOURCE-TABLEAU-004: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.
]
]
]
]
\end{oltableau}
\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 $\{\sFmla{\False}{!B}, \sFmla{\True}{!A \lif !B},
\sFmla{\True}{!A}\}$ has a closed !!{tableau}:
\begin{oltableau}
[\sFmla{\False}{\formula{B}}, just=\TAss
[\sFmla{\True}{\formula{A} \lif \formula{B}}, just=\TAss
[\sFmla{\True}{\formula{A}}, just=\TAss
[\sFmla{\False}{\formula{A}}, just = {\TRule{\True}{\lif}[2]}, close]
[\sFmla{\True}{\formula{B}}, just = {\TRule{\True}{\lif}[2]}, close]
]
]
]
\end{oltableau}
\item Both $\{\sFmla{\False}{!A \lif !B},
\sFmla{\True}{\lnot !A}\}$ and $\{\sFmla{\False}{!A \lif !B},
\sFmla{\True}{!B}\}$ have closed !!{tableau}s:
\begin{oltableau}
[\sFmla{\False}{\formula{A} \lif \formula{B}}, just = \TAss
[\sFmla{\True}{\lnot \formula{A}}, just = \TAss
[\sFmla{\True}{\formula{A}}, just = {\TRule{\False}{\lif}[1]}
[\sFmla{\False}{\formula{B}}, just = {\TRule{\False}{\lif}[1]}
[\sFmla{\False}{\formula{A}}, just = {\TRule{\True}{\lnot}[2]}, close]
]
]
]
]
\end{oltableau}
\begin{oltableau}
[\sFmla{\False}{\formula{A} \lif \formula{B}}, just = \TAss
[\sFmla{\True}{\formula{B}}, just = \TAss
[\sFmla{\True}{\formula{A}}, just = {\TRule{\False}{\lif}[1]}
[\sFmla{\False}{\formula{B}}, just = {\TRule{\False}{\lif}[1]},close
]
]
]
]
\end{oltableau}
\end{enumerate}
\end{proof}
\end{document}

content/first-order-logic/tableaux/soundness.tex

240 lines; SHA-256 49f119364f19485fa74c0c18e849f20b746e8edec9fdccb9e98a8aff7250a744. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: tableaux
% Section: soundness.tex
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{tab}{sou}}
{\olfileid{pl}{tab}{sou}}
\olsection{Soundness}
\begin{explain}
!!^a{derivation} system, such as tableaux, 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 closed
!!{tableau}s of some kind or other, proving (1)--(3) above requires
proving something about the semantic properties of closed
!!{tableau}s. We will first define what it means for !!a{signed
formula} to be satisfied in a structure, and then show that if a
!!{tableau} is closed, no structure satisfies all its assumptions.
(1)--(3) then follow as corollaries from this result.
\end{explain}
\begin{defn}
\iftag{FOL}{!!^a{structure}}{!!^a{valuation}}~$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$
\emph{satisfies} !!a{signed formula} $\sFmla{\True}{!A}$ iff
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$, and it satisfies
$\sFmla{\False}{!A}$ iff
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A}$. $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$
satisfies a set of !!{signed formula}s~$\Gamma$ iff it satisfies every
$\sFmla{S}{!A} \in \Gamma$. $\Gamma$~is \emph{satisfiable} if there is
\iftag{FOL}{!!a{structure}}{!!a{valuation}} that satisfies it, and
\emph{unsatisfiable} otherwise.
\end{defn}
\begin{thm}[Soundness]
\ollabel{thm:tableau-soundness}
If $\Gamma$ has a closed !!{tableau}, $\Gamma$ is unsatisfiable.
\end{thm}
\begin{proof}
Let's call a branch of !!a{tableau} satisfiable iff the set of
!!{signed formula}s on it is satisfiable, and let's call !!a{tableau}
satisfiable if it contains at least one satisfiable branch.
We show the following: Extending a satisfiable !!{tableau} by one of
the rules of inference always results in a satisfiable !!{tableau}.
This will prove the theorem: any closed !!{tableau} results by
applying rules of inference to the !!{tableau} consisting only of
assumptions from~$\Gamma$. So if $\Gamma$ were satisfiable, any
!!{tableau} for it would be satisfiable. A closed !!{tableau},
however, is clearly not satisfiable: every branch contains both
$\sFmla{\True}{!A}$ and $\sFmla{\False}{!A}$, and no structure can
both satisfy and not satisfy~$!A$.
Suppose we have a satisfiable !!{tableau}, i.e., !!a{tableau} with at
least one satisfiable branch. Applying a rule of inference either adds
!!{signed formula}s to a branch, or splits a branch in two. If the
!!{tableau} has a satisfiable branch which is not extended by the rule
application in question, it remains a satisfiable branch in the
extended !!{tableau}, so the extended tableau is satisfiable. So we
only have to consider the case where a rule is applied to a
satisfiable branch.
Let $\Gamma$ be the set of !!{signed formula}s on that branch, and
let $\sFmla{S}{!A} \in \Gamma$ be the !!{signed formula} to which the
rule is applied. If the rule does not result in a split branch, we
have to show that the extended branch, i.e., $\Gamma$ together with
the conclusions of the rule, is still satisfiable. If the rule results
in a split branch, we have to show that at least one of the two
resulting branches is satisfiable.
First, we consider the possible inferences that do not result in a split branch.
\begin{enumerate}
\item The branch is expanded by applying $\TRule{\True}{\lnot}$ to
$\sFmla{\True}{\lnot !B} \in \Gamma$. Then the extended branch
contains the !!{signed formula}s $\Gamma \cup
\{\sFmla{\False}{!B}\}$. Suppose
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$. In particular,
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\lnot !B}$. Thus,
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$, i.e.,
$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies
$\sFmla{\False}{!B}$.
\item The branch is expanded by applying $\TRule{\False}{\lnot}$ to
$\sFmla{\False}{\lnot !B} \in \Gamma$: Exercise.
\item The branch is expanded by applying $\TRule{\True}{\land}$ to
$\sFmla{\True}{!B \land !C} \in \Gamma$, which results in two new
!!{signed formula}s on the branch: $\sFmla{\True}{!B}$ and
$\sFmla{\True}{!C}$. Suppose
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, in particular
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B \land !C}$. Then
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ and
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$. This means that
$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies both
$\sFmla{\True}{!B}$ and $\sFmla{\True}{!C}$.
\item The branch is expanded by applying $\TRule{\False}{\lor}$ to
$\sFmla{\False}{!B \lor !C} \in \Gamma$: Exercise.
\item The branch is expanded by applying $\TRule{\False}{\lif}$ to
$\sFmla{\False}{!B \lif !C} \in \Gamma$: This results in two new
!!{signed formula}s on the branch: $\sFmla{\True}{!B}$ and
$\sFmla{\False}{!C}$. Suppose
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, in particular
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B \lif !C}$. Then
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ and
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$. This means that
$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies both
$\sFmla{\True}{!B}$ and $\sFmla{\False}{!C}$.
\iftag{FOL}{%
\item The branch is expanded by applying $\TRule{\True}{\lforall}$ to
$\sFmla{\True}{\lforall[x][!B(x)]} \in \Gamma$: This results in a
new !!{signed formula}~$\sFmla{\True}{!A(t)}$ on the branch.
Suppose $\Sat{M}{\Gamma}$, in particular,
$\Sat{M}{\lforall[x][!A(x)]}$. By
\olref[syn][sem]{prop:quant-terms}, $\Sat{M}{!A(t)}$. Consequently,
$\Struct{M}$ satisfies $\sFmla{\True}{!A(t)}$.
\item The branch is expanded by applying $\TRule{\False}{\lforall}$ to
$\sFmla{\False}{\lforall[x][!B(x)]} \in \Gamma$: This results in a
new !!{signed formula}~$\sFmla{\False}{!A(a)}$ where $a$ is
!!a{constant} not occurring in~$\Gamma$. Since $\Gamma$ is
satisfiable, there is a $\Struct{M}$ such that $\Sat{M}{\Gamma}$, in
particular $\Sat/{M}{\lforall[x][!B(x)]}$. We have to show that
$\Gamma \cup \{\sFmla{\False}{!A(a)}\}$ is satisfiable. To do this,
we define a suitable~$\Struct{M'}$ as follows.
By \olref[syn][ass]{prop:sat-quant}, $\Sat/{M}{\lforall[x][!B(x)]}$
iff for some $s$, $\Sat/{M}{!B(x)}[s]$. Now let $\Struct{M'}$ be
just like $\Struct{M}$, except $\Assign{a}{M'} = s(x)$. By
\olref[syn][ext]{cor:extensionality-sent}, for any
$\sFmla{\True}{!C} \in \Gamma$, $\Sat{M'}{!C}$, and for any
$\sFmla{\False}{!C} \in \Gamma$, $\Sat/{M'}{!C}$, since $a$ does not
occur in~$\Gamma$.
By \olref[syn][ext]{prop:extensionality}, $\Sat/{M'}{!A(x)}[s]$. By
\olref[syn][ext]{prop:ext-formulas}, $\Sat/{M'}{!A(a)}[s]$. Since
$!A(a)$ is !!a{sentence}, by
\olref[syn][ass]{prop:sentence-sat-true}, $\Sat/{M'}{!A(a)}$, i.e.,
$\Struct{M'}$ satisfies $\sFmla{\False}{!A(a)}$.
\item The branch is expanded by applying $\TRule{\True}{\lexists}$ to
$\sFmla{\True}{\lexists[x][!B(x)]} \in \Gamma$: Exercise.
\item The branch is expanded by applying $\TRule{\False}{\lexists}$ to
$\sFmla{\False}{\lexists[x][!B(x)]} \in \Gamma$: Exercise.}{}
\end{enumerate}
Now let's consider the possible inferences that result in a split branch.
\begin{enumerate}
\item The branch is expanded by applying $\TRule{\False}{\land}$ to
$\sFmla{\False}{!B \land !C} \in \Gamma$, which results in two
branches, a left one continuing through $\sFmla{\False}{!B}$ and a
right one through $\sFmla{\False}{!C}$. Suppose
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, in particular
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B \land !C}$. Then
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$ or
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$. In the former case,
$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies
$\sFmla{\False}{!B}$, i.e., $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$
satisfies the formulas on the left branch. In the latter,
$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies
$\sFmla{\False}{!C}$, i.e., $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$
satisfies the formulas on the right branch.
\item The branch is expanded by applying $\TRule{\True}{\lor}$ to
$\sFmla{\True}{!B \lor !C} \in \Gamma$: Exercise.
\item The branch is expanded by applying $\TRule{\True}{\lif}$ to
$\sFmla{\True}{!B \lif !C} \in \Gamma$: Exercise.
\item The branch is expanded by \Cut: This results in two branches,
one containing $\sFmla{\True}{!B}$, the other containing
$\sFmla{\False}{!B}$. Since $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$
and either $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ or
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$,
$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies either the left or
the right branch.
\end{enumerate}
\end{proof}
\tagprob{FOL}
\begin{prob}
Complete the proof of \olref[fol][tab][sou]{thm:tableau-soundness}.
\end{prob}
\tagendprob
\tagprob{notFOL}
\begin{prob}
Complete the proof of \olref[pl][tab][sou]{thm:tableau-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 $!B_1$, \dots, $!B_n \in
\Gamma$, $\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots,
\sFmla{\True}{!B_n}\}$ has a closed !!{tableau}. By
\olref{thm:tableau-soundness}, every
\iftag{FOL}{!!{structure}}{!!{valuation}}~$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$
either makes some $!B_i$ 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 are $!B_1$, \dots, $!B_n \in \Gamma$ and a closed
!!{tableau} for $\{\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}$. By
\olref{thm:tableau-soundness}, there is no
$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ such that
$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B_i}$ for all $i=1$, \dots,~$n$. But
then $\Gamma$ is not satisfiable.
\end{proof}
\end{document}