adding proof-theory/proof-search

Author: rzach

content/proof-theory/cut-elimination/cut-elimination.tex

@@ -13,7 +13,6 @@
 \olimport{midsequent}
 \olimport{interpolation}
 
-
 \OLEndChapterHook
 
 \end{document}

content/proof-theory/proof-search/completeness.tex

@@ -0,0 +1,194 @@
+% Part: proof-theory
+% Chapter: proof-search
+% Section: completeness
+
+\documentclass[../../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{pt}{ps}{cpl}
+
+\olsection{Completeness}
+
+We now show that the proof search algorithm is fool-proof, i.e., if it
+aborts or never halts, there is no !!{proof} of the starting
+sequent~$\Gamma \Sequent \Delta$. To do this, we define
+!!a{structure}~$\Struct M$ such that for all $!A \in \Gamma$,
+$\Sat{M}{!A}$, and for all~$! \in \Delta$, $\Sat/{M}{!A}$. In other
+words, all !!{formula}s in~$\Gamma$ are true and all !!{formula}s
+in~$\Delta$ are false in~$\Struct M$, i.e., $\Gamma \Sequent \Delta$
+is not valid. Since \Log{G3c} is sound, $\Gamma \Sequent \Delta$ has
+no !!{proof}
+
+We define $\Struct{M}$ from a pair $\Theta, \Xi$ of !!{formula}s and a
+set~$C$ of !!{constant}s. We obtain $\Theta, \Xi$ and~$C$ from a
+\emph{failure branch} of the failed (aborted or non-terminating) run
+of the proof search. A failure branch is a sequence $\Pi_n \Sequent
+\Lambda_n$ of sequents and sets of !!{constant}s~$C_n$ such that
+$\Pi_0 \Sequent \Lambda_0$ is the end-sequent $\Gamma \Sequent
+\Delta$, and $\Pi_{n+1} \Sequent \Lambda_{n+1}$ is a premise of $\Pi_n
+\Sequent \Lambda_n$ generated at stage~$n+1$ for which the algorithm
+does not find !!a{proof}. Such a premise must obviously exist for
+each~$n$, since otherwise the algorithm would have found !!a{proof}.
+We let $C_n$ be the set of !!{constant}s associated with~$\Pi_n
+\Sequent \Delta_n$.
+
+If the algorithm aborts at a top-most sequent consisting only of
+atomic !!{formula}s, the branch ending in that sequent is a failure
+branch. If if the algorithm never terminates, it keeps generating
+larger and larger trees. You can think of these as growing an infinite
+tree (the tree you'd have after infinitely many steps of the algorithm
+had run). This would be an infinite tree which is, however, finitely
+branching (every node only has one or two children---the sequents
+immediately above it). Every infinite, finitely branching tree must
+have an infinite branch by K\H{o}nig's Lemma. Such an infinite branch
+would be a failure branch in the case where the search algorithm runs
+forever.
+
+If the sequence of $\Pi_n \Sequent \Lambda_n$ and $C_n$ is a failure
+branch, let $\Theta = \bigcup_n \Pi_n$ and $\Xi = \bigcup_n \Lambda_n$
+(removing indices and multiple occurrences of !!{formula}s) and $C =
+\bigcup_n C_n$.
+
+We are ready to define~$\Struct{M}$.
+\begin{enumerate}
+\item The domain $\Domain{M}$ is the
+set of terms that can be formed from~$C$ and the !!{function}s
+in~$\Gamma \Sequent \Delta$, if there are any, but no !!{variable}s. 
+\item If $c \in \Domain{M}$, $\Assign{c}{M} = c$.
+\item If $f$ is an $m$-place !!{function} in $\Gamma \Sequent \Delta$, and $t_1$,
+\dots, $t_m \in \Domain{M}$, then $\Assign{f}{M}(t_1, \dots, t_m) =
+f(t_1, \dots, t_n)$.
+\item If $R$ is an $m$-place !!{predicate} in $\Gamma \Sequent
+\Delta$, then $\Assign{R}{M} = \Setabs{\tuple{t_1, \dots, t_m} \in
+\Domain{M}^n}{R(t_1, \dots, t_n) \in \Theta}$.
+\end{enumerate}
+$\Struct{M}$ is a \emph{term model} in that its domain is a set of
+terms, and the !!{constant}s and !!{function}s are interpreted so as
+to guarantee that $\Value{t}{M} = t$. The atomic !!{formula}s
+in~$\Theta$ are used to define $\Assign{R}{M}$ in such a way as to
+guarantee that $\Sat{M}{R(t_1, \dots, t_n)}$ iff $R(t_1, \dots, t_n)
+\in \Theta$. 
+
+\begin{lem}\ollabel{lem:truth}
+For all $!A \in \Theta \cup \Xi$:
+\begin{enumerate}
+  \item If $!A \in \Theta$ then $\Sat{M}{!A}$.
+  \item If $!A \in \Xi$ then $\Sat/{M}{!A}$.
+\end{enumerate}
+\end{lem}
+
+\begin{proof}
+  By induction on $\depth{!A}$.
+
+First assume $!A$ is atomic, i.e., either $!A \ident \lfalse$ or $!A
+\ident R(t_1, \dots, t_m)$.
+
+Because $\Pi_n \Sequent \Lambda_n$ is a failure branch, no $\Pi_n$ can
+contain $\lfalse$ (otherwise $\Pi_n \Sequent \Lambda_n$ would be an
+axiom). $\Sat{M}{R(t_1, \dots, t_m)}$ iff $R(t_1, \dots, t_m) \in
+\Theta$ by definition of~$\Struct{M}$. Together we have: if $!A \in
+\Theta$, then $\Sat{M}{!A}$.
+
+If $!A$ is atomic and $!A \in \Pi_n$ then $!A \in \Pi_{n+1}$ and if
+$!A \in \Lambda_n$ then $!A \in \Lambda_{n+1}$. (This follows from the
+way the proof search algorithm generates successor sequents.) Hence,
+if $!A \in \Theta \cap \Xi$ then for some~$n$, $!A \in \Pi_n \cap
+\Lambda_n$. This means that $\Pi_n \Sequent \Lambda_n$ is an axiom,
+and the failure branch can contain no axioms. So $!A \notin \Theta
+\cap \Xi$ for atomic~$!A$ by construction, and consequently if $!A \in
+\Xi$ then $!A \notin \Theta$. This implies that if $!A \in \Xi$ then
+$\Sat/{M}{!A}$ by definition of~$\Struct{M}$.
+
+For the inductive step, assume (1) and (2) hold for all !!{formula}s
+of lower !!{depth} than~$!A$. We prove (1) and (2) for $!A$ by
+distinguishing cases.
+
+First note that when $!A^i$ occurs in $\Pi_n \Sequent \Lambda_n$ then
+$!A^i$ also occurs in $\Pi_{n+1} \Sequent \Lambda_{n+1}$ unless $i$ is
+the smallest index in $\Pi_n \Sequent \Lambda_n$. Since the smallest
+index increases in topmost sequents added at each stage, eventually we
+reach $\Pi_n \Sequent \Lambda_n$ in which $!A^i$ occurs, and $i$ is
+the smallest index. At stage $n+1$ the algorithm reduces~$!A^i$. In
+other words, if $!A \in \Theta$, then for some $n$, $\Pi_n = \Pi_n',
+!A^i$ and $i$ is the smallest index. And if $!A \in \Xi$, then for
+some $n$, $\Lambda_n = \Lambda_n', !A^i$ and $i$~is the smallest
+index.
+
+\begin{enumerate}
+  \item $!A \in \Theta$ and $!A \ident !B \land !C$. Then for some
+  $n$, $\Pi_n = \Pi_n', (!B \land !C)^i$. $\Pi_{n+1} \Sequent
+  \Lambda_{n+1}$ is the corresponding premise of~\LeftR{\land}, i.e.,
+  $\Pi_{n+1} = \Pi_n', !B^k, !C^{k+1}$. Consequently, $!B, !C \in
+  \Theta$. By inductive hypothesis, $\Sat{M}{!B}$ and $\Sat{M}{!C}$.
+  By definition of $\Sat{M}{}$, we have $\Sat{M}{!B \land !C}$.
+
+  \item $!A \in \Xi$ and $!A \ident !B \land !C$. Then for some $n$,
+  $\Lambda_n = \Lambda_n', !B \land !C$. $\Pi_{n+1} \Sequent
+  \Lambda_{n+1}$ is one of the two premises of~\RightR{\land} with
+  conclusion $\Pi_n \Sequent \Lambda'_n, !B \land !C$, i.e.,
+  $\Lambda_{n+1} = \Lambda_n', !B^k$ or $\Lambda_{n+1} = \Lambda_n',
+  !C^k$. Consequently, either $!B \in \Xi$ or $!C \in \Xi$. By
+  inductive hypothesis, either $\Sat/{M}{!B}$ or $\Sat/{M}{!C}$. By
+  definition of $\Sat{M}{}$, we have $\Sat/{M}{!B \land !C}$.
+  
+  \item The cases where $!A \ident \lnot !B$, $!A \ident !B \lor !C$,
+  and $!A \ident !B \lif !C$ are similar and left as exercises.
+
+  \item $!A \in \Theta$ and $!A \ident \lexists[x][!B(x)]$. Then for
+  some $n$, $\Pi_n = \Pi_n', \lexists[x][!B(x)]^i$. $\Pi_{n+1}
+  \Sequent \Lambda_{n+1}$ is the corresponding premise
+  of~\LeftR{\lexists}, i.e., $\Pi_{n+1} = \Pi_n', !B(c)^k$ for
+  some~$c$. Consequently, $!B(c) \in \Theta$ and~$c \in C$. By
+  inductive hypothesis, $\Sat{M}{!B(c)}$. By definition of
+  $\Sat{M}{}$, we have $\Sat{M}{\lexists[x][!B(x)]}$.
+
+  \item $!A \in \Xi$ and $!A \ident \lexists[x][!B(x)]$. Then for some
+  $n$, $\Lambda_n = \Lambda_n', \lexists[x][!B(x)]^i$. Since every time
+  $\lexists[x][!B(x)]$ is reduced, $\lexists[x][!B(x)]$ remains on the
+  right side of the premise sequent with a new index,
+  $\lexists[x][!B(x)]$ is reduced infinitely often on the right side
+  in a failure branch if it occurs there. Every term $t \in
+  \Domain{M}$ eventually is ``the first term only containing constants
+  in~$C_n$ not already used in a reduction of $\lexists[x][!B(x)]$ on
+  the right'' on a failure branch. Hence, for all $t \in \Domain{M}$,
+  $!B(t) \in \Lambda_n$ for some~$n$ and consequently $!B(t) \in \Xi$.
+  By inductive hypothesis, $\Sat/{M}{!B(t)}$ for all $t \in
+  \Domain{M}$. By definition of $\Sat{M}{}$, we have
+  $\Sat/{M}{\lexists[x][!B(x)]}$.
+
+  \item The cases where $!A \ident \lforall[x][!B(x)]$ are similar and
+  left as exercises.
+\end{enumerate}
+\end{proof}
+
+\begin{cor}\ollabel{cor:complete} The proof search algorithm for
+\Log{G3c} is complete: if it aborts or never halts, the starting
+sequent~$\Gamma \Sequent \Delta$ is not valid and hence has no
+!!{proof}.
+\end{cor}
+
+\begin{proof}
+  If the algorithm aborts or never halts, there is a failure branch
+  from which $\Struct{M}$ can be defined. By \olref{lem:truth}, for
+  all $!A \in \Gamma$, $\Sat{M}{!A}$ and for all $!A \in \Delta$,
+  $\Sat/{M}{!A}$. (Recall that $\Pi_0 = \Gamma$ and $\Lambda_0 =
+  \Delta$, so $\Gamma \subseteq \Theta$ and $\Delta \subseteq \Xi$.)
+  So $\Gamma \Sequent \Delta$ is not valid. By soundness of~\Log{G3c},
+  $\Gamma \Sequent \Delta$ has no !!{proof}.
+\end{proof}
+
+\begin{cor}
+\Log{G3c} is complete: if $\Gamma \Sequent \Delta$ is valid,
+$\Log{G3c} \Proves \Gamma \Sequent \Delta$.
+\end{cor}
+
+\begin{proof}
+  We prove the contrapositive. Suppose $\Log{G3c} \Proves/ \Gamma
+  \Sequent \Delta$. Then the proof search algorithm must abort or
+  never halt, as there is no !!{proof} to be found. By \olref{cor:complete}, $\Gamma \Sequent \Delta$ is not
+  valid.
+\end{proof}
+
+
+\end{document}

content/proof-theory/proof-search/introduction.tex

@@ -0,0 +1,119 @@
+% Part: proof-theory
+% Chapter: proof-search
+% Section: introduction
+
+\documentclass[../../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{pt}{ps}{int}
+
+\olsection{Introduction}
+
+The axioms and inference rules of !!{proof} systems like \Log{G3c} or
+\Log{N1i} define what trees of sequents or !!{formula}s count as
+correct !!{proof}s. Given such a tree of sequents or !!{formula}s
+(possibly with additional information such as which rules are applied
+at each step, or labels for assumptions and inference rules that
+discharge them) the definitions of axioms and rules allow us to check
+whether the given tree is a correct !!{proof}. It is a diferent, and
+typically more difficult, problem to \emph{find} !!a{proof} of a given
+sequent or of a given !!{formula} from given assumptions. That is the
+problem of \emph{proof search}.
+
+There is a very simple-minded procedure for proof search. We can think
+of !!{formula}s as sequences of symbols from a finite alphabet.
+Sequents and trees of sequents or !!{formula}s can be thought of as
+sequences of !!{formula}s as well (perhaps using special brackets to
+indicate tree branching). The axioms and rules allow us to
+mechanically check if a sequence of symbols represents a correct
+!!{proof}. Consequently, we can mechanically generate \emph{all
+possible} correct !!{proof}s (by generating all sequences of symbols
+from the alphabet used to represent !!{proof}s and checking for each
+candidate sequence whether it represents a correct !!{proof}). The
+simple-minded proof search precedure is: generate all correct
+!!{proof}s until we find one that is a !!{proof} of the given sequent
+(or of the given !!{formula} with open assumptions among the given
+ones).
+
+A better method is to use the naive method you'd use to find
+!!a{proof} by hand: you start with the end-sequent, pick !!a{formula},
+and apply an inference rule ``backwards'' to generate a premise or
+premises which, if they had !!{proof}s, would combine with the last
+inference to !!a{proof} of the given sequent. A similar method
+(although more complicated) is what you'd use to find !!a{proof} in a
+natural deduction system.
+
+But this method is not fool-proof: if you pick the wrong rule, or
+!!{formula}s in the wrong order, you may hit a dead end. It is also
+not completely specified: at each point, there may be more than one
+possible !!{formula} to chose, or more than one rule to apply
+backwards. A \emph{proof search algorithm} is a completely specified
+procedure that will find !!a{proof} if one exists (i.e., is
+fool-proof).
+
+Some !!{proof} systems lend themselves to simpler proof search
+algorithms than others. In sequent systems, the !!{main operator} of
+!!a{formula}, and whether it occurs on the left or the right,
+determines which rule to apply backwards. E.g., if you want to find
+!!a{proof} of $\Gamma \Sequent \Delta, !A \land !B$ in which $!A \land
+!B$ occurs on the right, you should apply \RightR{\land} backwards and
+generate two corresponding premises $\Gamma \Sequent \Delta, !A$ and
+$\Gamma \Sequent \Delta, !B$. If your system is \Log{G1c}, however,
+the presence of contraction makes things more difficult because it
+gives you more options: You could also apply \RightR{\Contraction}
+backward and generate the premise $\Gamma \Sequent \Delta, !A \land
+!B, !A \land !B$ instead. And then the premise $\Gamma \Sequent
+\Delta, !A \land !B, !A \land !B, !A \land !B$, and so on. In
+\Log{G2c} it's even worse. Applying the rule \RightR{\land} backwards
+also means you have to guess $\Gamma_1$, $\Gamma_2$ such that $\Gamma
+= \Gamma_1 \cup \Gamma_2$ and $\Delta_1$, $\Delta_2$ such that $\Delta
+= \Delta_1 \cup \Delta_2$ and try your luck with the premises
+$\Gamma_1 \Sequent \Delta_1, !A$ and $\Gamma_2 \Sequent \Delta_2, !B$.
+A wrong guess might lead you into a dead end later on, and you'd have
+to backtrack to the beginning and pick different $\Gamma_1$,
+$\Gamma_2$, $\Delta_1$, $\Delta_2$. If the !!{formula} is $!A \lor !B$
+you have to chose one of the two possibilities for \RightR{\lor},
+producing one of the two possible premises $\Gamma \Sequent \Delta,
+!A$ or $\Gamma \Sequent \Delta, !B$. A wrong choice would again lead
+to having to backtrack.
+
+The system \Log{G3c} does not have these problems. It has no
+structural rules, and the choice of inference rule is determined by
+the !!{main operator} and the side the !!{formula} occurs on. Hence,
+\Log{G3c} is better suited to proof search than \Log{G1c} or
+\Log{G2c}. A successful search will yield !!a{proof} in \Log{G3c}, and
+that !!{proof} can then be translated into \Log{G1c} or \Log{G2c} (or
+\Log{N1c} for that matter). So having a proof search algorithm for
+\Log{G3c} and translation algorithms for \Log{G3c} !!{proof}s to
+!!{proof}s in other systems also solves the proof search methods for
+those systems.
+
+How do we know that a proof search algorithm is fool-proof? This would
+involve showing that if the algorithm fails to find !!a{proof}, no
+!!{proof} can exist. After all, if we pick a bad algorithm, we might
+run into cases where it fails to find a proof even if one exists. This
+is not a problem the simple minded algorithm has, because it searches
+through all possible !!{proof}s. But a proof search algorithm is
+supposed to be efficient and expend the minimum amount of effort.
+
+The key idea to showing that a proof search algorithm is fool-proof is
+to show that if the algorithm fails, we can show from the way it fails
+that the sequent can't possibly have !!a{proof}. And the way to show
+that is to show that it is not valid. In classical first-order logic,
+valid sequents $\Gamma \Sequent \Delta$ are those where every
+!!{structure} makes at least one !!{formula} in $\Gamma$ is false or
+at least one !!{formula} in~$\Delta$ is true. \Log{G3c} is
+\emph{sound}, i.e., it !!{prove}s only valid sequents. This is
+established by induction on !!{proof}s: Axioms are obvioulsy valid,
+and if the premises of a rule are valid, so is the conclusion. To show
+that a proof search algorithm is fool-proof we show that if the search
+for !!a{proof} of $\Gamma \Sequent \Delta$ fails, we can define
+!!a{structure} in which all !!{formula}s in $\Gamma$ are true and all
+!!{formula}s in~$\Delta$ are false. This also establishes that
+\Log{G3c} is \emph{complete}, i.e., that if $\Gamma \Sequent \Delta$
+is valid, there is a \Log{G3c}-!!{proof} of it. Since all failed
+proof searches show that $\Gamma \Sequent \Delta$ is invalid, every
+proof search for a valid sequent must succeed.
+
+\end{document}

content/proof-theory/proof-search/proof-search.tex

@@ -0,0 +1,17 @@
+% Part: proof-theory
+% Chapter: proof-search
+
+\documentclass[../../../include/open-logic-chapter]{subfiles}
+
+\begin{document}
+
+\olchapter{pt}{ps}{Proof Search}
+
+\olimport{introduction}
+\olimport{search-algorithm}
+\olimport{completeness}
+\olimport{tableaux}
+
+\OLEndChapterHook
+
+\end{document}