104

1 
%% $Id$


2 
\chapter{Firstorder sequent calculus}


3 
The directory~\ttindexbold{LK} implements classical firstorder 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 higherorder unification,


9 
handles lists.


10 


11 
The logic is manysorted, using Isabelle's type classes. The


12 
class of firstorder 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 (manysorted). 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 
Higherorder 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 flexflex equations. But note that the term


37 
$\lambda x.C(t,\Var{a})$ does not represent any list. Flexflex 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}]

111

43 
{\Gamma,P\conj Q,\Delta \turn \Theta}

104

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}

111

59 
\it name &\it metatype & \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$)

104

65 
\end{tabular}


66 
\end{center}


67 
\subcaption{Constants}


68 


69 
\begin{center}


70 
\begin{tabular}{llrrr}

111

71 
\it symbol &\it name &\it metatype & \it precedence & \it description \\

104

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

111

73 
universal quantifier ($\forall$) \\

104

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

111

75 
existential quantifier ($\exists$) \\

104

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

111

77 
definite description ($\iota$)

104

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 metatype & \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}

111

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

104

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{lksyntax}


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$} \\

111

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

104

133 
\end{array}


134 
\]


135 
\caption{Grammar of {\tt LK}} \label{lkgrammar}


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, PQ, $F


160 
\idx{disjL} [ $H, P, $G  $E; $H, Q, $G  $E ] ==> $H, PQ, $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

111

169 
\end{ttbox}

104

170 
\subcaption{Propositional rules}

111

171 
\caption{Rules of {\tt LK}} \label{lkrules}


172 
\end{figure}

104

173 

111

174 
\begin{figure}


175 
\begin{ttbox}

104

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


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


178 


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


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


181 


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


183 
$H  $E, P(THE x.P(x)), $F

111

184 
\end{ttbox}

104

185 
\subcaption{Quantifier rules}


186 

111

187 
\caption{Rules of {\tt LK} (continued)} \label{lkrules2}

104

188 
\end{figure}


189 


190 


191 
\begin{figure}


192 
\begin{ttbox}


193 
\idx{conR} $H  $E, P, $F, P ==> $H  $E, P, $F


194 
\idx{conL} $H, P, $G, P  $E ==> $H, P, $G  $E


195 


196 
\idx{symL} $H, $G, B = A  $E ==> $H, A = B, $G  $E


197 


198 
\idx{TrueR} $H  $E, True, $F


199 


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


201 
$H  $E, P<>Q, $F


202 


203 
\idx{iffL} [ $H, $G  $E, P, Q; $H, Q, P, $G  $E ] ==>


204 
$H, P<>Q, $G  $E


205 


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


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


208 
\end{ttbox}


209 


210 
\caption{Derived rules for {\tt LK}} \label{lkderived}


211 
\end{figure}


212 


213 


214 
\section{Syntax and rules of inference}


215 
Figure~\ref{lksyntax} gives the syntax for {\tt LK}, which is complicated


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


217 
of formulae.


218 


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


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


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


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


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


224 


225 
Traditionally, \(\Gamma\) and \(\Delta\) are metavariables for sequences.


226 
In Isabelle's notation, the prefix~\verb$ on a variable makes it range


227 
over sequences. In a sequent, anything not prefixed by \verb$ is taken


228 
as a formula.


229 


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

111

231 
Figures~\ref{lkrules} and~\ref{lkrules2} present the rules. The


232 
connective $\bimp$ is defined using $\conj$ and $\imp$. The axiom for


233 
basic sequents is expressed in a form that provides automatic thinning:


234 
redundant formulae are simply ignored. The other rules are expressed in


235 
the form most suitable for backward proof  they do not require exchange


236 
or contraction rules. The contraction rules are actually derivable (via


237 
cut) in this formulation.

104

238 


239 
Figure~\ref{lkderived} presents derived rules, including rules for


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


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


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


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


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


245 
specifying the formula to duplicate.


246 


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


248 
for complete listings of the rules and derived rules.


249 


250 


251 
\section{Tactics for the cut rule}


252 
According to the cutelimination theorem, the cut rule can be eliminated


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


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


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


256 
derivations of rules. For example, there is a trivial cutfree proof of


