104

1 
%% $Id$

291

2 
\chapter{FirstOrder Sequent Calculus}

316

3 
\index{sequent calculus(}


4 


5 
The theory~\thydx{LK} implements classical firstorder logic through

104

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


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


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


9 
\(\Gamma\turn \Delta\), where \(\Gamma\) and \(\Delta\) are lists of


10 
formulae. Associative unification, simulated by higherorder unification,


11 
handles lists.


12 

316

13 
The logic is manysorted, using Isabelle's type classes. The class of


14 
firstorder terms is called \cldx{term}. No types of individuals are


15 
provided, but extensions can define types such as {\tt nat::term} and type


16 
constructors such as {\tt list::(term)term}. Below, the type variable


17 
$\alpha$ ranges over class {\tt term}; the equality symbol and quantifiers


18 
are polymorphic (manysorted). The type of formulae is~\tydx{o}, which


19 
belongs to class {\tt logic}.

104

20 


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


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

316

23 
logic theorem prover that is as powerful as the generic classical reasoner,

104

24 
except that it does not perform equality reasoning.


25 

5151

26 
To work in LK, start up Isabelle specifying \texttt{Sequents} as the


27 
objectlogic. Once in Isabelle, change the context to theory \texttt{LK.thy}:


28 
\begin{ttbox}


29 
isabelle Sequents


30 
context LK.thy;


31 
\end{ttbox}


32 
Model logic and linear logic are also available, but unfortunately they are


33 
not documented.


34 

104

35 


36 
\begin{figure}


37 
\begin{center}


38 
\begin{tabular}{rrr}

111

39 
\it name &\it metatype & \it description \\

316

40 
\cdx{Trueprop}& $[sobj\To sobj, sobj\To sobj]\To prop$ & coercion to $prop$\\


41 
\cdx{Seqof} & $[o,sobj]\To sobj$ & singleton sequence \\


42 
\cdx{Not} & $o\To o$ & negation ($\neg$) \\


43 
\cdx{True} & $o$ & tautology ($\top$) \\


44 
\cdx{False} & $o$ & absurdity ($\bot$)

104

45 
\end{tabular}


46 
\end{center}


47 
\subcaption{Constants}


48 


49 
\begin{center}


50 
\begin{tabular}{llrrr}

316

51 
\it symbol &\it name &\it metatype & \it priority & \it description \\


52 
\sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 &

111

53 
universal quantifier ($\forall$) \\

316

54 
\sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 &

111

55 
existential quantifier ($\exists$) \\

316

56 
\sdx{THE} & \cdx{The} & $(\alpha\To o)\To \alpha$ & 10 &

111

57 
definite description ($\iota$)

104

58 
\end{tabular}


59 
\end{center}


60 
\subcaption{Binders}


61 


62 
\begin{center}

316

63 
\index{*"= symbol}


64 
\index{&@{\tt\&} symbol}


65 
\index{*" symbol}


66 
\index{*"""> symbol}


67 
\index{*"<""> symbol}

104

68 
\begin{tabular}{rrrr}

316

69 
\it symbol & \it metatype & \it priority & \it description \\


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

104

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


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


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


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


75 
\end{tabular}


76 
\end{center}


77 
\subcaption{Infixes}


78 


79 
\begin{center}


80 
\begin{tabular}{rrr}

111

81 
\it external & \it internal & \it description \\

104

82 
\tt $\Gamma$  $\Delta$ & \tt Trueprop($\Gamma$, $\Delta$) &


83 
sequent $\Gamma\turn \Delta$


84 
\end{tabular}


85 
\end{center}


86 
\subcaption{Translations}


87 
\caption{Syntax of {\tt LK}} \label{lksyntax}


88 
\end{figure}


89 


90 


91 
\begin{figure}


92 
\dquotes


93 
\[\begin{array}{rcl}


94 
prop & = & sequence "  " sequence


95 
\\[2ex]


96 
sequence & = & elem \quad (", " elem)^* \\


97 
&  & empty


98 
\\[2ex]


99 
elem & = & "\$ " id \\


100 
&  & "\$ " var \\


101 
&  & formula


102 
\\[2ex]


103 
formula & = & \hbox{expression of type~$o$} \\

111

104 
&  & term " = " term \\


105 
&  & "\ttilde\ " formula \\


106 
&  & formula " \& " formula \\


107 
&  & formula "  " formula \\


108 
&  & formula " > " formula \\


109 
&  & formula " <> " formula \\


110 
&  & "ALL~" id~id^* " . " formula \\


111 
&  & "EX~~" id~id^* " . " formula \\


112 
&  & "THE~" id~ " . " formula

104

113 
\end{array}


114 
\]


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


116 
\end{figure}


117 


118 

316

119 
\section{Unification for lists}


120 
Higherorder unification includes associative unification as a special


121 
case, by an encoding that involves function composition


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

5151

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

316

124 
represented by

5151

125 
\[ \lambda x. C(t@1,C(t@2,\ldots,C(t@n,x))). \]

316

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


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

104

128 

316

129 
Unlike orthodox associative unification, this technique can represent certain


130 
infinite sets of unifiers by flexflex equations. But note that the term

5151

131 
$\lambda x. C(t,\Var{a})$ does not represent any list. Flexflex constraints

316

132 
containing such garbage terms may accumulate during a proof.


133 
\index{flexflex constraints}

104

134 

316

135 
This technique lets Isabelle formalize sequent calculus rules,


136 
where the comma is the associative operator:


137 
\[ \infer[(\conj\hbox{left})]


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


139 
{\Gamma,P,Q,\Delta \turn \Theta} \]


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


141 
more than one conjunction on the left.

104

142 

316

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


144 
sequent calculus can be formalized using an ordinary representation of


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


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

104

147 

316

148 
Explicit formalization of sequents can be tiresome. But it gives precise


149 
control over contraction and weakening, and is essential to handle relevant


150 
and linear logics.

104

151 


152 


153 
\begin{figure}


154 
\begin{ttbox}

316

155 
\tdx{basic} $H, P, $G  $E, P, $F


156 
\tdx{thinR} $H  $E, $F ==> $H  $E, P, $F


157 
\tdx{thinL} $H, $G  $E ==> $H, P, $G  $E


158 
\tdx{cut} [ $H  $E, P; $H, P  $E ] ==> $H  $E


159 
\subcaption{Structural rules}

104

160 

316

161 
\tdx{refl} $H  $E, a=a, $F


162 
\tdx{sym} $H  $E, a=b, $F ==> $H  $E, b=a, $F


163 
\tdx{trans} [ $H $E, a=b, $F; $H $E, b=c, $F ] ==>


164 
$H $E, a=c, $F


165 
\subcaption{Equality rules}

104

166 

316

167 
\tdx{True_def} True == False>False


168 
\tdx{iff_def} P<>Q == (P>Q) & (Q>P)


169 


170 
\tdx{conjR} [ $H $E, P, $F; $H $E, Q, $F ] ==> $H $E, P&Q, $F


171 
\tdx{conjL} $H, P, Q, $G  $E ==> $H, P & Q, $G  $E

104

172 

316

173 
\tdx{disjR} $H  $E, P, Q, $F ==> $H  $E, PQ, $F


174 
\tdx{disjL} [ $H, P, $G  $E; $H, Q, $G  $E ] ==> $H, PQ, $G  $E


175 

841

176 
\tdx{impR} $H, P  $E, Q, $F ==> $H  $E, P>Q, $F

316

177 
\tdx{impL} [ $H,$G  $E,P; $H, Q, $G  $E ] ==> $H, P>Q, $G  $E


178 


179 
\tdx{notR} $H, P  $E, $F ==> $H  $E, ~P, $F


180 
\tdx{notL} $H, $G  $E, P ==> $H, ~P, $G  $E

104

181 

316

182 
\tdx{FalseL} $H, False, $G  $E

104

183 

5151

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


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

316

186 

5151

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


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

316

189 

5151

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


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

316

192 
\subcaption{Logical rules}

104

193 
\end{ttbox}


194 

316

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

104

196 
\end{figure}


197 


198 


199 
\section{Syntax and rules of inference}

316

200 
\index{*sobj type}


201 

104

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


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


204 
of formulae.


205 

5151

206 
The {\bf definite description} operator~$\iota x. P[x]$ stands for some~$a$

316

207 
satisfying~$P[a]$, if one exists and is unique. Since all terms in \LK{}

104

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


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

5151

210 
\hbox{\tt THE $x$. $P[x]$}. The corresponding rule (Fig.\ts\ref{lkrules})

316

211 
does not entail the Axiom of Choice because it requires uniqueness.

104

212 

316

213 
Figure~\ref{lkgrammar} presents the grammar of \LK. Traditionally,


214 
\(\Gamma\) and \(\Delta\) are metavariables for sequences. In Isabelle's


215 
notation, the prefix~\verb$ on a variable makes it range over sequences.


216 
In a sequent, anything not prefixed by \verb$ is taken as a formula.

104

217 

316

218 
Figure~\ref{lkrules} presents the rules of theory \thydx{LK}. The

111

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


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


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


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


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


224 
cut) in this formulation.

104

225 


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


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


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


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


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

316

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

104

232 
specifying the formula to duplicate.


233 

3148

234 
See theory {\tt Sequents/LK} in the sources for complete listings of


235 
the rules and derived rules.

104

236 


237 

316

238 
\begin{figure}


239 
\begin{ttbox}


240 
\tdx{conR} $H  $E, P, $F, P ==> $H  $E, P, $F


241 
\tdx{conL} $H, P, $G, P  $E ==> $H, P, $G  $E


242 


243 
\tdx{symL} $H, $G, B = A  $E ==> $H, A = B, $G  $E


244 


245 
\tdx{TrueR} $H  $E, True, $F


246 


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


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


249 


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


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


252 

5151

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


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

316

255 
\end{ttbox}


256 


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


258 
\end{figure}


259 


260 

104

261 
\section{Tactics for the cut rule}


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


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


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


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


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


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


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


269 
in a righthand formula:


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


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


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


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


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


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


276 
tactic.


277 


278 
\begin{ttbox}


279 
cutR_tac : string > int > tactic


280 
cutL_tac : string > int > tactic


281 
\end{ttbox}


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


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

316

284 
\begin{ttdescription}

264

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

104

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


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


288 
that formula by~$P$.


289 

264

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

104

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

291

292 
then deletes some formula from the left side of the new subgoal $i+1$,

104

293 
replacing that formula by~$P$.

316

294 
\end{ttdescription}

104

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

316

296 
applied to particular formulae using {\tt res_inst_tac}.

104

297 


298 


299 
\section{Tactics for sequents}


300 
\begin{ttbox}


301 
forms_of_seq : term > term list


302 
could_res : term * term > bool


303 
could_resolve_seq : term * term > bool


304 
filseq_resolve_tac : thm list > int > int > tactic


305 
\end{ttbox}


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


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

333

308 
optimisations. The following operations implement faster rule application,

104

309 
and may have other uses.

316

310 
\begin{ttdescription}

104

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


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


313 
variables.


314 

316

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

104

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

316

317 
premise or subgoal, while $u$ is from the conclusion of an objectrule.

104

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


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


320 
with some subgoal formula.


321 

316

322 
\item[\ttindexbold{could_resolve_seq} ($t$,$u$)]

291

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

316

324 
or subgoal, while $u$ is the conclusion of an objectrule. It simply

291

325 
calls {\tt could_res} twice to check that both the left and the right


326 
sides of the sequents are compatible.

104

327 


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


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


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


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


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

316

333 
\end{ttdescription}

104

334 


335 

6072

336 
\section{Packaging sequent rules}

104

337 

6072

338 
The sequent calculi come with simple proof procedures. These are incomplete


339 
but are reasonably powerful for interactive use. They expect rules to be


340 
classified as {\bf safe} or {\bf unsafe}. A rule is safe if applying it to a


341 
provable goal always yields provable subgoals. If a rule is safe then it can


342 
be applied automatically to a goal without destroying our chances of finding a


343 
proof. For instance, all the standard rules of the classical sequent calculus


344 
{\sc lk} are safe. An unsafe rule may render the goal unprovable; typical


345 
examples are the weakened quantifier rules {\tt allL_thin} and {\tt exR_thin}.


346 


347 
Proof procedures use safe rules whenever possible, using an unsafe rule as a


348 
last resort. Those safe rules are preferred that generate the fewest


349 
subgoals. Safe rules are (by definition) deterministic, while the unsafe


350 
rules require a search strategy, such as backtracking.

104

351 

316

352 
A {\bf pack} is a pair whose first component is a list of safe rules and


353 
whose second is a list of unsafe rules. Packs can be extended in an


354 
obvious way to allow reasoning with various collections of rules. For


355 
clarity, \LK{} declares \mltydx{pack} as an \ML{} datatype, although is


356 
essentially a type synonym:

104

357 
\begin{ttbox}


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


359 
\end{ttbox}

316

360 
Patternmatching using constructor {\tt Pack} can inspect a pack's


361 
contents. Packs support the following operations:

104

362 
\begin{ttbox}


363 
empty_pack : pack


364 
prop_pack : pack


365 
LK_pack : pack


366 
LK_dup_pack : pack


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


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


369 
\end{ttbox}

316

370 
\begin{ttdescription}

104

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


372 


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


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

316

375 
rules {\tt basic} and {\tt refl}. These are all safe.

104

376 


377 
\item[\ttindexbold{LK_pack}]

316

378 
extends {\tt prop_pack} with the safe rules {\tt allR}


379 
and~{\tt exL} and the unsafe rules {\tt allL_thin} and


380 
{\tt exR_thin}. Search using this is incomplete since quantified

104

381 
formulae are used at most once.


382 


383 
\item[\ttindexbold{LK_dup_pack}]

316

384 
extends {\tt prop_pack} with the safe rules {\tt allR}


385 
and~{\tt exL} and the unsafe rules \tdx{allL} and~\tdx{exR}.

104

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


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


388 
search.


389 


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


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


392 


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


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

316

395 
\end{ttdescription}

104

396 


397 


398 
\section{Proof procedures}

6072

399 

316

400 
The \LK{} proof procedure is similar to the classical reasoner


401 
described in


402 
\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%


403 
{Chap.\ts\ref{chap:classical}}.


404 
%


405 
In fact it is simpler, since it works directly with sequents rather than


406 
simulating them. There is no need to distinguish introduction rules from


407 
elimination rules, and of course there is no swap rule. As always,


408 
Isabelle's classical proof procedures are less powerful than resolution


409 
theorem provers. But they are more natural and flexible, working with an


410 
openended set of rules.

104

411 


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


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


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


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


416 
\[ \begin{array}{c}


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


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


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


420 
\end{array}


421 
\]


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


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

316

424 
backtracking only over axioms, such as {\tt basic} and {\tt refl};


425 
otherwise they are deterministic.

104

426 


427 


428 
\subsection{Method A}


429 
\begin{ttbox}


430 
reresolve_tac : thm list > int > tactic


431 
repeat_goal_tac : pack > int > tactic


432 
pc_tac : pack > int > tactic


433 
\end{ttbox}


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


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


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


437 
The method is inherently depthfirst.


438 


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

316

440 
premises. They fail  return no next state  if they can do nothing.


441 
\begin{ttdescription}

104

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


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


444 


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


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


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


448 


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


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

316

451 
\end{ttdescription}

104

452 


453 


454 
\subsection{Method B}


455 
\begin{ttbox}


456 
safe_goal_tac : pack > int > tactic


457 
step_tac : pack > int > tactic


458 
fast_tac : pack > int > tactic


459 
best_tac : pack > int > tactic


460 
\end{ttbox}


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

316

462 
reasoner. They use `Method~A' only on safe rules. They fail if they

104

463 
can do nothing.

316

464 
\begin{ttdescription}

104

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


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


467 
It ignores the unsafe rules.


468 


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


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


471 
rule.


472 


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


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

316

475 
Despite its name, it is frequently slower than {\tt pc_tac}.

104

476 


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


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


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

316

480 
\end{ttdescription}

104

481 


482 


483 


484 
\section{A simple example of classical reasoning}


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


486 
classical treatment of the existential quantifier. Classical reasoning


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

6072

488 
given in the FOL manual~\cite{isabelleZF}. From a logical point of view, the

316

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


490 
rather than the weaker~\tdx{exR_thin}.

104

491 
\begin{ttbox}

5151

492 
Goal " EX y. ALL x. P(y)>P(x)";

104

493 
{\out Level 0}


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


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


496 
by (resolve_tac [exR] 1);


497 
{\out Level 1}


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


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


500 
\end{ttbox}


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


502 
in reserve, we break down the universal one.


503 
\begin{ttbox}


504 
by (resolve_tac [allR] 1);


505 
{\out Level 2}


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


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


508 
by (resolve_tac [impR] 1);


509 
{\out Level 3}


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


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


512 
\end{ttbox}


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


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


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


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


517 
\begin{ttbox}


518 
by (resolve_tac [basic] 1);


519 
{\out by: tactic failed}


520 
\end{ttbox}

316

521 
We reuse the existential formula using~\tdx{exR_thin}, which discards


522 
it; we shall not need it a third time. We again break down the resulting

104

523 
formula.


524 
\begin{ttbox}


525 
by (resolve_tac [exR_thin] 1);


526 
{\out Level 4}


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


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


529 
by (resolve_tac [allR] 1);


530 
{\out Level 5}


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


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


533 
by (resolve_tac [impR] 1);


534 
{\out Level 6}


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


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


537 
\end{ttbox}


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

5151

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

104

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


541 
\begin{ttbox}


542 
by (resolve_tac [basic] 1);


543 
{\out Level 7}


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


545 
{\out No subgoals!}


546 
\end{ttbox}


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


548 
duplication, we employ bestfirst search:


549 
\begin{ttbox}

5151

550 
Goal " EX y. ALL x. P(y)>P(x)";

104

551 
{\out Level 0}


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


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


554 
by (best_tac LK_dup_pack 1);


555 
{\out Level 1}


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


557 
{\out No subgoals!}


558 
\end{ttbox}


559 


560 


561 


562 
\section{A more complex proof}


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


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


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


566 
not members of themselves:


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


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


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

291

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

104

571 
examples.


572 


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


574 
\begin{ttbox}

5151

575 
Goal " ~ (EX x. ALL y. F(y,x) <> ~F(y,y))";

104

576 
{\out Level 0}


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


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


579 
by (resolve_tac [notR] 1);


580 
{\out Level 1}


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


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


583 
\end{ttbox}


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


585 
left.


586 
\begin{ttbox}

316

587 
by (resolve_tac [exL] 1);

104

588 
{\out Level 2}


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


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


591 
by (resolve_tac [allL_thin] 1);


592 
{\out Level 3}


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


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


595 
\end{ttbox}

316

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

104

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


598 
\begin{ttbox}


599 
by (resolve_tac [iffL] 1);


600 
{\out Level 4}


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


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


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


604 
\end{ttbox}


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


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


607 
and create a basic sequent.


608 
\begin{ttbox}


609 
by (resolve_tac [notL] 2);


610 
{\out Level 5}


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


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


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


614 
by (resolve_tac [basic] 2);


615 
{\out Level 6}


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


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


618 
\end{ttbox}


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


620 
\begin{ttbox}


621 
by (resolve_tac [notR] 1);


622 
{\out Level 7}


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


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


625 
by (resolve_tac [basic] 1);


626 
{\out Level 8}


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


628 
{\out No subgoals!}


629 
\end{ttbox}

316

630 


631 
\index{sequent calculus)}
