diff -r a8b655d089ac -r c40adab7568e doc-src/Ref/classical.tex --- a/doc-src/Ref/classical.tex Sat Jun 04 19:39:45 2011 +0200 +++ b/doc-src/Ref/classical.tex Sat Jun 04 22:09:42 2011 +0200 @@ -3,186 +3,6 @@ \index{classical reasoner|(} \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}} -Although Isabelle is generic, many users will be working in some extension of -classical first-order logic. Isabelle's set theory~ZF is built upon -theory~FOL, while HOL conceptually contains first-order logic as a fragment. -Theorem-proving in predicate logic is undecidable, but many researchers have -developed strategies to assist in this task. - -Isabelle's classical reasoner is an \ML{} functor that accepts certain -information about a logic and delivers a suite of automatic tactics. Each -tactic takes a collection of rules and executes a simple, non-clausal proof -procedure. They are slow and simplistic compared with resolution theorem -provers, but they can save considerable time and effort. They can prove -theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in -seconds: -\[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x)) - \imp \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x)) \] -\[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x)) - \imp \neg (\exists z. \forall x. F(x,z)) -\] -% -The tactics are generic. They are not restricted to first-order logic, and -have been heavily used in the development of Isabelle's set theory. Few -interactive proof assistants provide this much automation. The tactics can -be traced, and their components can be called directly; in this manner, -any proof can be viewed interactively. - -We shall first discuss the underlying principles, then present the classical -reasoner. Finally, we shall see how to instantiate it for new logics. The -logics FOL, ZF, HOL and HOLCF have it already installed. - - -\section{The sequent calculus} -\index{sequent calculus} -Isabelle supports natural deduction, which is easy to use for interactive -proof. But natural deduction does not easily lend itself to automation, -and has a bias towards intuitionism. For certain proofs in classical -logic, it can not be called natural. The {\bf sequent calculus}, a -generalization of natural deduction, is easier to automate. - -A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$ -and~$\Delta$ are sets of formulae.% -\footnote{For first-order logic, sequents can equivalently be made from - lists or multisets of formulae.} The sequent -\[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \] -is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj -Q@n$. Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true, -while $Q@1,\ldots,Q@n$ represent alternative goals. A sequent is {\bf -basic} if its left and right sides have a common formula, as in $P,Q\turn -Q,R$; basic sequents are trivially valid. - -Sequent rules are classified as {\bf right} or {\bf left}, indicating which -side of the $\turn$~symbol they operate on. Rules that operate on the -right side are analogous to natural deduction's introduction rules, and -left rules are analogous to elimination rules. -Recall the natural deduction rules for - first-order logic, -\iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}% - {Fig.\ts\ref{fol-fig}}. -The sequent calculus analogue of~$({\imp}I)$ is the rule -$$ -\ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q} -\eqno({\imp}R) -$$ -This breaks down some implication on the right side of a sequent; $\Gamma$ -and $\Delta$ stand for the sets of formulae that are unaffected by the -inference. The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the -single rule -$$ -\ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q} -\eqno({\disj}R) -$$ -This breaks down some disjunction on the right side, replacing it by both -disjuncts. Thus, the sequent calculus is a kind of multiple-conclusion logic. - -To illustrate the use of multiple formulae on the right, let us prove -the classical theorem $(P\imp Q)\disj(Q\imp P)$. Working backwards, we -reduce this formula to a basic sequent: -\[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)} - {\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;} - {\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad} - {P, Q \turn Q, P\qquad\qquad}}} -\] -This example is typical of the sequent calculus: start with the desired -theorem and apply rules backwards in a fairly arbitrary manner. This yields a -surprisingly effective proof procedure. Quantifiers add few complications, -since Isabelle handles parameters and schematic variables. See Chapter~10 -of {\em ML for the Working Programmer}~\cite{paulson-ml2} for further -discussion. - - -\section{Simulating sequents by natural deduction} -Isabelle can represent sequents directly, as in the object-logic~\texttt{LK}\@. -But natural deduction is easier to work with, and most object-logics employ -it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn -Q@1,\ldots,Q@n$ by the Isabelle formula -\[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \] -where the order of the assumptions and the choice of~$Q@1$ are arbitrary. -Elim-resolution plays a key role in simulating sequent proofs. - -We can easily handle reasoning on the left. -As discussed in -\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{{\S}\ref{destruct}}, -elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$ -achieves a similar effect as the corresponding sequent rules. For the -other connectives, we use sequent-style elimination rules instead of -destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that -the rule $(\neg L)$ has no effect under our representation of sequents! -$$ -\ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}\eqno({\neg}L) -$$ -What about reasoning on the right? Introduction rules can only affect the -formula in the conclusion, namely~$Q@1$. The other right-side formulae are -represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$. -\index{assumptions!negated} -In order to operate on one of these, it must first be exchanged with~$Q@1$. -Elim-resolution with the {\bf swap} rule has this effect: -$$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap) $$ -To ensure that swaps occur only when necessary, each introduction rule is -converted into a swapped form: it is resolved with the second premise -of~$(swap)$. The swapped form of~$({\conj}I)$, which might be -called~$({\neg\conj}E)$, is -\[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \] -Similarly, the swapped form of~$({\imp}I)$ is -\[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R \] -Swapped introduction rules are applied using elim-resolution, which deletes -the negated formula. Our representation of sequents also requires the use -of ordinary introduction rules. If we had no regard for readability, we -could treat the right side more uniformly by representing sequents as -\[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \] - - -\section{Extra rules for the sequent calculus} -As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$ -must be replaced by sequent-style elimination rules. In addition, we need -rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj -Q$. The introduction rules~$({\disj}I1,2)$ are replaced by a rule that -simulates $({\disj}R)$: -\[ (\neg Q\Imp P) \Imp P\disj Q \] -The destruction rule $({\imp}E)$ is replaced by -\[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \] -Quantifier replication also requires special rules. In classical logic, -$\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules -$(\exists R)$ and $(\forall L)$ are dual: -\[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P} - {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R) - \qquad - \ainfer{\forall x{.}P, \Gamma &\turn \Delta} - {P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L) -\] -Thus both kinds of quantifier may be replicated. Theorems requiring -multiple uses of a universal formula are easy to invent; consider -\[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \] -for any~$n>1$. Natural examples of the multiple use of an existential -formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$. - -Forgoing quantifier replication loses completeness, but gains decidability, -since the search space becomes finite. Many useful theorems can be proved -without replication, and the search generally delivers its verdict in a -reasonable time. To adopt this approach, represent the sequent rules -$(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists -E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination -form: -$$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q \eqno(\forall E@2) $$ -Elim-resolution with this rule will delete the universal formula after a -single use. To replicate universal quantifiers, replace the rule by -$$ -\List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q. -\eqno(\forall E@3) -$$ -To replicate existential quantifiers, replace $(\exists I)$ by -\[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \] -All introduction rules mentioned above are also useful in swapped form. - -Replication makes the search space infinite; we must apply the rules with -care. The classical reasoner distinguishes between safe and unsafe -rules, applying the latter only when there is no alternative. Depth-first -search may well go down a blind alley; best-first search is better behaved -in an infinite search space. However, quantifier replication is too -expensive to prove any but the simplest theorems. - - \section{Classical rule sets} \index{classical sets} Each automatic tactic takes a {\bf classical set} --- a collection of