257 
the sequent \(P\conj Q\turn Q\conj P\).


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


259 
in a righthand formula:


260 
\[ \Gamma\turn \Delta, P\conj Q\over \Gamma\turn \Delta, Q\conj P \]


261 
The cut rule must be used, for $P\conj Q$ is not a subformula of $Q\conj


262 
P$. Most cuts directly involve a premise of the rule being derived (a


263 
metaassumption). In a few cases, the cut formula is not part of any


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


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


266 
tactic.


267 


268 
\begin{ttbox}


269 
cutR_tac : string > int > tactic


270 
cutL_tac : string > int > tactic


271 
\end{ttbox}


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


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


274 
\begin{description}

264

275 
\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}]

104

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


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


278 
that formula by~$P$.


279 

264

280 
\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}]

104

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


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


283 
replacing that formula by~$P$.


284 
\end{description}


285 
All the structural rules  cut, contraction, and thinning  can be


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


287 


288 


289 
\section{Tactics for sequents}


290 
\begin{ttbox}


291 
forms_of_seq : term > term list


292 
could_res : term * term > bool


293 
could_resolve_seq : term * term > bool


294 
filseq_resolve_tac : thm list > int > int > tactic


295 
\end{ttbox}


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


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


298 
optimizations. The following operations implement faster rule application,


299 
and may have other uses.


300 
\begin{description}


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


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


303 
variables.


304 


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


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


307 
premise (subgoal), while $u$ is from the conclusion of an objectrule.


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


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


310 
with some subgoal formula.


311 


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


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


