edl-tablmeta.tex

%!TEX root = edl.tex

\section{Derivations and Semantic Arguments}

At the beginning of the previous chapter, we mentioned a number of considerations that motivate the development of formal object language derivation systems. Now that we have an example of such a system for \lone, we may reflect on how it compares to evaluating arguments by directly discussing \lone-structures.

One thing to note is that the tableau system can be considerably more efficient. Consider this argument: $$(P \wedge (Q_{1} \wedge (Q_{2} \wedge (Q_{3} \wedge (Q_{4} \wedge Q_{5})))) \vdash (P \vee (R_{1} \vee (R_{2} \vee (R_{3} \vee (R_{4} \vee R_{5})))).$$  We can see the tableau derivation demonstrating the correctness of this claim in \autoref{fig:short} closes vey quickly. Even if we finish the tableau by applying the conjunction and negated disjunction rules repeatedly, the whole thing will be fewer than 30 lines.

\begin{figure}[t]
	\centering 
	{
\leaf{$P$\\ $(Q_{1} \wedge (Q_{2} \wedge (Q_{3} \wedge (Q_{4} \wedge Q_{5})))$\\ $¬P$ \\ $¬(R_{1} \vee (R_{2} \vee (R_{3} \vee (R_{4} \vee R_{5})))$\\ $\otimes$}
\branch{1}{$P \wedge (Q_{1} \wedge (Q_{2} \wedge (Q_{3} \wedge (Q_{4} \wedge Q_{5}))))$\\ $¬(P \vee (R_{1} \vee (R_{2} \vee (R_{3} \vee (R_{4} \vee R_{5}))))$}
\qobitree	}\caption{A brief tableau. \label{fig:short}}
\end{figure}

It is easy to see – by giving a semantic argument that basically parallels this tableau derivation – that this argument is a valid entailment. But demonstrating this via truth tables would involve a truth table of $2^{11} = 2048$ rows, which is prohibitively unwieldy. The tableau procedure is no less mechanical than the truth table procedure, but is considerably more efficient in this case.

On the other hand, consider an invalid argument like $$(P \vee (¬P \vee (¬¬P \vee (¬¬¬P \vee ¬¬¬¬P)))) \nvDash (P \wedge (¬P \wedge (¬¬P \wedge (¬¬¬P \wedge ¬¬¬¬P)))).$$ The truth table is two lines, on each of which the premise is true and the conclusion false. But the tableau, with its many uses of the disjunction and negated conjunction rules, branches extensively and is much less convenient to work with. 

This pattern is fairly representative. To show an argument invalid, we need to demonstrate the existence of just one structure in which the premises are true and the conclusion false. But checking invalidity by the construction of an attempted derivation involves the construction of a finished open tableau. In bad cases, this construction will take a long time to complete. To show an argument valid involves demonstrating the non-existence of a counterexample structure, which may require consideration of a great many structures. But a direct derivation of the conclusion from the premises may be more efficient.

We cannot yet recommend that we use semantic techniques to demonstrate invalidity, and formal derivations to demonstrate validity. This is because we do not yet know whether \emph{every} valid argument has a corresponding derivation; nor do we know whether \emph{every} derivation corresponds to a valid argument. It turns out that every valid argument is derivable, and every correctly constructed derivation can be associated with a valid argument. Both of these facts will be proved later in this chapter (\autoref{sec:tsoundcomp}), when we discuss the soundness and completeness of the tableau derivation system with respect to the semantics of \lone. 


\section{Transforming Derivations} % (fold)

Sometimes when we have a tableau derivation, we can use purely formal manipulations on the tree to construct other derivations. While trees can and do have other trees occuring within them (Def. \ref{def:occurswithin}), the trees which occur within a given tableau will always not meet the conditions for being a tableau themselves. But often simple modifications will enable us to convert one tableau into another, taking sub-trees of a tableau and re-using them in a new tableau. 

\paragraph{Structural Rules} We proved some structural rules for $\vDash$ (\autoref{twostruct}). We can show that analogous rules apply to $\vdash$. (I leave the demonstration of weakening for an exercise.) \begin{theorem}[$\vdash$ Permutation]
	$\Gamma, \psi, \chi, \Delta \vdash \phi$ iff\, $\Gamma, \chi, \psi, \Delta \vdash \phi$. \begin{proof}
	Immediate consequence of \autoref{thmorder}.
	\end{proof}
\end{theorem}
\begin{theorem}[$\vdash$ Contraction]
$\Gamma, \psi, \psi \vdash \phi$ iff\, $\Gamma, \psi \vdash \phi$. \begin{proof}
$\Gamma, \psi, \psi \vdash \phi$ iff there is a finished closed tableau generated by some finite set $\Sigma \cup \{\psi, \psi, ¬\phi\}$, where $\Sigma\subseteq \Gamma$. But any tableau generated by $\Sigma \cup \{\psi,\psi,¬\phi\}$ is generated by $\Sigma\cup \{\psi,¬\phi\}$, and vice versa, because those generating sets are identical (Def. \ref{def:gentabl}). 
\end{proof}
\end{theorem}


\paragraph{Syntactic Deduction} Just as we proved the deduction theorem (\autoref{ded}) for the semantic turnstile, we can prove a syntactic deduction theorem for the syntactic turnstile.
\begin{theorem}[Syntactic Deduction]\label{thm:sdt} $\Gamma, \phi\vdash \psi$ iff\, $\Gamma \vdash \phi \to \psi$. \begin{proof} \emph{If:} Assume $\Gamma \vdash \phi \to \psi$. Then there is at least one finite set $\Sigma$, a subset of $\Gamma$, such that every finished tableau $\mathbf{T}$ which is generated by $\Sigma \cup\{\neg(\phi \to \psi)\}$ is closed. Take one such tableau, where the first tableau rule applied was the negated conditional rule (\autoref{fig:stableaux}\subref{sf:nc}), so that each branch of the tableau begins $\langle \gamma_{1},\ldots,\gamma_{n}, \neg (\phi \to \psi), \phi, \neg \psi\rangle$, where each $\gamma_{i}\in \Sigma \subseteq \Gamma$. We have already dealt with $\neg (\phi \to \psi)$, so the sentences which close every branch on this tableau derive from $\Sigma$ or from $\phi$ or $\neg \psi$. Hence, we can construct a closed tableau where every branch begins $\langle \gamma_{1},\ldots,\gamma_{n}, \phi, \neg \psi\rangle$; hence some finite subset of $\Gamma\cup \{\phi, \neg \psi\}$ generates a closed tableau, hence $\Gamma, \phi \vdash \psi$. The only interesting case is if the original tableau had a branch which closed because of the presence of $(\phi \to \psi)$ on it. But then an application of the branching conditional rule to that node gives one branch with $\neg\phi$ occurring on it, which closes since $\phi$ occurs in the trunk;  and another branch with $\psi$ occurring on it, which closes since $\neg \psi$ occurs in the trunk. 

\noindent\emph{Only if:} We assume that $\Gamma, \phi \vdash \psi$. Then there is a closed finished tableaux that is generated by a finite subset of $\Gamma\cup \{\phi, \neg \psi\}$. If we modify this tableau by inserting $\neg(\phi \to \psi)$ above $\phi$ on every branch, the modified tree is closed also. Since $\phi$ and $\neg \psi$ can come from $\neg (\phi \to \psi)$ (\autoref{fig:stableaux}\subref{sf:nc}), this modified tree in fact satisfies the conditions for being a tableau. Since the original tableau is finished, and the modified tableau contains the results of applying tableau rules to the only new node, this is a finished tableau generated by  a finite subset of $\{\Gamma, \neg(\phi \to \psi)\}$, which means that $\Gamma \vdash \phi \to \psi$.
\end{proof}\end{theorem}

Now I'll prove some lemmas preliminary to proving a historically important theorem, Cut (\autoref{cut}). All of the following four lemmas involve showing that some tableau derivations can be converted into other tableau derivations, in such a way that the syntactic derivability mirrors what is intuitively provable in virtue of the meaning of the  sentences involved. 

\begin{lemma} \label{switch}
	$\Gamma \vdash \phi$ iff\, $\Gamma, \neg\phi \vdash$.
\end{lemma}
\begin{proof}
	$\Gamma \vdash \phi$ iff there exists a finite set $\Sigma\subseteq \Gamma$ such that there is a finished closed tableau generated by $\Sigma \cup\{\neg\phi\}$. This holds in turn iff $\Sigma\cup\{\neg\phi\}$ is inconsistent (by Definition~\ref{defcontab}).
\end{proof}
\begin{lemma} \label{dne}
	$\Gamma, \neg\neg\phi \vdash$ iff\, $\Gamma,\phi \vdash$.
\end{lemma}
\begin{proof}
\noindent\emph{Only If:}
	If $\Gamma, \neg\neg\phi \vdash$, there is a finished closed tableau generated by  $\Sigma \cup \{\neg\neg\phi\}$, where $\Sigma$ is a finite subset of $\Gamma$. Take such a tableau in which the first rule applied to the generating set was the $\neg\neg$ rule (\autoref{fig:stableaux}\subref{sf:dn}). Remove the node containing $\neg\neg\phi$: the tableau will still be closed. Why? Either  $\Sigma$ itself already contained some sentence and its negation; or the tableau closed because of some application of a tableau rule to $\phi$ (the result of applying the double negation rule to $\neg\neg\phi$); or the tableau closed because $\neg\neg\phi$ and its negation occurred on the tableau. In the first two cases, it is obvious that removing $\neg\neg\phi$ made no difference to whether the tableau is closed. So consider the third case. There are two subcases: either $\neg\neg\neg\phi$ occurs on the tableau, or $\neg\phi$ does (both are negations of $\neg\neg\phi$). If the latter, the tableau is closed because both $\phi$ and $\neg\phi$ occur. If the former, since the tableau is finished, some application of the double negation rule was made to $\neg\neg\neg\phi$ at some stage, so that $\neg\phi$ occurs as well as $\phi$, again closing the relevant branch.

	\noindent\emph{If:} If $\Gamma, \phi \vdash$, there is a finished closed tableau generated by $\Sigma\cup\{\phi\}$. Modify this tableau by inserting $¬¬\phi$ above the node containing $\phi$. The resulting tree remains closed; it also satisfies the conditions for being a tableau generated by $\Sigma\cup\{¬¬\phi\}$, since $\phi$ comes from an earlier node by application of the double negation rule. So $\Gamma, ¬¬\phi\vdash$.
\end{proof}


\begin{lemma} \label{negcon}
	If\, $\Gamma \vdash \neg(\phi \wedge\psi)$ then\, $\Gamma, \phi \vdash \neg\psi$.
\end{lemma}
\begin{proof}
	If $\Gamma \vdash \neg(\phi \wedge\psi)$, then there is a finite $\Sigma\subseteq \Gamma$ such that every finished tableau generated by $\Sigma \cup \{¬¬(\phi\wedge\psi)\}$ is closed, and by Lemma \ref{dne}, so too is every finished tableau generated by $\Sigma \cup \{\phi\wedge\psi\}$. Consider such a tableau in which the first rule applied was the conjunction rule (\autoref{fig:stableaux}\subref{sf:and}); this is also a finished closed tableau generated by $\Sigma \cup \{\phi\wedge\psi,\phi,\psi\}$. Remove the node containing $\phi\wedge\psi$, and the resulting tree remains a closed  tableau. Either the tableau is closed because of the results of applying the tableau rules to $\phi$ and $\psi$; or some branch of the tableau is closed because it contains $\neg(\phi\wedge\psi)$. But, because the tableau is finished, any such branch also contains either $\neg \phi$ or $\neg\psi$; either way, it will then close because of the presence of $\phi$ and $\psi$ earlier. So $\Gamma,\phi,\psi\vdash$; by Lemma \ref{dne}, $\Gamma,\phi,¬¬\psi\vdash$; by Lemma \ref{switch}, $\Gamma,\phi\vdash ¬\psi$.
\end{proof}

\begin{lemma} \label{con}
	If\, $\Gamma \vdash (\phi\wedge\psi)$, then\, $\Gamma \vdash \phi$ and\, $\Gamma \vdash \psi$.
\end{lemma}
\begin{proof}
	If $\Gamma \vdash (\phi\wedge\psi)$, there is a finished closed tableau generated by $\Sigma\cup\{\neg(\phi\wedge\psi)\}$ where $\Sigma$ is a finite subset of $\Gamma$. Suppose the first rule applied was the negated conjunction rule (\autoref{fig:stableaux}\subref{sf:nand}), giving two branches, both beginning with the members of $\Sigma$ and $\neg(\phi\wedge\psi)$, but one continuing with $\neg\phi$, and the other with $\neg\psi$. Because the tableau is closed, every branch beginning like those two branches is closed. Suppose we delete the node containing $\neg(\phi\wedge\psi)$, but keep $\neg\phi$. We will also therefore prune off the branch with $\neg\psi$ occurring on it. But the pruned tree remains a closed tableau, either because the tableau branches close due to the application of some tableau rule to $\neg\phi$, or because $\phi\wedge\psi$ occurs somewhere on the tableau; since it is finished, $\phi$ also appears, which  closes the branch. The same goes, \emph{mutatis mutandis}, for the other pruning. So $\Gamma\vdash \phi$ and $\Gamma\vdash \psi$.
\end{proof} 
Now we are in a position to prove the Cut theorem (or at least one theorem that commonly goes under that name.)


\begin{theorem}[Cut] \label{cut}
	If\, $\Gamma \vdash \phi$ and $\Gamma \vdash \neg\phi$ then $\Gamma \vdash$.
\end{theorem}
\begin{proof}
	We prove by (strong) induction on the complexity of $\phi$. 

\noindent\emph{Base case:} suppose $\phi$ is a sentence letter. Then there is a finite  $\Pi_{1}\subseteq\Gamma$ such that $\Pi_{1} \cup \{\neg\phi\}$ generates a finished closed tableau, and another finite $\Pi_{2}\subseteq \Gamma$ such that $\Pi_{2}\cup\{¬¬\phi\}$ generates a finished closed tableau. Let $\Sigma=\Pi_{1}\cup \Pi_{2}$ – $\Sigma$ too will be a finite subset of $\Gamma$. And note that adding more sentences to the trunk of a finished closed tableau will render it unfinished, but it will remain closed – finishing it will mean adding new leaves and possibly branches to already closed branches. So we can conclude that there is a finished closed tableau generated by $\Sigma\cup\{¬\phi\}$, and a finished closed tableau generated by $\Sigma\cup\{¬¬\phi\}$.

Suppose there is a finished open tableau $\mathbf{T}$ generated by $\Sigma$ alone. Inserting $\phi$ at the base of the trunk of $\mathbf{T}$ must render it closed, which means that each open branch must already have contained $¬\phi$. But since each tableau generated by $\Sigma\cup\{¬\phi\}$ is also closed, those branches must already have contained $\phi$ – those branches cannot in fact have been open. So any tableaux generated by $\Sigma$ must be closed, and hence $\Sigma$ is inconsistent and so are all of its supersets, including $\Gamma$.
	
\noindent\emph{The induction step:} $\phi$ is complex, and the induction hypothesis is that for each less complex constituent $\psi$ of $\phi$, and for any set $\Delta$ such that $\Delta\vdash\psi$ and $\Delta\vdash\neg\psi$, then $\Delta \vdash$. I consider two cases explicitly, those where $\phi$ is either a negation or a conjunction: \begin{enumerate}
		\item $\phi = \neg\psi$. We assume $\Gamma \vdash \phi$ and $\Gamma \vdash \neg\phi$, i.e., by Lemma \ref{switch}, $\Gamma,\phi\vdash$ and $\Gamma,\neg\phi\vdash$. Because $\phi=\neg\psi$, we also have $\Gamma,\neg\psi\vdash$ and $\Gamma,\neg\neg\psi\vdash$. By Lemma \ref{dne}, $\Gamma,\psi \vdash$. By the induction hypothesis applied to the simpler constituent $\psi$, $\Gamma\vdash.$
	
\item $\phi = (\psi\wedge\chi)$. Again, we assume (a) $\Gamma \vdash (\psi\wedge\chi)$ and (b) $\Gamma \vdash \neg(\psi\wedge\chi)$. By Lemma \ref{con} applied to (a), we have $\Gamma\vdash\chi$. But if a tableau generated by $\Sigma\cup\{\neg\chi\}$ closes, so does one generated by $\Sigma\cup\{\psi,\neg\chi\}$, where $\Sigma$ is a finite subset of $\Gamma$. So $\Gamma,\psi\vdash\chi$. By Lemma \ref{negcon} applied to (b), we have $\Gamma,\psi\vdash\neg\chi$. By the induction hypothesis $\Gamma,\psi\vdash$. But from Lemma \ref{con} applied to (a), we also have $\Gamma\vdash\psi$; by Lemma \ref{switch}, $\Gamma,\neg\psi\vdash$; and by the induction hypothesis, $\Gamma\vdash$. 
\item Other cases left for exercises; you will also need to establish lemmas parallelling Lemmas \ref{negcon}–\ref{con} for disjunction, conditional, and biconditional. 
	\end{enumerate} 
\end{proof}

What does the Cut Theorem show? Basically this: if you can get a tableau generated by $\Gamma$ and $\neg\phi$ to close, and you can get a tableau generated by $\Gamma$ and $\phi$ to close, then you could already have got a tableau generated by $\Gamma$ to close: whatever appeal you made respectively to $\phi$ and $\neg\phi$, it was inessential that they appeared on the trunk. (Either they weren't used, or they were derivable from something else already in $\Gamma$.) The interest of Cut in derivation systems is in showing that our derivations can all be `direct' in a sense: if we can derive something with the assistance of either $\phi$ or $¬\phi$, then we can derive it without detouring through that assistance.\footnote{This is more important when we consider natural deduction derivations in Chapters \ref{c:l1nd}–\ref{c:ndmeta}, where the Cut theorem is used to show that in principle all derivations can have a particularly elegant form where sentences are first broken down into simpler constituents and then built back up to establish the desired conclusions.}
Here is another way of making the same point. \begin{theorem}[Cut Again]\label{cutagain}
	If\, $\Gamma, \phi\vdash \psi$ and\, $\Gamma\vdash \phi$ then\, $\Gamma\vdash \psi$. \begin{proof}
		Suppose $\Gamma,\phi\vdash \psi$; then $\Gamma\cup\{¬\psi\}, \phi\vdash$ by Lemma \ref{switch} (and the fact that what flanks the turnstile are sets in which order doesn't matter). Suppose $\Gamma\vdash \phi$; then $\Gamma,¬ \phi\vdash$, and $\Gamma\cup\{¬\psi\},¬ \phi\vdash$ (by Weakening for $\vdash$, proved in exercises). By \autoref{cut}, $\Gamma\cup\{¬ \psi\}\vdash$, i.e., $\Gamma\vdash \psi$.
	\end{proof}
\end{theorem} In fact, this theorem is equivalent to \autoref{cut}. Note the parallel with \autoref{semanticcut}.

\begin{theorem}[Transitivity of Derivability] \label{transder}
If $\Gamma \vdash \phi$ and $\phi \vdash \psi$, then $\Gamma \vdash \psi$.
\end{theorem}
\begin{proof}
Assume $\phi\vdash \psi$. Then by weakening $\Gamma,\phi \vdash \psi$. Assume $\Gamma\vdash \phi$. Then by \autoref{cutagain}, $\Gamma\vdash \psi$.
\end{proof}
This shows is that any two-step derivation has a short-cut: if we can derive $\psi$ from something we can derive from $\Gamma$, well, we could have derived $\psi$ directly.

\section{Soundness and Completeness} \label{sec:tsoundcomp}
Soundness and completeness are properties that a specified derivation system for sentences in a given language may or may not have with respect to a particular semantic interpretation of the language.
\begin{definition}[Soundness] \label{def:soundness}
	A derivation system $P$ in a given language is \emph{sound} with respect to a semantic interpretation of the language just in case whenever there is a derivation which establishes $\Gamma \vdash_{P} \phi$, it is the case that $\Gamma \vDash \phi$.
\end{definition}
\begin{definition}[Completeness] \label{def:completeness}
	A derivation system $P$ in a given language is \emph{complete} with respect to a semantic interpretation of the language just in case whenever it is the case that $\Gamma \vDash \phi$, there is a derivation which establishes $\Gamma \vdash_{P} \phi$.
\end{definition}

Obviously we've already talked informally about the correspondence between $\vDash$ and $\vdash$ we are about to establish, and we designed our derivation system with one eye on capturing all and only correct entailments in derivations. But those intentions in the design of these derivation systems could have gone awry, so it is important to check they have not. So we prove soundness for our tableau derivation system.


\section{Soundness of the Tableaux Derivation System}

We begin by proving soundness of the tableaux system. We will prove it in this form: that every syntactic theorem – derivable sentence – is a semantic theorem, so that if $\vdash \phi$ then $\vDash \phi$.\footnote{Other proofs of soundness for tableau derivation systems can be found in \citet[165–7]{bosintlo}, \citet[119]{hodges}, and \citet[33–4]{jefforlos}, among many others.}

\begin{lemma}[Tableau rules preserve satisfiability]\label{lemma1} If a tableau is generated by a satisfiable negated sentence, there is at least one branch on that tableau such that every sentence on that branch is simultaneously satisfiable. That is: if there is an \lone\ structure $\mathscr{A}$ such that $\val{\neg \phi}{A} = T$, there is some branch $B$ on a tableau generated by $\{\neg\phi\}$ such that for all sentences $\beta \in B$, $\val{\beta}{A} = T$.\end{lemma}
\begin{proof} We prove the lemma by {\em induction on the length of tableau branch $B$}. In effect, we consider a sequence of (mostly unfinished) tableaux, such that each member extends the preceding member by application of one of the tableau rules.

\emph{Base case:} Consider the smallest tableaux $\mathbf{T}$ generated by $\{\neg\phi\}$: the single node $\langle\neg\phi\rangle$. Since this is the only member of the only branch on $\mathbf{T}$, and by hypothesis it is assigned $T$ by $\mathscr{A}$, the lemma holds in this case.

 \emph{Induction step:} Assume that the lemma holds of a branch 
 $B$ on tableau $\mathbf{T}_{n}$. Then we show the lemma holds of a branch $B^{+}$ on a tableau $\mathbf{T}_{n+1}$ obtained from $\mathbf{T}_{n}$ by one additional application of a rule in \autoref{fig:stableaux} to a sentence in $B$ on $T_{n}$. There are three cases.
    \begin{enumerate}
	\item We apply the Double Negation Rule (\autoref{fig:stableaux}\subref{sf:dn}). Then some sentence on $B$ is of the form $\neg\neg\chi$, and we add $\chi$ to the bottom of the branch to get $B^{+}$. Since the valuation function induced by the \lone\ structure $\mathscr{A}$ is classical, $\val{\chi}{A} = \val{¬¬\chi}{A} = T$, as required by the lemma.
	\item We apply a non-branching rule to some sentence  on $B$. Then we add two sentences to the bottom of $B$. If we applied, for example, the Negated Conditional rule (\autoref{fig:stableaux}\subref{sf:nc}) to $\neg(\psi \to \chi)$, we added $\psi$ and $\neg\chi$ to the bottom of $B$ to get $B^{+}$. By the rules on classical valuations, $\val{¬(\psi\to\chi)}{A} = T$ iff $\val{\psi \to \chi}{A} = F$ iff $\val{\psi}{A} = T$ and $\val{\chi}{A} = F$ iff $\val{\psi}{A} = T$ and $\val{\neg\chi}{A} = T$, as required. 

	Similarly for the Conjunction rule: $\val{\psi\wedge\chi}{A} = T$ iff $\val{\psi}{A} = T$ and $\val{\chi}{A} = T$. So the lemma holds of $B^{+}$. (The Negated Disjunction rule is left as an exercise.)

	\item We apply a branching rule to some sentence on $B$. We then get two new branches, $B^{+}_{1}$ and $B^{+}_{2}$, either of which can satisfy the lemma (but we only need one of them to satisfy it: the lemma only says that there is \emph{at least one} branch on a tableau such that all of the sentences on it are assigned $T$ by $\mathscr{A}$). For instance, if we apply Disjunction (\autoref{fig:stableaux}\subref{sf:di}) to $\psi \vee \chi$, $B^{+}_{1} = B \cup \{\psi\}$ and $B^{+}_{2} = B \cup \{\chi\}$. Since by the rules for classical valuations, $\val{\psi\vee\chi}{A} = T$ iff either $\val{\psi}{A} = T$ or $\val{\chi}{A} = T$; that is, the lemma holds of at least one of $B^{+}_{1}$ or $B^{+}_{2}$.

Similarly for the Negated Conjunction rule:	If $\neg(\phi \wedge \psi) \in B$, then $\neg\phi \in B^{+}_{1}$ and	$\neg\psi \in B^{+}_{2}$. $\val{¬(\phi \wedge \psi)}{A} = T$ iff $\val{\phi \wedge \psi}{A} = F$ iff	$\val{\phi}{A} = F$ or $\val{\psi}{A} = F$ iff $\val{¬ \phi}{A} = T$ or $\val{¬ \psi}{A} = T$. (The Conditional rule is left as an exercise.) 
\end{enumerate}That completes the induction.\end{proof}

Lemma \ref{lemma1} shows that the tableau rules preserve satisfiability: any tableau, finished or otherwise, generated by a satisfiable sentence has at least one branch, all of whose elements are simultaneously satisfiable. Now we are in a position to prove soundness.

\begin{theorem}[Soundness] \label{thm:sound} If\, $\vdash \phi$ then $\vDash \phi$.\end{theorem}\begin{proof} Assume that $\vdash\phi$. Then every finished tableau generated by $\{\neg\phi\}$ is closed. 

Assume for \emph{reductio} that $\nvDash \phi$. Then there is an \lone\ structure $\mathscr{A}$ that makes $\neg \phi$ true: $\val{\neg\phi}{A}=T$. By Lemma \ref{lemma1}, there is a finished tableau $\mathbf{T}$ generated by $\neg \phi$, with a branch $B$ such that for every $\beta \in B$, $\val{\beta}{A} = T$. Since the valuation function induced by $\mathscr{A}$ is classical, for any \lone\ sentence $\psi$, if $\psi \in B$, then $\neg\psi \notin B$. (Since for any structure $A$, $\val{\psi}{A} ≠ \val{\neg\psi}{A}$, and every sentence on $B$ is satisfied in some structure and hence all have the same truth value in that structure.) Hence $B$ cannot be closed;  hence $\mathbf{T}$ is not closed. But $\mathbf{T}$ is generated by $\{\neg \phi\}$, and our initial assumption was that any finished tableau generated by $\{¬\phi\}$ is closed. So our \emph{reductio} hypothesis must be wrong; that is, it must instead be true that $\vDash \phi$. But now we've shown $\vDash\phi$ on the assumption that $\vdash\phi$.
\end{proof}

Having proved the theorem, we can easily extend it to the general
case of an arbitrary argument. 

\begin{theorem}[General Soundness]
	If $\Gamma\vdash\phi$ then $\Gamma\vDash\phi$.
\end{theorem}
\begin{proof}
	Recall that $\Gamma\vdash\phi$ iff there is a finished closed tableau generated by a finite set $\Sigma\cup\{\neg\phi\}$, where $\Sigma\subseteq\Gamma$, i.e., iff $\Sigma\vdash\phi$. 
	
	Assume that $\Gamma\vdash\phi$. Then there is a finite set $\Sigma\cup\{¬\phi\} = \{\sigma_{1},…,\sigma_{n},\neg\phi\}$ which generates a finished closed tableau. By repeated applications of the Deduction theorem for tableaux (\autoref{thm:sdt}), $\vdash (\sigma_{1} \to (\sigma_{2} \to ( … (\sigma_{n}\to\phi))))$. By Soundness (Theorem \ref{thm:sound}), $\vDash (\sigma_{1} \to (\sigma_{2} \to ( … (\sigma_{n}\to\phi))))$. By repeated applications of the Deduction theorem for entailment (\autoref{ded}), $\Sigma \vDash\phi$. Since $\Sigma\subseteq\Gamma$, $\Gamma \vDash \phi$, by Weakening for $\vDash$.\footnote{Actually (because Weakening as stated only applies to a single sentence) what we need is the stronger claim (still obviously correct), that for any set $\Delta$, if $\Sigma\vDash\phi$, then $\Sigma \cup \Delta\vDash\phi$. And we then let $\Delta=\Gamma\setminus\Sigma$, so that $\Sigma\cup\Delta=\Gamma$, and the result follows.}
\end{proof}














\section{Completeness for Tableaux}


The proof of completeness for the tableaux derivation system is relatively straightforward. The idea is simple: we show that, if set of sentences $\Gamma$ is consistent, then $\Gamma$ is satisfiable. Recall that (Definition \ref{defcontab}) a set of sentences $\Gamma$ is syntaxctically consistent if every finished tableau generated by a finite subset of $\Gamma$ has an open branch. We will use this fact to show that there is a structure in which all the members of $\Gamma$ are true. To do this, we have to show an intermediate lemma, to the effect that an open branch can be used to determine a structure which makes each sentence on the branch true.


\begin{lemma}[Hintikka's Lemma]\label{lemm:hin} If $B$ is an open branch on a finished open tableau generated by a finite set of \lone\ sentences $\Sigma$, then there is an \lone\ structure $\mathcal{B}$ such that for every sentence $\beta$ on $B$, $\val{\beta}{B} = T$.\end{lemma}
\begin{proof}
	
	Suppose there is an open branch on a finished tableau generated by $\Sigma$, $B$. Define an \lone\ structure $\mathscr{B}$ as follows: for every sentence letter $s$, \[\mathscr{B}(s) = \begin{cases}
		T \quad\text{if $s$ occurs in some node on $B$;}\\
		F \quad\text{if $\neg s$ occurs in some node on $B$;}\\
		T \quad\text{otherwise.}
	\end{cases}\] Because $B$ is an open branch, this successfully defines an \lone\ structure: no sentence letter and its negation both occur on $B$, so this definition assigns one and only one value to each \lone\ sentence letter. (It is thus a classical structure, and induces a classical two-valued valuation of all sentences.)
	
We show by induction on complexity on sentences  that  for every sentence $\beta$ on $B$, $\val{\beta}{B}=T$. Because this is a tableau construction, the neatest way to think about the induction on complexity is that the base case comprises those sentences to which no tableau rule applies, and the induction step involves consideration of sentences to which tableau rules apply. (Our base ‘case’ thus encompasses literals, rather than just sentence letters.) 

\noindent\emph{Base case:} Suppose $\beta$ occurs on $B$, and is a literal: either is a sentence letter or a negated sentence letter. If the former, by construction, $\mathscr{B}(\beta)=T$, so $\val{\beta}{B}=T$, by the definition of an \lone\ structure. If the latter, i.e., $\beta = \neg s$ for some sentence letter $s$, $\val{\beta}{B} = T$ iff $\val{s}{B} = F$ iff $\mathscr{B}(s) = F$ iff $\neg s$ occurs on $B$; which of course it does.

\noindent\emph{Induction step:} Suppose $\beta$ is a complex sentence, and the lemma holds of its less complex constituents. There are three cases of interest, corresponding to different tableau rules: $\beta$ is a
double negation; a branch rule can be applied to $\beta$; or a list
rule can be applied to $\beta$. \begin{enumerate}
	\item $\beta$ is a double negation, $\neg\neg\phi$. Then, because this is a finished branch, $\phi$ appears on $\beta$; because the lemma holds of less complex constituents, $\val{\phi}{B}=T$. So $\val{\neg\phi}{B}=F$, and $\val{\neg\neg\phi}{B}=T$, i.e., $\val{\beta}{B}=T$.
  \item $\beta$ can have a list rule applied to it. Let us choose Negated
    Conditional, so $\beta = \neg(\phi \to \psi)$. Then $\phi$ and $\neg \psi$
    appear on $B$, because the tableau is finished, and by the induction hypothesis $\val{\phi}{B} = \val{¬\psi}{B} =T$. Therefore by the rules on the valuation function, $\val{\phi\to\psi}{B}=F$, and $\val{\neg(\phi \to \psi)}{B}=T$, i.e., $\val{\beta}{B}=T$, as required. Analogous reasoning applies to the other list rules.
    \item $\beta$ can have a branch rule applied to it. Let $\beta = \phi
    \vee \psi$. Then either $\phi$ or $\psi$ appears on $B$; hence either $\val{\phi}{B} = T$ or $\val{\psi}{B} =T$, which by the rules on the valuation function, means that $\val{\phi\vee\psi}{B}=T$,  i.e., $\val{\beta}{B}=T$, as required. Analogous reasoning applies to the other branch rules.
\end{enumerate}
    That suffices to show the lemma.\end{proof}



\begin{theorem}[Completeness for tautologies]\label{thm:comp} If\, $\vDash \phi$ then $\vdash \phi$.\end{theorem}
\begin{proof} We prove the equivalent contrapositive, namely, that if it is {\em not} the case that $\phi$ is a syntactic theorem (which we write `$\nvdash \phi$') then it is not the case that $\phi$ is a semantic theorem (`$\nvDash \phi$').
    
Assume that $\nvdash \phi$. Then there is a finished open tableau generated by $\{\neg\phi\}$ which has an open branch, $B$. Let $\mathscr{B}$ be the structure induced by $B$, in accordance with Hintikka's Lemma (Lemma \ref{lemm:hin}). By that lemma, every sentence occurring on $B$ is true in $\mathscr{B}$. Since $\neg\phi$ appears on $B$, as the root, $\val{\neg\phi}{B}=1.$ Hence there is a structure which makes $\phi$ false, so $\nvDash \phi$.
\end{proof}

Theorem \ref{thm:comp} states that every tautology is derivable. This can easily be extended to arguments with finitely many premises: \begin{theorem}[Completeness for finite arguments]\label{thm:fargc} When $\Gamma$ is finite, if\/ $\Gamma \vDash \phi$ then $\Gamma \vdash \phi$.	
\end{theorem}
\begin{proof}
	If $\Gamma \vDash \phi$, and $\Gamma$ is a finite set $\{\gamma_{1},\ldots,\gamma_{n}\}$, then (by repeated applications of the Deduction theorem for entailment (\autoref{ded}), $(\gamma_{1} \to (\gamma_{2} \to (\ldots(\gamma_{n} \to \phi)\ldots)))$ is a tautology. By Theorem \ref{thm:comp}, $\vdash (\gamma_{1} \to (\gamma_{2} \to (\ldots(\gamma_{n} \to \phi)\ldots)))$. By repeated applications of the deduction theorem for tableaux (\autoref{thm:sdt}), $\Gamma \vdash \phi$.
\end{proof}

\paragraph{Completeness for Arbitrary Arguments} \autoref{thm:fargc} shows that if an argument with finitely many premises is valid, there is a tableau derivation of the conclusion from the premises. But what if there are infinitely many premises in $\Gamma$? Could a claim validly follow from infinitely many premises, and yet there be no tableau derivation associated with that argument?

We already have enough materials to see that the answer is no.

\begin{theorem}[Completeness from Compactness]
For any set of \lone\ sentences $\Gamma$, if\, $\Gamma\vDash \phi$ then $\Gamma\vdash\phi$.
\begin{proof}
	If $\Gamma\vDash\phi$, then $\Gamma\cup\{¬\phi\}$ is unsatisfiable. By Compactness (\autoref{compact}), if $\Gamma\cup\{¬\phi\}$ is unsatisfiable, then for some finite set $\Sigma\subseteq\Gamma$, $\Sigma\cup\{¬\phi\}$ is unsatisfiable, i.e., $\Sigma \vDash$. Accordingly, $\Sigma\vDash\phi$. By \autoref{thm:fargc}, $\Sigma\vdash \phi$; and since $\Sigma\subseteq \Gamma$, $\Gamma\vdash \phi$. 
\end{proof}
\end{theorem}


We can also prove completeness directly without detouring through compactness. There are no infinite tableaux, so we need to pursue our goal with some subtlety. Rather than consider a tree generated by
the entire infinite set $\Gamma$, we will consider a sequence of finite tableaux, each of which is generated by successively more of $\Gamma$, and each of which contains the previous tableau as a proper part.

\begin{theorem}[Completeness Directly]\label{compdirect}
	For any set of \lone\ sentences $\Gamma$, if\, $\Gamma\vDash \phi$ then $\Gamma\vdash\phi$. \begin{proof}
		Let $\Gamma$ be enumerated $\gamma_{1},…$. Let $\mathbf{T}_{0}$ be a finished tableau generated by $\{¬\phi\}$, and let each $\mathbf{T}_{n}$ be a finished tableau generated by $\langle \gamma_{n},…,\gamma_{1},¬\phi\rangle$, where $\mathbf{T}_{n}$ is constructed from $\mathbf{T}_{n-1}$ by adding $\gamma_{n}$ as the topmost node, and applying any applicable tableau rule to it by extending any branch in $\mathbf{T}_{n-1}$ at the leaf, and then finishing the resulting tableau by extending that leaf to a tip by application of tableau rules. Note immediately that $\mathbf{T}_{i}$ is a proper part of $\mathbf{T}_{i+1}$; and if any branch is closed in $\mathbf{T}_{i}$, every branch including it in $\mathbf{T}_{i+1}$ remains closed. 

If any $\mathbf{T}_{i}$ closes, then we can apply \eqref{thm:fargc} to conclude that $\Gamma\vdash\phi$, since it is generated by a finite subset of $\Gamma\cup\{¬\phi\}$. So let us assume for \emph{reductio} that every $\mathbf{T}_{i}$ is open. Since closed branches never reopen, the fact that every tableau in our sequence is open means that each tableau contains at least one open branch that is contained within an open branch on all later tableaux in the sequence.  By Hintikka's Lemma \ref{lemm:hin}, for each $\mathbf{T}_{i}$ there is an \lone\ structure $\mathscr{B}_{i}$ that makes each member of $\{¬\phi,\gamma_{1},…,\gamma_{i}\}$ true. Because each subsequent tableau retains at least one branch that is open on its predecessor, we know more specifically that this $\mathscr{B}_{i}$ can be chosen in such as way that it also makes true $\gamma_{i+1}$. And this is true for every $\mathbf{T}_{i}$, so in fact there is a single structure $\mathscr{B}$ such that each $\mathbf{T}_{i}$ has an open branch all of whose members are true in $\mathscr{B}$.

Since $\Gamma\cup\{¬\phi\}$ is unsatisfiable, however, at least one $\gamma_{j}\in \Gamma$ is false in $\mathscr{B}$. But $\gamma_{j}$ occurs in every open branch on $\mathbf{T}_{j}$, including the branch all of whose members are true in $\mathscr{B}$. Contradiction: not all of the $\mathbf{T}_{i}$s can be open. 
	\end{proof}
\end{theorem}
This in effect amounts to another proof of compactness.
\begin{corol}[Compactness from Completeness]\label{comptabl}
	If\, $\Gamma\vDash$ then for some finite subset $\Sigma$ of\, $\Gamma$, $\Sigma\vDash$. \begin{proof}
		If $\Gamma\vDash$, then by \autoref{compdirect}, $\Gamma\vdash$. By the definition of `$\vdash$' in Definition \ref{tablderv}, there is a finished closed tableau generated by some finite subset $\Sigma$ of $\Gamma$. By Soundness (\autoref{thm:sound}), $\Sigma$ is unsatisfiable. 
	\end{proof}
\end{corol}

The proofs of Soundness and Completeness together show that whatever we can show using the semantic notions of satisfaction and truth in a structure, we could have equally well demonstrated by using the purely mechanical device of tableau derivation. A few simple rules for manipulating and deriving consequences from a collection of \lone\ sentences, simple enough that you could teach them to a child or a computer, nevertheless turn out to be powerful enough to demonstrate the correctness of every valid argument (and the incorrectness of every invalid argument) in propositional logic. This might not seem all that surprising – after all, it is fairly transparent to see that the rules governing tableaux were precisely chosen to have the right semantic properties. (They were not plucked randomly out of thin air.) But look again: isn't it at least a little remarkable that notions of truth and meaning can have their practical significance (in sorting arguments into conclusive and non-conclusive) captured entirely by formal rules which depend only on syntax? This is yet another sense in which our logic is formal: semantic consequence is extensionally equivalent to formal syntactic derivability. 


\section{Finitude and Decidability}

In \autoref{c:l1meta} we considered issues around decidability by considering an effective procedure for checking validity using truth tables. We can use tableau derivations in an effective procedure too. 
In the previous chapter we showed that any finite set of \lone\ sentences generates a finished finite tableau (\autoref{fintab}), and the procedure described in the proof for generating a finished tableau from a finite generating set is an effective one. So we can certainly produce finished tableau in a finite time.

\paragraph{Effective Evaluation of Tableaux} For a decision procedure, however, we need to do more than produce a finished tableau – we need to check whether that tableau is closed. But since every \lone\ tree is finite, comprised of finitely many branches, we can effectively check by exhaustive search whether it is closed. Enumerate the branches in some order; take the first branch, then for each node $\phi$ on the branch, check whether each branch descendent $\psi$ to see whether $\phi$ is of the form $¬ \psi$ or $\psi$ is of the form $¬ \phi$. If all the branches are closed, the tableau is closed. But we only needed to check finitely many nodes on finitely many branches, so we can perform this check in finite time.

\paragraph{A Tableau Decision Procedure} Because a closed tableau will remain closed when finished, an unfinished closed tableau still shows the generating set to be inconsistent. This suggests the following decision procedure for inconsistency of a finite set $\Gamma$ of \lone\ sentences:
\begin{enumerate}
	\item Enumerate $\Gamma = \gamma_{1},…,\gamma_{n}$, and inscribe a tableau $\mathbf{T}_{0}$ which contains $\langle \gamma_{1},…,\gamma_{n}\rangle$ as its only branch.
	\item Check whether $\mathbf{T}_{0}$ is closed; if it is, terminate with the report that $\Gamma$ is inconsistent; otherwise continue to step 3.
	\item If $\mathbf{T}_{i}$ is the last tableau constructed, then apply the tableau rules to $\gamma_{i+1}$, and then to any sentences resulting from $\gamma_{i+1}$, and to sentences resulting from them, etc. (Since each \lone\ sentence is of finite complexity, this process involves the generation of only finitely many sentences before the tableau rules no longer apply. The key is that after this process the only sentences which have not had tableau rules applied to them are original members of $\Gamma$.) 
	\item Apply the check for closure to $\mathbf{T}_{i+1}$. If it is closed terminate with the report that $\Gamma$ is inconsistent; if it is open, and $\gamma_{i+2}\in \Gamma$, then return to step 3; if is is open and each $\gamma\in \Gamma$ has already had tableau rules applied to it, terminate with the report that $\Gamma$ is consistent. 
\end{enumerate}

 This procedure is a decision procedure for inconsistency: it terminates in a finite time after the construction of a finished tableau, and reports either open or closed. Because of the soundness and completeness theorems, this is also another decision procedure for unsatisfiability of finite sets of \lone\ sentences (\autoref{findec}).

\paragraph{Positive Decidability for Infinite Inconsistency} We've already shown that there is no decision procedure as to whether or not an infinite set of \lone\ sentences is unsatisfiable. Because of soundness and completeness, if the question of consistency of an infinite set of sentences were decidable, we could use that procedure to construct a decision procedure for satisfiability. So consistency must also be undecidable.

But, just as earlier (\autoref{posdecinc}), the question of inconsistency is positively decidable: if a recursively enumerable set of sentences is inconsistent, we can describe an effective procedure demonstrating that. The procedure is to begin with our enumeration of $\Gamma$, $\gamma_{1},…$. At stage $i$, take the set $\Gamma_{i} = \{ \gamma_{1},…,\gamma_{i}\}$ to be the generating sequence for a tableau $\mathbf{T}_{\gamma_{i}}$; apply the procedure described above to check whether $\Gamma_{i}$ is inconsistent. If it is, terminate with the message that $\Gamma$ is inconsistent. If not, move on to stage $i+1$. It can readily be seen that this procedure will not terminate if $\Gamma$ is consistent: the search for inconsistency will continue, constructing larger and larger open tableaux at each stage.


\section{Alternate Tableau Systems}

% labelled tableaux make semantics clear

Consider these two rules: \begin{center}
	{\leaf{$\neg\phi\vee\neg\psi$}\branch{1}{$\neg(\phi\wedge\psi)$}\qobitree} \qquad {\leaf{$\neg\phi\wedge\neg\psi$}\branch{1}{$\neg(\phi\vee\psi)$}\qobitree}
\end{center}

% Let us note firstly, that these proposed rules can be derived in our existing system. That is demonstrated by these two schematic tableau proofs:
% \begin{center}
% 	{\leaf{$\neg\phi\vee\neg\psi$}\branch{1}{$\neg(\phi\wedge\psi$)}\qobitree} \qquad {\leaf{$\neg\phi\wedge\neg\psi$}\branch{1}{$\neg(\phi\vee\psi)$}\qobitree}
% \end{center}


% What if we developed a new tableau system, in which we replaced our familiar rules for negated conjunction (\autoref{fig:stableaux}\subref{sf:nand}) and negated disjunction (\autoref{fig:stableaux}\subref{sf:ndsj}) by these rules?

\section{Trees and Tableaux}

In this section some general theorems about trees are proved that are useful for situating the metatheory of tableaux in its mathematical context.

\paragraph{The Set-theoretic Conception of Tree}
 The more general definition of a tree is  set-theoretic: 
\begin{definition}[General Tree]\label{tree}
	A tree $\mathbf{T}$ is a pair $\langle N, \preceq\rangle$ where $N$ is a set of items (`nodes'), and $\preceq$ is a partial order on $N$, such that (i) there is a \emph{root node} $r \in N$ such that for all $n\in N$, $r \preceq n$, and (ii) for each $n \in N$, the set $\{x \in N: x \preceq n\}$ is well-ordered by $\preceq$ (recall Definition \ref{def:wellord}). 
\end{definition} The nodes in this definition are otherwise featureless indices, individuated entirely by their place in the tree structure. In \lone-trees, a given sentence can occur more than once on a branch, but a node cannot occur more than once in any tree. So if we want to show that \lone-trees from Definition \ref{l1tree} are trees in the sense of Definition \ref{tree}, we will have to come up with some way of associating \lone\ sentences with nodes. The simplest way is to \emph{label} the tree. A labelled tree is a tree together with a total function $f$ from $N$ into the set of \lone\ sentences, which assigns to each node a sentence as label. The function is into, so a given sentence might label more than one node.

\begin{theorem}[\lone-trees are labelled trees]
	Each \lone-tree corresponds to a labelled tree. \begin{proof}
		We want to show that, if we have an \lone-tree $\mathbf{T}$, there is a corresponding tree $\mathbf{T}'$. So we need to show (1) that there is an appropriate set of nodes; (2) there is a partial order; (3) there is a root node; (4) the branches are well-ordered; and (5) there is a labelling function. \begin{enumerate}
			\item If $X$ is a sequence $\langle x_{1},…,x_{n},…\rangle$, define an \emph{index set} $X_{n}$ as follows: $X_{n} = \{\langle x_{i},i\rangle: x_{i} \in X\}$. This transforms an ordered sequence of items into an unordered set of item, position pairs.

			Recalling that an \lone-branch is just a sequence of \lone\ sentences, and an \lone-tree is just a set of \lone-branches, there will be an index set for each \lone-branch in $\mathbf{T}$. The union of all index sets for \lone-branches in our \lone-tree $\mathbf{T}$ will be the set $N$ of nodes for our desired tree $\mathbf{T}'$. Each $\langle$sentence, index$\rangle$ pair occuring on some branch is included. Because sets with the same members are identical, and when branches overlap they have the same sentences at the same position, then we do not have redundancy: though every \lone-branch shares the root node, the pair $\langle \rho,1\rangle$ will be added to the union of all index sets `several times', but of course we end up with just one member of the set for that shared node. Since we have said nothing about what the set of nodes is to consist in, it is perfectly acceptable for this complex set of pairs to be the set of nodes for $\mathbf{T}'$.
			\item We need to define the partial order $\preceq$ on $N$. Since each member of $N$ is of the form $\langle \phi,i\rangle$, it suffices to define it on pairs of this form. We will say that $\langle \phi,i\rangle \preceq \langle \psi,n\rangle$ iff there is an \lone-branch on $\mathbf{T}$ that includes $\phi$ at position $i$ and $\psi$ at position $j$, and $i≤j$. So defined, $\preceq$ is a partial order (Definition \ref{def:order}): it is transitive (since if $x\preceq y$ and $y\preceq z$, then all of $x,y,z$ fall on the same \lone-branch, and the transitivity of $≤$ ensures that $x\preceq z$); it is reflexive (since $≤$ is reflexive; and it is antisymmetric (since if $x\preceq y$ and $y\preceq x$, then $x$ and $y$ fall on the same \lone-branch and $i≤j$ and $j≤i$, which entails that $i=j$, and since there is only one sentence at each position in a branch, $x=y$).
			\item Since every \lone-branch on $\mathbf{T}$ shares a common initial subsequence, each begins with some sentence $\phi$. So $\langle \phi,1\rangle$ is the root node of $\mathbf{T}'$.
			\item Recall that a well-ordering is a total order on a set such that every non-empty subset has a least member – there are no infinite descending chains. We need to show that $\preceq$, as defined, when restricted to sets of the form $\{x \in N: x \preceq n\}$ for some $n\in N$, is a well-ordering. Since $x\preceq y$ only if $x$ and $y$ fall on the same \lone-branch, the sets of this form are index sets of initial subsequences of \lone-branches. Restricted to these intial subsequences, $\preceq$ is total because $≤$ is total; and since the initial subsequences are sequences, they can be mapped one-one onto subsets of $\mathbb{N}$, and the least number principle then entails that $≤$ is a well-ordering on these initial subsequences, so that $\preceq$ is a well-ordering on the corresponding index sets.
			\item The labelling function is: $f(\langle \phi,i\rangle) = \phi$. This simply labels a node with its first element, which is the sentence from the original \lone-tree.			
		\end{enumerate}
	\end{proof}
\end{theorem}

\paragraph{Infinite Trees} The set-theoretic account of trees permits trees with infinitely many nodes. Such a tree might be infinitely tall, with an infinite branch descending from the root; or it might be infinitely wide, with infinitely many branches. But if there are only finitely many branches from each node, an infinite tree must have an infinite branch.
\begin{lemma}[König's Lemma for Trees]\label{konig}
	Every finitely-branching tree containing infinitely many sentences has an infinite branch. \begin{proof} (See also \citet[152]{bevpospa}.) Let us say that $\psi$ is a \emph{descendent} of $\phi$ iff there is a branch on which both occur and where $\psi$ occurs after $\phi$ in the sequence. If a tree contains infinitely many sentences, the root node $\nu_{0}$ must have infinitely many descendents. 

	Suppose a node $\nu_{n}$ on an infinite tree has infinitely many descendents. Then there is a node $\nu_{n+1}$ immediately posterior to and on the same branch as $\nu_{n}$ with infinitely many descendents. For if every branch $B$ on which $\nu_{n}$ occurs is such that the next item in the sequence after $\nu_{n}$ has only finitely many descendents, then every branch on which $\nu_{n}$ occurs must be finite. Since $\nu_{n}$ has infinitely many descendents, there must be infinitely many branches $B_{i}$ agreeing with $B$ up through $\nu_{n}$ but disagreeing on the next item in the sequence: $B_{i} = \langle \rho,…,\nu_{n},\phi_{i},…,\lambda\rangle$. But this cannot be a tree, since for any finitely branching tree, there are at most finitely many distinct branches agreeing with $B$ up through $\nu_{n}$. So at least one immediate descendent of $\nu_{n}$ must have infinitely many descendents; pick one and call it $\nu_{n+1}$.

	We have shown that the root $\nu_{0}$ has infinitely many descendents, and that if a node $\nu_{n}$ has infinitely many descendents, then there is an immediate descendent $\nu_{n+1}$ which also has infinitely many descendents. The sequence $\langle \nu_{0},…,\nu_{n},…\rangle$ is an infinite sequence of \lone\ sentences,  each of which follows from previous members of the sequence by the tree rules. So it is an infinite tree branch.
	\end{proof}
\end{lemma}
We used this lemma in the proof of the finitude of tableaux (\autoref{fintab}), where the finitude of finished \lone\ tableau branches was used to establish the finitude of \lone\ tableaux.



{\small

\subsection*{Further Reading}
\addcontentsline{toc}{subsection}{Further Reading}
\citet{smullyan}, \citet{bevpospa}, \citet{hodges}, \citet[ch. 4]{bosintlo} and \citet{jefforlos}  all discuss the metatheory of tableaux systems in ways that may be illuminating to consider in comparison to the results and discussion offered above.

\subsection*{Exercises} \label{ex:tablmeta}
\addcontentsline{toc}{subsection}{Exercises}

\begin{enumerate}
\item Show Weakening for $\vdash$: that if $\Gamma\vdash \phi$ then $\Gamma\cup \Delta \vdash \phi$ for any $\Delta$.
\item Prove that \autoref{cutagain} entails \autoref{cut}, thus showing that those two theorems are equivalent.
\item Assuming the  soundness theorem, prove that if $\Gamma \vDash \phi$  is an \emph{incorrect} sequent  then $\Gamma \vdash \phi$ is also incorrect.


\item Consider  an operator $\odot$ defined by the following tableau rules: 
 \begin{center}
 {\leaf{$(\phi \odot \phi)$\\$(\psi \odot \psi)$}\branch{1}{$\qquad\qquad(\phi 
 \odot  \psi)\qquad\qquad$}\qobitree} \qquad
 {\leaf{$\phi$}\leaf{\quad$\psi$\qquad}\branch{2}{$\qquad\qquad((\phi \odot
\psi) \odot (\phi \odot \psi))\qquad\qquad$}\qobitree}\end{center}

\begin{enumerate}
 \item  Which truth-function does $\odot$ express? (I.e., which truth function is characterised by these tableau rules?)
 \item If these rules were the only rules for a system of tableau,
 under what conditions should a branch be counted as closed?
\item Are these tableau rules sound?
 \end{enumerate}
 \item A fellow student argues as follows: \begin{quotation}
	If the derivation system just introduced is complete, then whenever $\Gamma \vDash \phi$, there is a derivation that shows $\Gamma \vdash \phi$. But proofs are finite; so if $\Gamma$ is infinite, there is no proof that $\Gamma \vdash \phi$ – so the system is not complete!
\end{quotation} How should you respond?
 \end{enumerate}


% \exercise{\begin{ex}Prove the induction step of the derivation for Lemma 1 in the
%     cases where the branch $B$ is extended by (i) the negated disjunction
%     rule; and (ii) the conditional rule.
% \end{ex}

% \begin{ex} Assuming the  soundness theorem, prove that if $\Xi \vDash \phi$ 
% is an \emph{incorrect} sequent  then $\Xi \vdash \phi$ is also incorrect.
% \end{ex}

% \begin{ex} Recall the tableau rules involving the $\odot$ operator from exercise \ref{odot}.
%    Are those tableau rules sound?
%     \end{ex}

% }


Answers to selected exercises on page \pageref{ans:tablmeta}.
}