doc-src/Logics/LK.tex

 
 No generic packages are instantiated, since Isabelle does not provide
 packages for sequent calculi at present.  \LK{} implements a classical
 logic theorem prover that is as powerful as the generic classical reasoner,
 except that it does not perform equality reasoning.
+
+To work in LK, start up Isabelle specifying  \texttt{Sequents} as the
+object-logic.  Once in Isabelle, change the context to theory \texttt{LK.thy}:
+\begin{ttbox}
+isabelle Sequents
+context LK.thy;
+\end{ttbox}
+Model logic and linear logic are also available, but unfortunately they are
+not documented.
 
 
 \begin{figure} 
 \begin{center}
 \begin{tabular}{rrr} 

 
 \section{Unification for lists}
 Higher-order unification includes associative unification as a special
 case, by an encoding that involves function composition
 \cite[page~37]{huet78}.  To represent lists, let $C$ be a new constant.
-The empty list is $\lambda x.x$, while $[t@1,t@2,\ldots,t@n]$ is
+The empty list is $\lambda x. x$, while $[t@1,t@2,\ldots,t@n]$ is
 represented by
-\[ \lambda x.C(t@1,C(t@2,\ldots,C(t@n,x))).  \]
+\[ \lambda x. C(t@1,C(t@2,\ldots,C(t@n,x))).  \]
 The unifiers of this with $\lambda x.\Var{f}(\Var{g}(x))$ give all the ways
 of expressing $[t@1,t@2,\ldots,t@n]$ as the concatenation of two lists.
 
 Unlike orthodox associative unification, this technique can represent certain
 infinite sets of unifiers by flex-flex equations.   But note that the term
-$\lambda x.C(t,\Var{a})$ does not represent any list.  Flex-flex constraints
+$\lambda x. C(t,\Var{a})$ does not represent any list.  Flex-flex constraints
 containing such garbage terms may accumulate during a proof.
 \index{flex-flex constraints}
 
 This technique lets Isabelle formalize sequent calculus rules,
 where the comma is the associative operator:

 \tdx{notR}    $H, P |- $E, $F ==> $H |- $E, ~P, $F
 \tdx{notL}    $H, $G |- $E, P ==> $H, ~P, $G |- $E
 
 \tdx{FalseL}  $H, False, $G |- $E
 
-\tdx{allR}    (!!x.$H|- $E, P(x), $F) ==> $H|- $E, ALL x.P(x), $F
-\tdx{allL}    $H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G|- $E
+\tdx{allR}    (!!x. $H|- $E, P(x), $F) ==> $H|- $E, ALL x. P(x), $F
+\tdx{allL}    $H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G|- $E
             
-\tdx{exR}     $H|- $E, P(x), $F, EX x.P(x) ==> $H|- $E, EX x.P(x), $F
-\tdx{exL}     (!!x.$H, P(x), $G|- $E) ==> $H, EX x.P(x), $G|- $E
-
-\tdx{The}     [| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
-        $H |- $E, P(THE x.P(x)), $F
+\tdx{exR}     $H|- $E, P(x), $F, EX x. P(x) ==> $H|- $E, EX x. P(x), $F
+\tdx{exL}     (!!x. $H, P(x), $G|- $E) ==> $H, EX x. P(x), $G|- $E
+
+\tdx{The}     [| $H |- $E, P(a), $F;  !!x. $H, P(x) |- $E, x=a, $F |] ==>
+        $H |- $E, P(THE x. P(x)), $F
 \subcaption{Logical rules}
 \end{ttbox}
 
 \caption{Rules of {\tt LK}}  \label{lk-rules}
 \end{figure}

 
 Figure~\ref{lk-syntax} gives the syntax for {\tt LK}, which is complicated
 by the representation of sequents.  Type $sobj\To sobj$ represents a list
 of formulae.
 
-The {\bf definite description} operator~$\iota x.P[x]$ stands for some~$a$
+The {\bf definite description} operator~$\iota x. P[x]$ stands for some~$a$
 satisfying~$P[a]$, if one exists and is unique.  Since all terms in \LK{}
 denote something, a description is always meaningful, but we do not know
 its value unless $P[x]$ defines it uniquely.  The Isabelle notation is
-\hbox{\tt THE $x$.$P[x]$}.  The corresponding rule (Fig.\ts\ref{lk-rules})
+\hbox{\tt THE $x$. $P[x]$}.  The corresponding rule (Fig.\ts\ref{lk-rules})
 does not entail the Axiom of Choice because it requires uniqueness.
 
 Figure~\ref{lk-grammar} presents the grammar of \LK.  Traditionally,
 \(\Gamma\) and \(\Delta\) are meta-variables for sequences.  In Isabelle's
 notation, the prefix~\verb|$| on a variable makes it range over sequences.

             $H |- $E, P<->Q, $F
 
 \tdx{iffL}        [| $H, $G |- $E, P, Q;  $H, Q, P, $G |- $E |] ==>
             $H, P<->Q, $G |- $E
 
-\tdx{allL_thin}   $H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E
-\tdx{exR_thin}    $H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F
+\tdx{allL_thin}   $H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E
+\tdx{exR_thin}    $H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F
 \end{ttbox}
 
 \caption{Derived rules for {\tt LK}} \label{lk-derived}
 \end{figure}
 

 is easy using~{\LK}, as you can see by comparing this proof with the one
 given in~\S\ref{fol-cla-example}.  From a logical point of view, the
 proofs are essentially the same; the key step here is to use \tdx{exR}
 rather than the weaker~\tdx{exR_thin}.
 \begin{ttbox}
-goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
+Goal "|- EX y. ALL x. P(y)-->P(x)";
 {\out Level 0}
 {\out  |- EX y. ALL x. P(y) --> P(x)}
 {\out  1.  |- EX y. ALL x. P(y) --> P(x)}
 by (resolve_tac [exR] 1);
 {\out Level 1}

 {\out Level 6}
 {\out  |- EX y. ALL x. P(y) --> P(x)}
 {\out  1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)}
 \end{ttbox}
 Subgoal~1 seems to offer lots of possibilities.  Actually the only useful
-step is instantiating~$\Var{x@7}$ to $\lambda x.x$,
+step is instantiating~$\Var{x@7}$ to $\lambda x. x$,
 transforming~$\Var{x@7}(x)$ into~$x$.
 \begin{ttbox}
 by (resolve_tac [basic] 1);
 {\out Level 7}
 {\out  |- EX y. ALL x. P(y) --> P(x)}
 {\out No subgoals!}
 \end{ttbox}
 This theorem can be proved automatically.  Because it involves quantifier
 duplication, we employ best-first search:
 \begin{ttbox}
-goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
+Goal "|- EX y. ALL x. P(y)-->P(x)";
 {\out Level 0}
 {\out  |- EX y. ALL x. P(y) --> P(x)}
 {\out  1.  |- EX y. ALL x. P(y) --> P(x)}
 by (best_tac LK_dup_pack 1);
 {\out Level 1}

 short manual proof.  See the directory {\tt LK/ex} for many more
 examples.
 
 We set the main goal and move the negated formula to the left.
 \begin{ttbox}
-goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
+Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
 {\out Level 0}
 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
 {\out  1.  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
 by (resolve_tac [notR] 1);
 {\out Level 1}