doc-src/Logics/LK.tex
 changeset 104 d8205bb279a7 child 111 1b3cddf41b2d
equal inserted replaced
103:30bd42401ab2 104:d8205bb279a7

     1 %% $Id$

     2 \chapter{First-order sequent calculus}

     3 The directory~\ttindexbold{LK} implements classical first-order logic through

     4 Gentzen's sequent calculus (see Gallier~\cite{gallier86} or

     5 Takeuti~\cite{takeuti87}).  Resembling the method of semantic tableaux, the

     6 calculus is well suited for backwards proof.  Assertions have the form

     7 $$\Gamma\turn \Delta$$, where $$\Gamma$$ and $$\Delta$$ are lists of

     8 formulae.  Associative unification, simulated by higher-order unification,

     9 handles lists.

    10

    11 The logic is many-sorted, using Isabelle's type classes.  The

    12 class of first-order terms is called {\it term}.  No types of individuals

    13 are provided, but extensions can define types such as $nat::term$ and type

    14 constructors such as $list::(term)term$.  Below, the type variable $\alpha$

    15 ranges over class {\it term\/}; the equality symbol and quantifiers are

    16 polymorphic (many-sorted).  The type of formulae is~{\it o}, which belongs

    17 to class {\it logic}.

    18

    19 No generic packages are instantiated, since Isabelle does not provide

    20 packages for sequent calculi at present.  \LK{} implements a classical

    21 logic theorem prover that is as powerful as the generic classical module,

    22 except that it does not perform equality reasoning.

    23

    24

    25 \section{Unification for lists}

    26 Higher-order unification includes associative unification as a special

    27 case, by an encoding that involves function composition

    28 \cite[page~37]{huet78}.  To represent lists, let $C$ be a new constant.

    29 The empty list is $\lambda x.x$, while $[t@1,t@2,\ldots,t@n]$ is

    30 represented by

    31 $\lambda x.C(t@1,C(t@2,\ldots,C(t@n,x))).$

    32 The unifiers of this with $\lambda x.\Var{f}(\Var{g}(x))$ give all the ways

    33 of expressing $[t@1,t@2,\ldots,t@n]$ as the concatenation of two lists.

    34

    35 Unlike orthodox associative unification, this technique can represent certain

    36 infinite sets of unifiers by flex-flex equations.   But note that the term

    37 $\lambda x.C(t,\Var{a})$ does not represent any list.  Flex-flex equations

    38 containing such garbage terms may accumulate during a proof.

    39

    40 This technique lets Isabelle formalize sequent calculus rules,

    41 where the comma is the associative operator:

    42 $\infer[\conj\hbox{-left}]    43 {\Gamma,P\conj Q,\Delta \turn \Theta}    44 {\Gamma,P,Q,\Delta \turn \Theta}$

    45 Multiple unifiers occur whenever this is resolved against a goal containing

    46 more than one conjunction on the left.  Explicit formalization of sequents

    47 can be tiresome, but gives precise control over contraction and weakening,

    48 needed to handle relevant and linear logics.

    49

    50 \LK{} exploits this representation of lists.  As an alternative, the

    51 sequent calculus can be formalized using an ordinary representation of

    52 lists, with a logic program for removing a formula from a list.  Amy Felty

    53 has applied this technique using the language $\lambda$Prolog~\cite{felty91a}.

    54

    55

    56 \begin{figure}

    57 \begin{center}

    58 \begin{tabular}{rrr}

    59   \it name    	&\it meta-type 		& \it description	\\

    60   \idx{Trueprop}& $o\To prop$		& coercion to $prop$	\\

    61   \idx{Seqof}   & $[o,sobj]\To sobj$  	& singleton sequence	\\

    62   \idx{Not}	& $o\To o$		& negation ($\neg$) 	\\

    63   \idx{True}	& $o$			& tautology ($\top$) 	\\

    64   \idx{False}	& $o$			& absurdity ($\bot$)

    65 \end{tabular}

    66 \end{center}

    67 \subcaption{Constants}

    68

    69 \begin{center}

    70 \begin{tabular}{llrrr}

    71   \it symbol &\it name	   &\it meta-type & \it precedence & \it description \\

    72   \idx{ALL}  & \idx{All}  & $(\alpha\To o)\To o$ & 10 &

    73 	universal quantifier ($\forall$) \\

    74   \idx{EX}   & \idx{Ex}   & $(\alpha\To o)\To o$ & 10 &

    75 	existential quantifier ($\exists$) \\

    76   \idx{THE} & \idx{The}  & $(\alpha\To o)\To \alpha$ & 10 &

    77 	definite description ($\iota$)

    78 \end{tabular}

    79 \end{center}

    80 \subcaption{Binders}

    81

    82 \begin{center}

    83 \indexbold{*"=}

    84 \indexbold{&@{\tt\&}}

    85 \indexbold{*"|}

    86 \indexbold{*"-"-">}

    87 \indexbold{*"<"-">}

    88 \begin{tabular}{rrrr}

    89     \it symbol  & \it meta-type & \it precedence & \it description \\

    90     \tt = &     $[\alpha,\alpha]\To o$   & Left 50 & equality ($=$) \\

    91     \tt \& &    $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\

    92     \tt | &     $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\

    93     \tt --> &   $[o,o]\To o$ & Right 25 & implication ($\imp$) \\

    94     \tt <-> &   $[o,o]\To o$ & Right 25 & biconditional ($\bimp$)

    95 \end{tabular}

    96 \end{center}

    97 \subcaption{Infixes}

    98

    99 \begin{center}

   100 \begin{tabular}{rrr}

   101   \it external		& \it internal	& \it description \\

   102   \tt $\Gamma$ |- $\Delta$  &  \tt Trueprop($\Gamma$, $\Delta$) &

   103         sequent $\Gamma\turn \Delta$

   104 \end{tabular}

   105 \end{center}

   106 \subcaption{Translations}

   107 \caption{Syntax of {\tt LK}} \label{lk-syntax}

   108 \end{figure}

   109

   110

   111 \begin{figure}

   112 \dquotes

   113 $\begin{array}{rcl}    114 prop & = & sequence " |- " sequence     115 \\[2ex]    116 sequence & = & elem \quad (", " elem)^* \\    117 & | & empty     118 \\[2ex]    119 elem & = & "\ " id \\    120 & | & "\ " var \\    121 & | & formula     122 \\[2ex]    123 formula & = & \hbox{expression of type~o} \\    124 & | & term " = " term \\    125 & | & "\ttilde\ " formula \\    126 & | & formula " \& " formula \\    127 & | & formula " | " formula \\    128 & | & formula " --> " formula \\    129 & | & formula " <-> " formula \\    130 & | & "ALL~" id~id^* " . " formula \\    131 & | & "EX~~" id~id^* " . " formula \\    132 & | & "THE~" id~ " . " formula    133 \end{array}    134$

   135 \caption{Grammar of {\tt LK}} \label{lk-grammar}

   136 \end{figure}

   137

   138

   139 \begin{figure}

   140 \begin{ttbox}

   141 \idx{basic}       $H, P,$G |- $E, P,$F

   142 \idx{thinR}       $H |-$E, $F ==>$H |- $E, P,$F

   143 \idx{thinL}       $H,$G |- $E ==>$H, P, $G |-$E

   144 \idx{cut}         [| $H |-$E, P;  $H, P |-$E |] ==> $H |-$E

   145 \subcaption{Structural rules}

   146

   147 \idx{refl}        $H |-$E, a=a, $F    148 \idx{sym}$H |- $E, a=b,$F ==> $H |-$E, b=a, $F    149 \idx{trans} [|$H|- $E, a=b,$F;  $H|-$E, b=c, $F |] ==>     150$H|- $E, a=c,$F

   151 \subcaption{Equality rules}

   152

   153 \idx{True_def}    True  == False-->False

   154 \idx{iff_def}     P<->Q == (P-->Q) & (Q-->P)

   155

   156 \idx{conjR}   [| $H|-$E, P, $F;$H|- $E, Q,$F |] ==> $H|-$E, P&Q, $F    157 \idx{conjL}$H, P, Q, $G |-$E ==> $H, P & Q,$G |- $E    158     159 \idx{disjR}$H |- $E, P, Q,$F ==> $H |-$E, P|Q, $F    160 \idx{disjL} [|$H, P, $G |-$E;  $H, Q,$G |- $E |] ==>$H, P|Q, $G |-$E

   161

   162 \idx{impR}    $H, P |-$E, Q, $F ==>$H |- $E, P-->Q,$

   163 \idx{impL}    [| $H,$G |- $E,P;$H, Q, $G |-$E |] ==> $H, P-->Q,$G |- $E    164     165 \idx{notR}$H, P |- $E,$F ==> $H |-$E, ~P, $F    166 \idx{notL}$H, $G |-$E, P ==> $H, ~P,$G |- $E    167     168 \idx{FalseL}$H, False, $G |-$E

   169 \subcaption{Propositional rules}

   170

   171 \idx{allR}    (!!x.$H|-$E, P(x), $F) ==>$H|- $E, ALL x.P(x),$F

   172 \idx{allL}    $H, P(x),$G, ALL x.P(x) |- $E ==>$H, ALL x.P(x), $G|-$E

   173

   174 \idx{exR}     $H|-$E, P(x), $F, EX x.P(x) ==>$H|- $E, EX x.P(x),$F

   175 \idx{exL}     (!!x.$H, P(x),$G|- $E) ==>$H, EX x.P(x), $G|-$E

   176

   177 \idx{The}     [| $H |-$E, P(a), $F; !!x.$H, P(x) |- $E, x=a,$F |] ==>

   178         $H |-$E, P(THE x.P(x)), $F    179 \subcaption{Quantifier rules}    180 \end{ttbox}    181     182 \caption{Rules of {\tt LK}} \label{lk-rules}    183 \end{figure}    184     185     186 \begin{figure}     187 \begin{ttbox}    188 \idx{conR}$H |- $E, P,$F, P ==> $H |-$E, P, $F    189 \idx{conL}$H, P, $G, P |-$E ==> $H, P,$G |- $E    190     191 \idx{symL}$H, $G, B = A |-$E ==> $H, A = B,$G |- $E    192     193 \idx{TrueR}$H |- $E, True,$F

   194

   195 \idx{iffR}        [| $H, P |-$E, Q, $F;$H, Q |- $E, P,$F |] ==>

   196             $H |-$E, P<->Q, $F    197     198 \idx{iffL} [|$H, $G |-$E, P, Q;  $H, Q, P,$G |- $E |] ==>    199$H, P<->Q, $G |-$E

   200

   201 \idx{allL_thin}   $H, P(x),$G |- $E ==>$H, ALL x.P(x), $G |-$E

   202 \idx{exR_thin}    $H |-$E, P(x), $F ==>$H |- $E, EX x.P(x),$F

   203 \end{ttbox}

   204

   205 \caption{Derived rules for {\tt LK}} \label{lk-derived}

   206 \end{figure}

   207

   208

   209 \section{Syntax and rules of inference}

   210 Figure~\ref{lk-syntax} gives the syntax for {\tt LK}, which is complicated

   211 by the representation of sequents.  Type $sobj\To sobj$ represents a list

   212 of formulae.

   213

   214 The {\bf definite description} operator~$\iota x.P(x)$ stands for the

   215 unique~$a$ satisfying~$P(a)$, if such exists.  Since all terms in \LK{}

   216 denote something, a description is always meaningful, but we do not know

   217 its value unless $P[x]$ defines it uniquely.  The Isabelle notation is

   218 \hbox{\tt THE $x$.$P[x]$}.

   219

   220 Traditionally, $$\Gamma$$ and $$\Delta$$ are meta-variables for sequences.

   221 In Isabelle's notation, the prefix~\verb|$| on a variable makes it range    222 over sequences. In a sequent, anything not prefixed by \verb|$| is taken

   223 as a formula.

   224

   225 The theory has the \ML\ identifier \ttindexbold{LK.thy}.

   226 Figure~\ref{lk-rules} presents the rules.  The connective $\bimp$ is

   227 defined using $\conj$ and $\imp$.  The axiom for basic sequents is

   228 expressed in a form that provides automatic thinning: redundant formulae

   229 are simply ignored.  The other rules are expressed in the form most

   230 suitable for backward proof --- they do not require exchange or contraction

   231 rules.  The contraction rules are actually derivable (via cut) in this

   232 formulation.

   233

   234 Figure~\ref{lk-derived} presents derived rules, including rules for

   235 $\bimp$.  The weakened quantifier rules discard each quantification after a

   236 single use; in an automatic proof procedure, they guarantee termination,

   237 but are incomplete.  Multiple use of a quantifier can be obtained by a

   238 contraction rule, which in backward proof duplicates a formula.  The tactic

   239 \ttindex{res_inst_tac} can instantiate the variable~{\tt?P} in these rules,

   240 specifying the formula to duplicate.

   241

   242 See the files \ttindexbold{LK/lk.thy} and \ttindexbold{LK/lk.ML}

   243 for complete listings of the rules and derived rules.

   244

   245

   246 \section{Tactics for the cut rule}

   247 According to the cut-elimination theorem, the cut rule can be eliminated

   248 from proofs of sequents.  But the rule is still essential.  It can be used

   249 to structure a proof into lemmas, avoiding repeated proofs of the same

   250 formula.  More importantly, the cut rule can not be eliminated from

   251 derivations of rules.  For example, there is a trivial cut-free proof of

   252 the sequent $$P\conj Q\turn Q\conj P$$.

   253 Noting this, we might want to derive a rule for swapping the conjuncts

   254 in a right-hand formula:

   255 $\Gamma\turn \Delta, P\conj Q\over \Gamma\turn \Delta, Q\conj P$

   256 The cut rule must be used, for $P\conj Q$ is not a subformula of $Q\conj    257 P$.  Most cuts directly involve a premise of the rule being derived (a

   258 meta-assumption).  In a few cases, the cut formula is not part of any

   259 premise, but serves as a bridge between the premises and the conclusion.

   260 In such proofs, the cut formula is specified by calling an appropriate

   261 tactic.

   262

   263 \begin{ttbox}

   264 cutR_tac : string -> int -> tactic

   265 cutL_tac : string -> int -> tactic

   266 \end{ttbox}

   267 These tactics refine a subgoal into two by applying the cut rule.  The cut

   268 formula is given as a string, and replaces some other formula in the sequent.

   269 \begin{description}

   270 \item[\ttindexbold{cutR_tac} {\it formula} {\it i}]

   271 reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It

   272 then deletes some formula from the right side of subgoal~$i$, replacing

   273 that formula by~$P$.

   274

   275 \item[\ttindexbold{cutL_tac} {\it formula} {\it i}]

   276 reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It

   277 then deletes some formula from the let side of the new subgoal $i+1$,

   278 replacing that formula by~$P$.

   279 \end{description}

   280 All the structural rules --- cut, contraction, and thinning --- can be

   281 applied to particular formulae using \ttindex{res_inst_tac}.

   282

   283

   284 \section{Tactics for sequents}

   285 \begin{ttbox}

   286 forms_of_seq       : term -> term list

   287 could_res          : term * term -> bool

   288 could_resolve_seq  : term * term -> bool

   289 filseq_resolve_tac : thm list -> int -> int -> tactic

   290 \end{ttbox}

   291 Associative unification is not as efficient as it might be, in part because

   292 the representation of lists defeats some of Isabelle's internal

   293 optimizations.  The following operations implement faster rule application,

   294 and may have other uses.

   295 \begin{description}

   296 \item[\ttindexbold{forms_of_seq} {\it t}]

   297 returns the list of all formulae in the sequent~$t$, removing sequence

   298 variables.

   299

   300 \item[\ttindexbold{could_res} $(t,u)$]

   301 tests whether two formula lists could be resolved.  List $t$ is from a

   302 premise (subgoal), while $u$ is from the conclusion of an object-rule.

   303 Assuming that each formula in $u$ is surrounded by sequence variables, it

   304 checks that each conclusion formula is unifiable (using {\tt could_unify})

   305 with some subgoal formula.

   306

   307 \item[\ttindexbold{could_resolve} $(t,u)$]

   308 tests whether two sequents could be resolved.  Sequent $t$ is a premise

   309 (subgoal), while $u$ is the conclusion of an object-rule.  It uses {\tt

   310 could_res} to check the left and right sides of the two sequents.

   311

   312 \item[\ttindexbold{filseq_resolve_tac} {\it thms} {\it maxr} {\it i}]

   313 uses {\tt filter_thms could_resolve} to extract the {\it thms} that are

   314 applicable to subgoal~$i$.  If more than {\it maxr\/} theorems are

   315 applicable then the tactic fails.  Otherwise it calls {\tt resolve_tac}.

   316 Thus, it is the sequent calculus analogue of \ttindex{filt_resolve_tac}.

   317 \end{description}

   318

   319

   320

   321 \section{Packaging sequent rules}

   322 For theorem proving, rules can be classified as {\bf safe} or {\bf

   323 unsafe}.  An unsafe rule (typically a weakened quantifier rule) may reduce

   324 a provable goal to an unprovable set of subgoals, and should only be used

   325 as a last resort.

   326

   327 A {\bf pack} is a pair whose first component is a list of safe

   328 rules, and whose second is a list of unsafe rules.  Packs can be extended

   329 in an obvious way to allow reasoning with various collections of rules.

   330 For clarity, \LK{} declares the datatype

   331 \ttindexbold{pack}:

   332 \begin{ttbox}

   333 datatype pack = Pack of thm list * thm list;

   334 \end{ttbox}

   335 The contents of any pack can be inspected by pattern-matching.  Packs

   336 support the following operations:

   337 \begin{ttbox}

   338 empty_pack  : pack

   339 prop_pack   : pack

   340 LK_pack     : pack

   341 LK_dup_pack : pack

   342 add_safes   : pack * thm list -> pack               \hfill{\bf infix 4}

   343 add_unsafes : pack * thm list -> pack               \hfill{\bf infix 4}

   344 \end{ttbox}

   345 \begin{description}

   346 \item[\ttindexbold{empty_pack}] is the empty pack.

   347

   348 \item[\ttindexbold{prop_pack}] contains the propositional rules, namely

   349 those for $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, along with the

   350 rules \ttindex{basic} and \ttindex{refl}.  These are all safe.

   351

   352 \item[\ttindexbold{LK_pack}]

   353 extends {\tt prop_pack} with the safe rules \ttindex{allR}

   354 and~\ttindex{exL} and the unsafe rules \ttindex{allL_thin} and

   355 \ttindex{exR_thin}.  Search using this is incomplete since quantified

   356 formulae are used at most once.

   357

   358 \item[\ttindexbold{LK_dup_pack}]

   359 extends {\tt prop_pack} with the safe rules \ttindex{allR}

   360 and~\ttindex{exL} and the unsafe rules \ttindex{allL} and~\ttindex{exR}.

   361 Search using this is complete, since quantified formulae may be reused, but

   362 frequently fails to terminate.  It is generally unsuitable for depth-first

   363 search.

   364

   365 \item[$pack$ \ttindexbold{add_safes} $rules$]

   366 adds some safe~$rules$ to the pack~$pack$.

   367

   368 \item[$pack$ \ttindexbold{add_unsafes} $rules$]

   369 adds some unsafe~$rules$ to the pack~$pack$.

   370 \end{description}

   371

   372

   373 \section{Proof procedures}

   374 The \LK{} proof procedure is similar to the generic classical module

   375 described in the {\em Reference Manual}.  In fact it is simpler, since it

   376 works directly with sequents rather than simulating them.  There is no need

   377 to distinguish introduction rules from elimination rules, and of course

   378 there is no swap rule.  As always, Isabelle's classical proof procedures

   379 are less powerful than resolution theorem provers.  But they are more

   380 natural and flexible, working with an open-ended set of rules.

   381

   382 Backtracking over the choice of a safe rule accomplishes nothing: applying

   383 them in any order leads to essentially the same result.  Backtracking may

   384 be necessary over basic sequents when they perform unification.  Suppose

   385 that~0, 1, 2,~3 are constants in the subgoals

   386 $\begin{array}{c}    387 P(0), P(1), P(2) \turn P(\Var{a}) \\    388 P(0), P(2), P(3) \turn P(\Var{a}) \\    389 P(1), P(3), P(2) \turn P(\Var{a})     390 \end{array}    391$

   392 The only assignment that satisfies all three subgoals is $\Var{a}\mapsto 2$,

   393 and this can only be discovered by search.  The tactics given below permit

   394 backtracking only over axioms, such as {\tt basic} and {\tt refl}.

   395

   396

   397 \subsection{Method A}

   398 \begin{ttbox}

   399 reresolve_tac   : thm list -> int -> tactic

   400 repeat_goal_tac : pack -> int -> tactic

   401 pc_tac          : pack -> int -> tactic

   402 \end{ttbox}

   403 These tactics use a method developed by Philippe de Groote.  A subgoal is

   404 refined and the resulting subgoals are attempted in reverse order.  For

   405 some reason, this is much faster than attempting the subgoals in order.

   406 The method is inherently depth-first.

   407

   408 At present, these tactics only work for rules that have no more than two

   409 premises.  They {\bf fail} if they can do nothing.

   410 \begin{description}

   411 \item[\ttindexbold{reresolve_tac} $thms$ $i$]

   412 repeatedly applies the $thms$ to subgoal $i$ and the resulting subgoals.

   413

   414 \item[\ttindexbold{repeat_goal_tac} $pack$ $i$]

   415 applies the safe rules in the pack to a goal and the resulting subgoals.

   416 If no safe rule is applicable then it applies an unsafe rule and continues.

   417

   418 \item[\ttindexbold{pc_tac} $pack$ $i$]

   419 applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$.

   420 \end{description}

   421

   422

   423 \subsection{Method B}

   424 \begin{ttbox}

   425 safe_goal_tac : pack -> int -> tactic

   426 step_tac      : pack -> int -> tactic

   427 fast_tac      : pack -> int -> tactic

   428 best_tac      : pack -> int -> tactic

   429 \end{ttbox}

   430 These tactics are precisely analogous to those of the generic classical

   431 module.  They use Method~A' only on safe rules.  They {\bf fail} if they
       
   432 can do nothing.
       
   433 \begin{description}
       
   434 \item[\ttindexbold{safe_goal_tac} $pack$ $i$] 
       
   435 applies the safe rules in the pack to a goal and the resulting subgoals.
       
   436 It ignores the unsafe rules.  
       
   437 
       
   438 \item[\ttindexbold{step_tac} $pack$ $i$] 
       
   439 either applies safe rules (using {\tt safe_goal_tac}) or applies one unsafe
       
   440 rule.
       
   441 
       
   442 \item[\ttindexbold{fast_tac} $pack$ $i$] 
       
   443 applies {\tt step_tac} using depth-first search to solve subgoal~$i$.
       
   444 Despite the names, {\tt pc_tac} is frequently faster.
       
   445 
       
   446 \item[\ttindexbold{best_tac} $pack$ $i$] 
       
   447 applies {\tt step_tac} using best-first search to solve subgoal~$i$.  It is
       
   448 particularly useful for quantifier duplication (using \ttindex{LK_dup_pack}).
       
   449 \end{description}
       
   450 
       
   451 
       
   452 
       
   453 \section{A simple example of classical reasoning} 
       
   454 The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the
       
   455 classical treatment of the existential quantifier.  Classical reasoning
       
   456 is easy using~{\LK}, as you can see by comparing this proof with the one
       
   457 given in~\S\ref{fol-cla-example}.  From a logical point of view, the
       
   458 proofs are essentially the same; the key step here is to use \ttindex{exR}
       
   459 rather than the weaker~\ttindex{exR_thin}.
       
   460 \begin{ttbox}
       
   461 goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
       
   462 {\out Level 0}
       
   463 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   464 {\out  1.  |- EX y. ALL x. P(y) --> P(x)}
       
   465 by (resolve_tac [exR] 1);
       
   466 {\out Level 1}
       
   467 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   468 {\out  1.  |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
       
   469 \end{ttbox}
       
   470 There are now two formulae on the right side.  Keeping the existential one
       
   471 in reserve, we break down the universal one.
       
   472 \begin{ttbox}
       
   473 by (resolve_tac [allR] 1);
       
   474 {\out Level 2}
       
   475 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   476 {\out  1. !!x.  |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
       
   477 by (resolve_tac [impR] 1);
       
   478 {\out Level 3}
       
   479 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   480 {\out  1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)}
       
   481 \end{ttbox}
       
   482 Because {\LK} is a sequent calculus, the formula~$P(\Var{x})$ does not
       
   483 become an assumption;  instead, it moves to the left side.  The
       
   484 resulting subgoal cannot be instantiated to a basic sequent: the bound
       
   485 variable~$x$ is not unifiable with the unknown~$\Var{x}$.
       
   486 \begin{ttbox}
       
   487 by (resolve_tac [basic] 1);
       
   488 {\out by: tactic failed}
       
   489 \end{ttbox}
       
   490 We reuse the existential formula using~\ttindex{exR_thin}, which discards
       
   491 it; we will not need it a third time.  We again break down the resulting
       
   492 formula.
       
   493 \begin{ttbox}
       
   494 by (resolve_tac [exR_thin] 1);
       
   495 {\out Level 4}
       
   496 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   497 {\out  1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)}
       
   498 by (resolve_tac [allR] 1);
       
   499 {\out Level 5}
       
   500 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   501 {\out  1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)}
       
   502 by (resolve_tac [impR] 1);
       
   503 {\out Level 6}
       
   504 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   505 {\out  1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)}
       
   506 \end{ttbox}
       
   507 Subgoal~1 seems to offer lots of possibilities.  Actually the only useful
       
   508 step is instantiating~$\Var{x@7}$ to $\lambda x.x$,
       
   509 transforming~$\Var{x@7}(x)$ into~$x$.
       
   510 \begin{ttbox}
       
   511 by (resolve_tac [basic] 1);
       
   512 {\out Level 7}
       
   513 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   514 {\out No subgoals!}
       
   515 \end{ttbox}
       
   516 This theorem can be proved automatically.  Because it involves quantifier
       
   517 duplication, we employ best-first search:
       
   518 \begin{ttbox}
       
   519 goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
       
   520 {\out Level 0}
       
   521 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   522 {\out  1.  |- EX y. ALL x. P(y) --> P(x)}
       
   523 by (best_tac LK_dup_pack 1);
       
   524 {\out Level 1}
       
   525 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   526 {\out No subgoals!}
       
   527 \end{ttbox}
       
   528 
       
   529 
       
   530 
       
   531 \section{A more complex proof}
       
   532 Many of Pelletier's test problems for theorem provers \cite{pelletier86}
       
   533 can be solved automatically.  Problem~39 concerns set theory, asserting
       
   534 that there is no Russell set --- a set consisting of those sets that are
       
   535 not members of themselves:
       
   536 $\turn \neg (\exists x. \forall y. y\in x \bimp y\not\in y)$
       
   537 This does not require special properties of membership; we may
       
   538 generalize $x\in y$ to an arbitrary predicate~$F(x,y)$.  The theorem has a
       
   539 short manual proof.  See the directory \ttindexbold{LK/ex} for many more
       
   540 examples.
       
   541 
       
   542 We set the main goal and move the negated formula to the left.
       
   543 \begin{ttbox}
       
   544 goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
       
   545 {\out Level 0}
       
   546 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   547 {\out  1.  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   548 by (resolve_tac [notR] 1);
       
   549 {\out Level 1}
       
   550 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   551 {\out  1. EX x. ALL y. F(y,x) <-> ~ F(y,y) |-}
       
   552 by (resolve_tac [exL] 1);
       
   553 \end{ttbox}
       
   554 The right side is empty; we strip both quantifiers from the formula on the
       
   555 left.
       
   556 \begin{ttbox}
       
   557 {\out Level 2}
       
   558 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   559 {\out  1. !!x. ALL y. F(y,x) <-> ~ F(y,y) |-}
       
   560 by (resolve_tac [allL_thin] 1);
       
   561 {\out Level 3}
       
   562 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   563 {\out  1. !!x. F(?x2(x),x) <-> ~ F(?x2(x),?x2(x)) |-}
       
   564 \end{ttbox}
       
   565 The rule \ttindex{iffL} says, if $P\bimp Q$ then $P$ and~$Q$ are either
       
   566 both true or both false.  It yields two subgoals.
       
   567 \begin{ttbox}
       
   568 by (resolve_tac [iffL] 1);
       
   569 {\out Level 4}
       
   570 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   571 {\out  1. !!x.  |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
       
   572 {\out  2. !!x. ~ F(?x2(x),?x2(x)), F(?x2(x),x) |-}
       
   573 \end{ttbox}
       
   574 We must instantiate~$\Var{x@2}$, the shared unknown, to satisfy both
       
   575 subgoals.  Beginning with subgoal~2, we move a negated formula to the left
       
   576 and create a basic sequent.
       
   577 \begin{ttbox}
       
   578 by (resolve_tac [notL] 2);
       
   579 {\out Level 5}
       
   580 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   581 {\out  1. !!x.  |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
       
   582 {\out  2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))}
       
   583 by (resolve_tac [basic] 2);
       
   584 {\out Level 6}
       
   585 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   586 {\out  1. !!x.  |- F(x,x), ~ F(x,x)}
       
   587 \end{ttbox}
       
   588 Thanks to the instantiation of~$\Var{x@2}$, subgoal~1 is obviously true.
       
   589 \begin{ttbox}
       
   590 by (resolve_tac [notR] 1);
       
   591 {\out Level 7}
       
   592 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   593 {\out  1. !!x. F(x,x) |- F(x,x)}
       
   594 by (resolve_tac [basic] 1);
       
   595 {\out Level 8}
       
   596 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   597 {\out No subgoals!}
       
   598 \end{ttbox}`