314 
(subgoal), while $u$ is the conclusion of an objectrule. It uses {\tt


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


316 


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


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


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


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


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


322 
\end{description}


323 


324 


325 


326 
\section{Packaging sequent rules}


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


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


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


330 
as a last resort.


331 


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


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


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


335 
For clarity, \LK{} declares the datatype


336 
\ttindexbold{pack}:


337 
\begin{ttbox}


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


339 
\end{ttbox}


340 
The contents of any pack can be inspected by patternmatching. Packs


341 
support the following operations:


342 
\begin{ttbox}


343 
empty_pack : pack


344 
prop_pack : pack


345 
LK_pack : pack


346 
LK_dup_pack : pack


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


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


349 
\end{ttbox}


350 
\begin{description}


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


352 


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


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


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


356 


357 
\item[\ttindexbold{LK_pack}]


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


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


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


361 
formulae are used at most once.


362 


363 
\item[\ttindexbold{LK_dup_pack}]


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


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


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


367 
frequently fails to terminate. It is generally unsuitable for depthfirst


368 
search.


369 


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


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


372 


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


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


375 
\end{description}


376 


377 


378 
\section{Proof procedures}


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


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


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


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


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


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


385 
natural and flexible, working with an openended set of rules.


386 


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


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


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


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


391 
\[ \begin{array}{c}


392 
P(0), P(1), P(2) \turn P(\Var{a}) \\


393 
P(0), P(2), P(3) \turn P(\Var{a}) \\


394 
P(1), P(3), P(2) \turn P(\Var{a})


395 
\end{array}


396 
\]


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


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


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


400 


401 


402 
\subsection{Method A}


403 
\begin{ttbox}


404 
reresolve_tac : thm list > int > tactic


405 
repeat_goal_tac : pack > int > tactic


406 
pc_tac : pack > int > tactic


407 
\end{ttbox}


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


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


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


411 
The method is inherently depthfirst.


412 


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


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


415 
\begin{description}


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


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


418 


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


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


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


422 


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


424 
applies {\tt repeat_goal_tac} using depthfirst search to solve subgoal~$i$.


425 
\end{description}


426 


427 


428 
\subsection{Method B}


429 
\begin{ttbox}


430 
safe_goal_tac : pack > int > tactic


431 
step_tac : pack > int > tactic


432 
fast_tac : pack > int > tactic


433 
best_tac : pack > int > tactic


434 
\end{ttbox}


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


436 
module. They use `Method~A' only on safe rules. They {\bf fail} if they


437 
can do nothing.


438 
\begin{description}


439 
\item[\ttindexbold{safe_goal_tac} $pack$ $i$]


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


441 
It ignores the unsafe rules.


442 


443 
\item[\ttindexbold{step_tac} $pack$ $i$]


444 
either applies safe rules (using {\tt safe_goal_tac}) or applies one unsafe


445 
rule.


446 


447 
\item[\ttindexbold{fast_tac} $pack$ $i$]


448 
applies {\tt step_tac} using depthfirst search to solve subgoal~$i$.


449 
Despite the names, {\tt pc_tac} is frequently faster.


450 


451 
\item[\ttindexbold{best_tac} $pack$ $i$]


452 
applies {\tt step_tac} using bestfirst search to solve subgoal~$i$. It is


453 
particularly useful for quantifier duplication (using \ttindex{LK_dup_pack}).


454 
\end{description}


455 


456 


457 


458 
\section{A simple example of classical reasoning}


459 
The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the


460 
classical treatment of the existential quantifier. Classical reasoning


461 
is easy using~{\LK}, as you can see by comparing this proof with the one


462 
given in~\S\ref{folclaexample}. From a logical point of view, the


463 
proofs are essentially the same; the key step here is to use \ttindex{exR}


464 
rather than the weaker~\ttindex{exR_thin}.


465 
\begin{ttbox}


466 
goal LK.thy " EX y. ALL x. P(y)>P(x)";


467 
{\out Level 0}


468 
{\out  EX y. ALL x. P(y) > P(x)}


469 
{\out 1.  EX y. ALL x. P(y) > P(x)}


470 
by (resolve_tac [exR] 1);


471 
{\out Level 1}


472 
{\out  EX y. ALL x. P(y) > P(x)}


473 
{\out 1.  ALL x. P(?x) > P(x), EX x. ALL xa. P(x) > P(xa)}


474 
\end{ttbox}


475 
There are now two formulae on the right side. Keeping the existential one


476 
in reserve, we break down the universal one.


477 
\begin{ttbox}


478 
by (resolve_tac [allR] 1);


479 
{\out Level 2}


480 
{\out  EX y. ALL x. P(y) > P(x)}


481 
{\out 1. !!x.  P(?x) > P(x), EX x. ALL xa. P(x) > P(xa)}


482 
by (resolve_tac [impR] 1);


483 
{\out Level 3}


484 
{\out  EX y. ALL x. P(y) > P(x)}


485 
{\out 1. !!x. P(?x)  P(x), EX x. ALL xa. P(x) > P(xa)}


486 
\end{ttbox}


487 
Because {\LK} is a sequent calculus, the formula~$P(\Var{x})$ does not


488 
become an assumption; instead, it moves to the left side. The


489 
resulting subgoal cannot be instantiated to a basic sequent: the bound


490 
variable~$x$ is not unifiable with the unknown~$\Var{x}$.


491 
\begin{ttbox}


492 
by (resolve_tac [basic] 1);


493 
{\out by: tactic failed}


494 
\end{ttbox}


495 
We reuse the existential formula using~\ttindex{exR_thin}, which discards


496 
it; we will not need it a third time. We again break down the resulting


497 
formula.


498 
\begin{ttbox}


499 
by (resolve_tac [exR_thin] 1);


500 
{\out Level 4}


501 
{\out  EX y. ALL x. P(y) > P(x)}


502 
{\out 1. !!x. P(?x)  P(x), ALL xa. P(?x7(x)) > P(xa)}


503 
by (resolve_tac [allR] 1);


504 
{\out Level 5}


505 
{\out  EX y. ALL x. P(y) > P(x)}


506 
{\out 1. !!x xa. P(?x)  P(x), P(?x7(x)) > P(xa)}


507 
by (resolve_tac [impR] 1);


508 
{\out Level 6}


509 
{\out  EX y. ALL x. P(y) > P(x)}


510 
{\out 1. !!x xa. P(?x), P(?x7(x))  P(x), P(xa)}


511 
\end{ttbox}


512 
Subgoal~1 seems to offer lots of possibilities. Actually the only useful


513 
step is instantiating~$\Var{x@7}$ to $\lambda x.x$,


514 
transforming~$\Var{x@7}(x)$ into~$x$.


515 
\begin{ttbox}


516 
by (resolve_tac [basic] 1);


517 
{\out Level 7}


518 
{\out  EX y. ALL x. P(y) > P(x)}


519 
{\out No subgoals!}


520 
\end{ttbox}


521 
This theorem can be proved automatically. Because it involves quantifier


522 
duplication, we employ bestfirst search:


523 
\begin{ttbox}


524 
goal LK.thy " EX y. ALL x. P(y)>P(x)";


525 
{\out Level 0}


526 
{\out  EX y. ALL x. P(y) > P(x)}


527 
{\out 1.  EX y. ALL x. P(y) > P(x)}


528 
by (best_tac LK_dup_pack 1);


529 
{\out Level 1}


530 
{\out  EX y. ALL x. P(y) > P(x)}


531 
{\out No subgoals!}


532 
\end{ttbox}


533 


534 


535 


536 
\section{A more complex proof}


537 
Many of Pelletier's test problems for theorem provers \cite{pelletier86}


538 
can be solved automatically. Problem~39 concerns set theory, asserting


539 
that there is no Russell set  a set consisting of those sets that are


540 
not members of themselves:


541 
\[ \turn \neg (\exists x. \forall y. y\in x \bimp y\not\in y) \]


542 
This does not require special properties of membership; we may


543 
generalize $x\in y$ to an arbitrary predicate~$F(x,y)$. The theorem has a


544 
short manual proof. See the directory \ttindexbold{LK/ex} for many more


545 
examples.


546 


547 
We set the main goal and move the negated formula to the left.


548 
\begin{ttbox}


549 
goal LK.thy " ~ (EX x. ALL y. F(y,x) <> ~F(y,y))";


550 
{\out Level 0}


551 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


552 
{\out 1.  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


553 
by (resolve_tac [notR] 1);


554 
{\out Level 1}


555 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


556 
{\out 1. EX x. ALL y. F(y,x) <> ~ F(y,y) }


557 
by (resolve_tac [exL] 1);


558 
\end{ttbox}


559 
The right side is empty; we strip both quantifiers from the formula on the


560 
left.


561 
\begin{ttbox}


562 
{\out Level 2}


563 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


564 
{\out 1. !!x. ALL y. F(y,x) <> ~ F(y,y) }


565 
by (resolve_tac [allL_thin] 1);


566 
{\out Level 3}


567 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


568 
{\out 1. !!x. F(?x2(x),x) <> ~ F(?x2(x),?x2(x)) }


569 
\end{ttbox}


570 
The rule \ttindex{iffL} says, if $P\bimp Q$ then $P$ and~$Q$ are either


571 
both true or both false. It yields two subgoals.


572 
\begin{ttbox}


573 
by (resolve_tac [iffL] 1);


574 
{\out Level 4}


575 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


576 
{\out 1. !!x.  F(?x2(x),x), ~ F(?x2(x),?x2(x))}


577 
{\out 2. !!x. ~ F(?x2(x),?x2(x)), F(?x2(x),x) }


578 
\end{ttbox}


579 
We must instantiate~$\Var{x@2}$, the shared unknown, to satisfy both


580 
subgoals. Beginning with subgoal~2, we move a negated formula to the left


581 
and create a basic sequent.


582 
\begin{ttbox}


583 
by (resolve_tac [notL] 2);


584 
{\out Level 5}


585 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


586 
{\out 1. !!x.  F(?x2(x),x), ~ F(?x2(x),?x2(x))}


587 
{\out 2. !!x. F(?x2(x),x)  F(?x2(x),?x2(x))}


588 
by (resolve_tac [basic] 2);


589 
{\out Level 6}


590 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


591 
{\out 1. !!x.  F(x,x), ~ F(x,x)}


592 
\end{ttbox}


593 
Thanks to the instantiation of~$\Var{x@2}$, subgoal~1 is obviously true.


594 
\begin{ttbox}


595 
by (resolve_tac [notR] 1);


596 
{\out Level 7}


597 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


598 
{\out 1. !!x. F(x,x)  F(x,x)}


599 
by (resolve_tac [basic] 1);


600 
{\out Level 8}


601 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


602 
{\out No subgoals!}


603 
\end{ttbox}
