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 


26 


27 
\begin{figure}


28 
\begin{center}


29 
\begin{tabular}{rrr}

111

30 
\it name &\it metatype & \it description \\

316

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


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


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


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


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

104

36 
\end{tabular}


37 
\end{center}


38 
\subcaption{Constants}


39 


40 
\begin{center}


41 
\begin{tabular}{llrrr}

316

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


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

111

44 
universal quantifier ($\forall$) \\

316

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

111

46 
existential quantifier ($\exists$) \\

316

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

111

48 
definite description ($\iota$)

104

49 
\end{tabular}


50 
\end{center}


51 
\subcaption{Binders}


52 


53 
\begin{center}

316

54 
\index{*"= symbol}


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


56 
\index{*" symbol}


57 
\index{*"""> symbol}


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

104

59 
\begin{tabular}{rrrr}

316

60 
\it symbol & \it metatype & \it priority & \it description \\


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

104

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


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


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


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


66 
\end{tabular}


67 
\end{center}


68 
\subcaption{Infixes}


69 


70 
\begin{center}


71 
\begin{tabular}{rrr}

111

72 
\it external & \it internal & \it description \\

104

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


74 
sequent $\Gamma\turn \Delta$


75 
\end{tabular}


76 
\end{center}


77 
\subcaption{Translations}


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


79 
\end{figure}


80 


81 


82 
\begin{figure}


83 
\dquotes


84 
\[\begin{array}{rcl}


85 
prop & = & sequence "  " sequence


86 
\\[2ex]


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


88 
&  & empty


89 
\\[2ex]


90 
elem & = & "\$ " id \\


91 
&  & "\$ " var \\


92 
&  & formula


93 
\\[2ex]


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

111

95 
&  & term " = " term \\


96 
&  & "\ttilde\ " formula \\


97 
&  & formula " \& " formula \\


98 
&  & formula "  " formula \\


99 
&  & formula " > " formula \\


100 
&  & formula " <> " formula \\


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


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


103 
&  & "THE~" id~ " . " formula

104

104 
\end{array}


105 
\]


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


107 
\end{figure}


108 


109 

316

110 
\section{Unification for lists}


111 
Higherorder unification includes associative unification as a special


112 
case, by an encoding that involves function composition


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


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


115 
represented by


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


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


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

104

119 

316

120 
Unlike orthodox associative unification, this technique can represent certain


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


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


123 
containing such garbage terms may accumulate during a proof.


124 
\index{flexflex constraints}

104

125 

316

126 
This technique lets Isabelle formalize sequent calculus rules,


127 
where the comma is the associative operator:


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


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


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


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


132 
more than one conjunction on the left.

104

133 

316

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


135 
sequent calculus can be formalized using an ordinary representation of


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


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

104

138 

316

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


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


141 
and linear logics.

104

142 


143 


144 
\begin{figure}


145 
\begin{ttbox}

316

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


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


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


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


150 
\subcaption{Structural rules}

104

151 

316

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


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


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


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


156 
\subcaption{Equality rules}

104

157 

316

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


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


160 


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


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

104

163 

316

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


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


166 

841

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

316

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


169 


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


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

104

172 

316

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

104

174 

316

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


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


177 


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


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


180 


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


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


183 
\subcaption{Logical rules}

104

184 
\end{ttbox}


185 

316

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

104

187 
\end{figure}


188 


189 


190 
\section{Syntax and rules of inference}

316

191 
\index{*sobj type}


192 

104

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


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


195 
of formulae.


196 

316

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


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

104

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


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

316

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


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

104

203 

316

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


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


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


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

104

208 

316

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

111

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


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


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


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


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


215 
cut) in this formulation.

104

216 


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


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


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


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


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

316

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

104

223 
specifying the formula to duplicate.


224 

333

225 
See the files {\tt LK/LK.thy} and {\tt LK/LK.ML}

104

226 
for complete listings of the rules and derived rules.


227 


228 

316

229 
\begin{figure}


230 
\begin{ttbox}


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


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


233 


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


235 


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


237 


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


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


240 


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


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


243 


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


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


246 
\end{ttbox}


247 


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


249 
\end{figure}


250 


251 

104

252 
\section{Tactics for the cut rule}


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


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


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


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


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


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


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


260 
in a righthand formula:


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


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


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


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


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


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


267 
tactic.


268 


269 
\begin{ttbox}


270 
cutR_tac : string > int > tactic


271 
cutL_tac : string > int > tactic


272 
\end{ttbox}


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


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

316

275 
\begin{ttdescription}

264

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

104

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


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


279 
that formula by~$P$.


280 

264

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

104

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

291

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

104

284 
replacing that formula by~$P$.

316

285 
\end{ttdescription}

104

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

316

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

104

288 


289 


290 
\section{Tactics for sequents}


291 
\begin{ttbox}


292 
forms_of_seq : term > term list


293 
could_res : term * term > bool


294 
could_resolve_seq : term * term > bool


295 
filseq_resolve_tac : thm list > int > int > tactic


296 
\end{ttbox}


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


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

333

299 
optimisations. The following operations implement faster rule application,

104

300 
and may have other uses.

316

301 
\begin{ttdescription}

104

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


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


304 
variables.


305 

316

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

104

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

316

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

104

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


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


311 
with some subgoal formula.


312 

316

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

291

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

316

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

291

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


317 
sides of the sequents are compatible.

104

318 


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


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


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


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


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

316

324 
\end{ttdescription}

104

325 


326 


327 


328 
\section{Packaging sequent rules}

316

329 
Section~\ref{sec:safe} described the distinction between safe and unsafe


330 
rules. An unsafe rule may reduce a provable goal to an unprovable set of


331 
subgoals, and should only be used as a last resort. Typical examples are


332 
the weakened quantifier rules {\tt allL_thin} and {\tt exR_thin}.

104

333 

316

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


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


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


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


338 
essentially a type synonym:

104

339 
\begin{ttbox}


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


341 
\end{ttbox}

316

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


343 
contents. Packs support the following operations:

104

344 
\begin{ttbox}


345 
empty_pack : pack


346 
prop_pack : pack


347 
LK_pack : pack


348 
LK_dup_pack : pack


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


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


351 
\end{ttbox}

316

352 
\begin{ttdescription}

104

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


354 


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


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

316

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

104

358 


359 
\item[\ttindexbold{LK_pack}]

316

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


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


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

104

363 
formulae are used at most once.


364 


365 
\item[\ttindexbold{LK_dup_pack}]

316

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


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

104

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


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


370 
search.


371 


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


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


374 


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


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

316

377 
\end{ttdescription}

104

378 


379 


380 
\section{Proof procedures}

316

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


382 
described in


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


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


385 
%


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


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


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


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


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


391 
openended set of rules.

104

392 


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


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


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


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


397 
\[ \begin{array}{c}


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


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


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


401 
\end{array}


402 
\]


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


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

316

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


406 
otherwise they are deterministic.

104

407 


408 


409 
\subsection{Method A}


410 
\begin{ttbox}


411 
reresolve_tac : thm list > int > tactic


412 
repeat_goal_tac : pack > int > tactic


413 
pc_tac : pack > int > tactic


414 
\end{ttbox}


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


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


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


418 
The method is inherently depthfirst.


419 


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

316

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


422 
\begin{ttdescription}

104

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


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


425 


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


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


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


429 


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


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

316

432 
\end{ttdescription}

104

433 


434 


435 
\subsection{Method B}


436 
\begin{ttbox}


437 
safe_goal_tac : pack > int > tactic


438 
step_tac : pack > int > tactic


439 
fast_tac : pack > int > tactic


440 
best_tac : pack > int > tactic


441 
\end{ttbox}


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

316

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

104

444 
can do nothing.

316

445 
\begin{ttdescription}

104

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


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


448 
It ignores the unsafe rules.


449 


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


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


452 
rule.


453 


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


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

316

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

104

457 


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


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


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

316

461 
\end{ttdescription}

104

462 


463 


464 


465 
\section{A simple example of classical reasoning}


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


467 
classical treatment of the existential quantifier. Classical reasoning


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


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

316

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


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

104

472 
\begin{ttbox}


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


474 
{\out Level 0}


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


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


477 
by (resolve_tac [exR] 1);


478 
{\out Level 1}


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


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


481 
\end{ttbox}


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


483 
in reserve, we break down the universal one.


484 
\begin{ttbox}


485 
by (resolve_tac [allR] 1);


486 
{\out Level 2}


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


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


489 
by (resolve_tac [impR] 1);


490 
{\out Level 3}


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


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


493 
\end{ttbox}


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


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


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


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


498 
\begin{ttbox}


499 
by (resolve_tac [basic] 1);


500 
{\out by: tactic failed}


501 
\end{ttbox}

316

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


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

104

504 
formula.


505 
\begin{ttbox}


506 
by (resolve_tac [exR_thin] 1);


507 
{\out Level 4}


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


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


510 
by (resolve_tac [allR] 1);


511 
{\out Level 5}


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


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


514 
by (resolve_tac [impR] 1);


515 
{\out Level 6}


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


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


518 
\end{ttbox}


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


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


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


522 
\begin{ttbox}


523 
by (resolve_tac [basic] 1);


524 
{\out Level 7}


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


526 
{\out No subgoals!}


527 
\end{ttbox}


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


529 
duplication, we employ bestfirst search:


530 
\begin{ttbox}


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


532 
{\out Level 0}


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


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


535 
by (best_tac LK_dup_pack 1);


536 
{\out Level 1}


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


538 
{\out No subgoals!}


539 
\end{ttbox}


540 


541 


542 


543 
\section{A more complex proof}


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


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


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


547 
not members of themselves:


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


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


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

291

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

104

552 
examples.


553 


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


555 
\begin{ttbox}


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


557 
{\out Level 0}


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


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


560 
by (resolve_tac [notR] 1);


561 
{\out Level 1}


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


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


564 
\end{ttbox}


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


566 
left.


567 
\begin{ttbox}

316

568 
by (resolve_tac [exL] 1);

104

569 
{\out Level 2}


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


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


572 
by (resolve_tac [allL_thin] 1);


573 
{\out Level 3}


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


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


576 
\end{ttbox}

316

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

104

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


579 
\begin{ttbox}


580 
by (resolve_tac [iffL] 1);


581 
{\out Level 4}


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


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


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


585 
\end{ttbox}


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


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


588 
and create a basic sequent.


589 
\begin{ttbox}


590 
by (resolve_tac [notL] 2);


591 
{\out Level 5}


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


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


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


595 
by (resolve_tac [basic] 2);


596 
{\out Level 6}


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


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


599 
\end{ttbox}


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


601 
\begin{ttbox}


602 
by (resolve_tac [notR] 1);


603 
{\out Level 7}


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


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


606 
by (resolve_tac [basic] 1);


607 
{\out Level 8}


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


609 
{\out No subgoals!}


610 
\end{ttbox}

316

611 


612 
\index{sequent calculus)}
