doc-src/Logics/FOL.tex
 changeset 313 a45ae7b38672 parent 287 6b62a6ddbe15 child 333 2ca08f62df33
--- a/doc-src/Logics/FOL.tex	Fri Apr 15 12:13:37 1994 +0200
+++ b/doc-src/Logics/FOL.tex	Fri Apr 15 12:42:30 1994 +0200
@@ -1,31 +1,30 @@
%% $Id$
-\chapter{First-Order logic}
-The directory~\ttindexbold{FOL} contains theories for first-order logic
-based on Gentzen's natural deduction systems (which he called {\sc nj} and
-{\sc nk}).  Intuitionistic logic is defined first; then classical logic is
+\chapter{First-Order Logic}
+\index{first-order logic|(}
+
+Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc
+  nk}.  Intuitionistic first-order logic is defined first, as theory
+\thydx{IFOL}.  Classical logic, theory \thydx{FOL}, is
obtained by adding the double negation rule.  Basic proof procedures are
provided.  The intuitionistic prover works with derived rules to simplify
-implications in the assumptions.  Classical logic makes use of Isabelle's
-generic prover for classical reasoning, which simulates a sequent calculus.
+implications in the assumptions.  Classical~{\tt FOL} employs Isabelle's
+classical reasoner, which simulates a sequent calculus.

\section{Syntax and rules of inference}
-The logic is many-sorted, using Isabelle's type classes.  The
-class of first-order terms is called {\it term} and is a subclass of
-{\it logic}.  No types of individuals
-are provided, but extensions can define types such as $nat::term$ and type
-constructors such as $list::(term)term$.  See the examples directory.
-Below, the type variable $\alpha$ ranges over class {\it term\/}; the
-equality symbol and quantifiers are polymorphic (many-sorted).  The type of
-formulae is~{\it o}, which belongs to class {\it logic}.
-Figure~\ref{fol-syntax} gives the syntax.  Note that $a$\verb|~=|$b$ is
-translated to \verb|~(|$a$=$b$\verb|)|.
+The logic is many-sorted, using Isabelle's type classes.  The class of
+first-order terms is called \cldx{term} and is a subclass of {\tt logic}.
+No types of individuals are provided, but extensions can define types such
+as {\tt nat::term} and type constructors such as {\tt list::(term)term}
+(see the examples directory, {\tt FOL/ex}).  Below, the type variable
+$\alpha$ ranges over class {\tt term}; the equality symbol and quantifiers
+are polymorphic (many-sorted).  The type of formulae is~\tydx{o}, which
+belongs to class~\cldx{logic}.  Figure~\ref{fol-syntax} gives the syntax.
+Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$.

-The intuitionistic theory has the \ML\ identifier
-\ttindexbold{IFOL.thy}.  Figure~\ref{fol-rules} shows the inference
-rules with their~\ML\ names.  Negation is defined in the usual way for
-intuitionistic logic; $\neg P$ abbreviates $P\imp\bot$.  The
-biconditional~($\bimp$) is defined through $\conj$ and~$\imp$; introduction
-and elimination rules are derived for it.
+Figure~\ref{fol-rules} shows the inference rules with their~\ML\ names.
+Negation is defined in the usual way for intuitionistic logic; $\neg P$
+abbreviates $P\imp\bot$.  The biconditional~($\bimp$) is defined through
+$\conj$ and~$\imp$; introduction and elimination rules are derived for it.

The unique existence quantifier, $\exists!x.P(x)$, is defined in terms
of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
@@ -41,7 +40,7 @@
$({\imp}E)$, and~$(\forall E)$.  Isabelle's backwards style handles these
rules badly, so sequent-style rules are derived to eliminate conjunctions,
implications, and universal quantifiers.  Used with elim-resolution,
-\ttindex{allE} eliminates a universal quantifier while \ttindex{all_dupE}
+\tdx{allE} eliminates a universal quantifier while \tdx{all_dupE}
re-inserts the quantified formula for later use.  The rules {\tt
conj_impE}, etc., support the intuitionistic proof procedure
(see~\S\ref{fol-int-prover}).
@@ -54,35 +53,36 @@
\begin{center}
\begin{tabular}{rrr}
\it name      &\it meta-type  & \it description \\
-  \idx{Trueprop}& $o\To prop$           & coercion to $prop$\\
-  \idx{Not}     & $o\To o$              & negation ($\neg$) \\
-  \idx{True}    & $o$                   & tautology ($\top$) \\
-  \idx{False}   & $o$                   & absurdity ($\bot$)
+  \cdx{Trueprop}& $o\To prop$           & coercion to $prop$\\
+  \cdx{Not}     & $o\To o$              & negation ($\neg$) \\
+  \cdx{True}    & $o$                   & tautology ($\top$) \\
+  \cdx{False}   & $o$                   & absurdity ($\bot$)
\end{tabular}
\end{center}
\subcaption{Constants}

\begin{center}
\begin{tabular}{llrrr}
-  \it symbol &\it name     &\it meta-type & \it precedence & \it description \\
-  \idx{ALL}  & \idx{All}  & $(\alpha\To o)\To o$ & 10 &
+  \it symbol &\it name     &\it meta-type & \it priority & \it description \\
+  \sdx{ALL}  & \cdx{All}  & $(\alpha\To o)\To o$ & 10 &
universal quantifier ($\forall$) \\
-  \idx{EX}   & \idx{Ex}   & $(\alpha\To o)\To o$ & 10 &
+  \sdx{EX}   & \cdx{Ex}   & $(\alpha\To o)\To o$ & 10 &
existential quantifier ($\exists$) \\
-  \idx{EX!}  & \idx{Ex1}  & $(\alpha\To o)\To o$ & 10 &
+  {\tt EX!}  & \cdx{Ex1}  & $(\alpha\To o)\To o$ & 10 &
unique existence ($\exists!$)
\end{tabular}
+\index{*"E"X"! symbol}
\end{center}
\subcaption{Binders}

\begin{center}
-\indexbold{*"=}
-\indexbold{&@{\tt\&}}
-\indexbold{*"|}
-\indexbold{*"-"-">}
-\indexbold{*"<"-">}
+\index{*"= symbol}
+\index{&@{\tt\&} symbol}
+\index{*"| symbol}
+\index{*"-"-"> symbol}
+\index{*"<"-"> symbol}
\begin{tabular}{rrrr}
-  \it symbol    & \it meta-type & \it precedence & \it description \\
+  \it symbol    & \it meta-type         & \it priority & \it description \\
\tt =         & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\
\tt \&        & $[o,o]\To o$          & Right 35 & conjunction ($\conj$) \\
\tt |         & $[o,o]\To o$          & Right 30 & disjunction ($\disj$) \\
@@ -114,81 +114,81 @@

\begin{figure}
\begin{ttbox}
-\idx{refl}        a=a
-\idx{subst}       [| a=b;  P(a) |] ==> P(b)
+\tdx{refl}        a=a
+\tdx{subst}       [| a=b;  P(a) |] ==> P(b)
\subcaption{Equality rules}

-\idx{conjI}       [| P;  Q |] ==> P&Q
-\idx{conjunct1}   P&Q ==> P
-\idx{conjunct2}   P&Q ==> Q
+\tdx{conjI}       [| P;  Q |] ==> P&Q
+\tdx{conjunct1}   P&Q ==> P
+\tdx{conjunct2}   P&Q ==> Q

-\idx{disjI1}      P ==> P|Q
-\idx{disjI2}      Q ==> P|Q
-\idx{disjE}       [| P|Q;  P ==> R;  Q ==> R |] ==> R
+\tdx{disjI1}      P ==> P|Q
+\tdx{disjI2}      Q ==> P|Q
+\tdx{disjE}       [| P|Q;  P ==> R;  Q ==> R |] ==> R

-\idx{impI}        (P ==> Q) ==> P-->Q
-\idx{mp}          [| P-->Q;  P |] ==> Q
+\tdx{impI}        (P ==> Q) ==> P-->Q
+\tdx{mp}          [| P-->Q;  P |] ==> Q

-\idx{FalseE}      False ==> P
+\tdx{FalseE}      False ==> P
\subcaption{Propositional rules}

-\idx{allI}        (!!x. P(x))  ==> (ALL x.P(x))
-\idx{spec}        (ALL x.P(x)) ==> P(x)
+\tdx{allI}        (!!x. P(x))  ==> (ALL x.P(x))
+\tdx{spec}        (ALL x.P(x)) ==> P(x)

-\idx{exI}         P(x) ==> (EX x.P(x))
-\idx{exE}         [| EX x.P(x);  !!x. P(x) ==> R |] ==> R
+\tdx{exI}         P(x) ==> (EX x.P(x))
+\tdx{exE}         [| EX x.P(x);  !!x. P(x) ==> R |] ==> R
\subcaption{Quantifier rules}

-\idx{True_def}    True        == False-->False
-\idx{not_def}     ~P          == P-->False
-\idx{iff_def}     P<->Q       == (P-->Q) & (Q-->P)
-\idx{ex1_def}     EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)
+\tdx{True_def}    True        == False-->False
+\tdx{not_def}     ~P          == P-->False
+\tdx{iff_def}     P<->Q       == (P-->Q) & (Q-->P)
+\tdx{ex1_def}     EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)
\subcaption{Definitions}
\end{ttbox}

-\caption{Rules of intuitionistic {\tt FOL}} \label{fol-rules}
+\caption{Rules of intuitionistic logic} \label{fol-rules}
\end{figure}

\begin{figure}
\begin{ttbox}
-\idx{sym}       a=b ==> b=a
-\idx{trans}     [| a=b;  b=c |] ==> a=c
-\idx{ssubst}    [| b=a;  P(a) |] ==> P(b)
+\tdx{sym}       a=b ==> b=a
+\tdx{trans}     [| a=b;  b=c |] ==> a=c
+\tdx{ssubst}    [| b=a;  P(a) |] ==> P(b)
\subcaption{Derived equality rules}

-\idx{TrueI}     True
+\tdx{TrueI}     True

-\idx{notI}      (P ==> False) ==> ~P
-\idx{notE}      [| ~P;  P |] ==> R
+\tdx{notI}      (P ==> False) ==> ~P
+\tdx{notE}      [| ~P;  P |] ==> R

-\idx{iffI}      [| P ==> Q;  Q ==> P |] ==> P<->Q
-\idx{iffE}      [| P <-> Q;  [| P-->Q; Q-->P |] ==> R |] ==> R
-\idx{iffD1}     [| P <-> Q;  P |] ==> Q
-\idx{iffD2}     [| P <-> Q;  Q |] ==> P
+\tdx{iffI}      [| P ==> Q;  Q ==> P |] ==> P<->Q
+\tdx{iffE}      [| P <-> Q;  [| P-->Q; Q-->P |] ==> R |] ==> R
+\tdx{iffD1}     [| P <-> Q;  P |] ==> Q
+\tdx{iffD2}     [| P <-> Q;  Q |] ==> P

-\idx{ex1I}      [| P(a);  !!x. P(x) ==> x=a |]  ==>  EX! x. P(x)
-\idx{ex1E}      [| EX! x.P(x);  !!x.[| P(x);  ALL y. P(y) --> y=x |] ==> R
+\tdx{ex1I}      [| P(a);  !!x. P(x) ==> x=a |]  ==>  EX! x. P(x)
+\tdx{ex1E}      [| EX! x.P(x);  !!x.[| P(x);  ALL y. P(y) --> y=x |] ==> R
|] ==> R
\subcaption{Derived rules for $$\top$$, $$\neg$$, $$\bimp$$ and $$\exists!$$}

-\idx{conjE}     [| P&Q;  [| P; Q |] ==> R |] ==> R
-\idx{impE}      [| P-->Q;  P;  Q ==> R |] ==> R
-\idx{allE}      [| ALL x.P(x);  P(x) ==> R |] ==> R
-\idx{all_dupE}  [| ALL x.P(x);  [| P(x); ALL x.P(x) |] ==> R |] ==> R
+\tdx{conjE}     [| P&Q;  [| P; Q |] ==> R |] ==> R
+\tdx{impE}      [| P-->Q;  P;  Q ==> R |] ==> R
+\tdx{allE}      [| ALL x.P(x);  P(x) ==> R |] ==> R
+\tdx{all_dupE}  [| ALL x.P(x);  [| P(x); ALL x.P(x) |] ==> R |] ==> R
\subcaption{Sequent-style elimination rules}

-\idx{conj_impE} [| (P&Q)-->S;  P-->(Q-->S) ==> R |] ==> R
-\idx{disj_impE} [| (P|Q)-->S;  [| P-->S; Q-->S |] ==> R |] ==> R
-\idx{imp_impE}  [| (P-->Q)-->S;  [| P; Q-->S |] ==> Q;  S ==> R |] ==> R
-\idx{not_impE}  [| ~P --> S;  P ==> False;  S ==> R |] ==> R
-\idx{iff_impE}  [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P;
+\tdx{conj_impE} [| (P&Q)-->S;  P-->(Q-->S) ==> R |] ==> R
+\tdx{disj_impE} [| (P|Q)-->S;  [| P-->S; Q-->S |] ==> R |] ==> R
+\tdx{imp_impE}  [| (P-->Q)-->S;  [| P; Q-->S |] ==> Q;  S ==> R |] ==> R
+\tdx{not_impE}  [| ~P --> S;  P ==> False;  S ==> R |] ==> R
+\tdx{iff_impE}  [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P;
S ==> R |] ==> R
-\idx{all_impE}  [| (ALL x.P(x))-->S;  !!x.P(x);  S ==> R |] ==> R
-\idx{ex_impE}   [| (EX x.P(x))-->S;  P(a)-->S ==> R |] ==> R
+\tdx{all_impE}  [| (ALL x.P(x))-->S;  !!x.P(x);  S ==> R |] ==> R
+\tdx{ex_impE}   [| (EX x.P(x))-->S;  P(a)-->S ==> R |] ==> R
\end{ttbox}
\subcaption{Intuitionistic simplification of implication}
-\caption{Derived rules for {\tt FOL}} \label{fol-int-derived}
+\caption{Derived rules for intuitionistic logic} \label{fol-int-derived}
\end{figure}

@@ -206,37 +206,40 @@
simplification set for classical logic.  Both equality ($=$) and the
biconditional ($\bimp$) may be used for rewriting.  See the file
{\tt FOL/simpdata.ML} for a complete listing of the simplification
-rules.
+rules%
+\iflabelundefined{sec:setting-up-simp}{}%
+        {, and \S\ref{sec:setting-up-simp} for discussion}.
+
\item
-It instantiates the classical reasoning module.  See~\S\ref{fol-cla-prover}
+It instantiates the classical reasoner.  See~\S\ref{fol-cla-prover}
for details.
\end{itemize}

\section{Intuitionistic proof procedures} \label{fol-int-prover}
Implication elimination (the rules~{\tt mp} and~{\tt impE}) pose
-difficulties for automated proof.  Given $P\imp Q$ we may assume $Q$
-provided we can prove $P$.  In classical logic the proof of $P$ can assume
-$\neg P$, but the intuitionistic proof of $P$ may require repeated use of
-$P\imp Q$.  If the proof of $P$ fails then the whole branch of the proof
-must be abandoned.  Thus intuitionistic propositional logic requires
-backtracking.  For an elementary example, consider the intuitionistic proof
-of $Q$ from $P\imp Q$ and $(P\imp Q)\imp P$.  The implication $P\imp Q$ is
-needed twice:
+difficulties for automated proof.  In intuitionistic logic, the assumption
+$P\imp Q$ cannot be treated like $\neg P\disj Q$.  Given $P\imp Q$, we may
+use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated
+use of $P\imp Q$.  If the proof of~$P$ fails then the whole branch of the
+proof must be abandoned.  Thus intuitionistic propositional logic requires
+backtracking.
+
+For an elementary example, consider the intuitionistic proof of $Q$ from
+$P\imp Q$ and $(P\imp Q)\imp P$.  The implication $P\imp Q$ is needed
+twice:
$\infer[({\imp}E)]{Q}{P\imp Q & \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}}$
The theorem prover for intuitionistic logic does not use~{\tt impE}.\@
Instead, it simplifies implications using derived rules
(Fig.\ts\ref{fol-int-derived}).  It reduces the antecedents of implications
-to atoms and then uses Modus Ponens: from $P\imp Q$ and $P$ deduce~$Q$.
-The rules \ttindex{conj_impE} and \ttindex{disj_impE} are
+to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$.
+The rules \tdx{conj_impE} and \tdx{disj_impE} are
straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and
$(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp S$.  The other \ldots{\tt_impE} rules are unsafe; the method requires
-backtracking.  Observe that \ttindex{imp_impE} does not admit the (unsound)
-inference of~$P$ from $(P\imp Q)\imp S$.  All the rules are derived in
-essentially the same simple manner.
+backtracking.  All the rules are derived in the same simple manner.

Dyckhoff has independently discovered similar rules, and (more importantly)
has demonstrated their completeness for propositional
@@ -248,17 +251,17 @@
eq_mp_tac         : int -> tactic
Int.safe_step_tac : int -> tactic
Int.safe_tac      :        tactic
+Int.inst_step_tac : int -> tactic
Int.step_tac      : int -> tactic
Int.fast_tac      : int -> tactic
Int.best_tac      : int -> tactic
\end{ttbox}
-Most of these belong to the structure \ttindexbold{Int}.  They are
-similar or identical to tactics (with the same names) provided by
-Isabelle's classical module (see the {\em Reference Manual\/}).
+Most of these belong to the structure {\tt Int} and resemble the
+tactics of Isabelle's classical reasoner.

-\begin{description}
+\begin{ttdescription}
\item[\ttindexbold{mp_tac} {\it i}]
-attempts to use \ttindex{notE} or \ttindex{impE} within the assumptions in
+attempts to use \tdx{notE} or \tdx{impE} within the assumptions in
subgoal $i$.  For each assumption of the form $\neg P$ or $P\imp Q$, it
searches for another assumption unifiable with~$P$.  By
contradiction with $\neg P$ it can solve the subgoal completely; by Modus
@@ -270,8 +273,8 @@
is safe.

\item[\ttindexbold{Int.safe_step_tac} $i$] performs a safe step on
-subgoal~$i$.  This may include proof by assumption or Modus Ponens, taking
-care not to instantiate unknowns, or \ttindex{hyp_subst_tac}.
+subgoal~$i$.  This may include proof by assumption or Modus Ponens (taking
+care not to instantiate unknowns), or {\tt hyp_subst_tac}.

\item[\ttindexbold{Int.safe_tac}] repeatedly performs safe steps on all
subgoals.  It is deterministic, with at most one outcome.
@@ -279,20 +282,16 @@
\item[\ttindexbold{Int.inst_step_tac} $i$] is like {\tt safe_step_tac},
but allows unknowns to be instantiated.

-\item[\ttindexbold{step_tac} $i$] tries {\tt safe_tac} or {\tt
-inst_step_tac}, or applies an unsafe rule.  This is the basic step of the
-proof procedure.
-
-\item[\ttindexbold{Int.step_tac} $i$] tries {\tt safe_tac} or
-certain unsafe inferences.  This is the basic step of the intuitionistic
-proof procedure.
+\item[\ttindexbold{Int.step_tac} $i$] tries {\tt safe_tac} or {\tt
+    inst_step_tac}, or applies an unsafe rule.  This is the basic step of
+  the intuitionistic proof procedure.

\item[\ttindexbold{Int.fast_tac} $i$] applies {\tt step_tac}, using
depth-first search, to solve subgoal~$i$.

\item[\ttindexbold{Int.best_tac} $i$] applies {\tt step_tac}, using
best-first search (guided by the size of the proof state) to solve subgoal~$i$.
-\end{description}
+\end{ttdescription}
Here are some of the theorems that {\tt Int.fast_tac} proves
automatically.  The latter three date from {\it Principia Mathematica}
(*11.53, *11.55, *11.61)~\cite{principia}.
@@ -307,22 +306,22 @@

\begin{figure}
\begin{ttbox}
-\idx{excluded_middle}    ~P | P
+\tdx{excluded_middle}    ~P | P

-\idx{disjCI}    (~Q ==> P) ==> P|Q
-\idx{exCI}      (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)
-\idx{impCE}     [| P-->Q; ~P ==> R; Q ==> R |] ==> R
-\idx{iffCE}     [| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
-\idx{notnotD}   ~~P ==> P
-\idx{swap}      ~P ==> (~Q ==> P) ==> Q
+\tdx{disjCI}    (~Q ==> P) ==> P|Q
+\tdx{exCI}      (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)
+\tdx{impCE}     [| P-->Q; ~P ==> R; Q ==> R |] ==> R
+\tdx{iffCE}     [| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
+\tdx{notnotD}   ~~P ==> P
+\tdx{swap}      ~P ==> (~Q ==> P) ==> Q
\end{ttbox}
\caption{Derived rules for classical logic} \label{fol-cla-derived}
\end{figure}

\section{Classical proof procedures} \label{fol-cla-prover}
-The classical theory has the \ML\ identifier \ttindexbold{FOL.thy}.  It
-consists of intuitionistic logic plus the rule
+The classical theory, \thydx{FOL}, consists of intuitionistic logic plus
+the rule
$$\vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical)$$
\noindent
Natural deduction in classical logic is not really all that natural.
@@ -330,11 +329,11 @@
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
rule (see Fig.\ts\ref{fol-cla-derived}).

-The classical reasoning module is set up for \FOL, as the
-structure~\ttindexbold{Cla}.  This structure is open, so \ML{} identifiers
+The classical reasoner is set up for \FOL, as the
+structure~{\tt Cla}.  This structure is open, so \ML{} identifiers
such as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
Single-step proofs can be performed, using \ttindex{swap_res_tac} to deal
-with negated assumptions.
+with negated assumptions.\index{assumptions!negated}

{\FOL} defines the following classical rule sets:
\begin{ttbox}
@@ -342,28 +341,30 @@
FOL_cs     : claset
FOL_dup_cs : claset
\end{ttbox}
-\begin{description}
+\begin{ttdescription}
\item[\ttindexbold{prop_cs}] contains the propositional rules, namely
those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
-along with the rule~\ttindex{refl}.
+along with the rule~{\tt refl}.

\item[\ttindexbold{FOL_cs}]
-extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}
-and the unsafe rules \ttindex{allE} and~\ttindex{exI}, as well as rules for
+extends {\tt prop_cs} with the safe rules {\tt allI} and~{\tt exE}
+and the unsafe rules {\tt allE} and~{\tt exI}, as well as rules for
unique existence.  Search using this is incomplete since quantified
formulae are used at most once.

\item[\ttindexbold{FOL_dup_cs}]
-extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}
-and the unsafe rules \ttindex{all_dupE} and~\ttindex{exCI}, as well as
+extends {\tt prop_cs} with the safe rules {\tt allI} and~{\tt exE}
+and the unsafe rules {\tt all_dupE} and~{\tt exCI}, as well as
rules for unique existence.  Search using this is complete --- quantified
formulae may be duplicated --- but frequently fails to terminate.  It is
generally unsuitable for depth-first search.
-\end{description}
+\end{ttdescription}
\noindent
See the file {\tt FOL/fol.ML} for derivations of the
-classical rules, and the {\em Reference Manual} for more discussion of
-classical proof methods.
+classical rules, and
+\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
+        {Chap.\ts\ref{chap:classical}}
+for more discussion of classical proof methods.

\section{An intuitionistic example}
@@ -383,7 +384,7 @@
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
{\out  1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)}
\end{ttbox}
-In this example we will never have more than one subgoal.  Applying
+In this example, we shall never have more than one subgoal.  Applying
$({\imp}I)$ replaces~\verb|-->| by~\verb|==>|, making
$$\ex{y}\all{x}Q(x,y)$$ an assumption.  We have the choice of
$({\exists}E)$ and $({\forall}I)$; let us try the latter.
@@ -395,7 +396,7 @@
\end{ttbox}
Applying $({\forall}I)$ replaces the \hbox{\tt ALL x} by \hbox{\tt!!x},
changing the universal quantifier from object~($\forall$) to
-meta~($\Forall$).  The bound variable is a {\em parameter\/} of the
+meta~($\Forall$).  The bound variable is a {\bf parameter} of the
subgoal.  We now must choose between $({\exists}I)$ and $({\exists}E)$.  What
happens if the wrong rule is chosen?
\begin{ttbox}
@@ -415,11 +416,10 @@
{\out  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
\end{ttbox}
Applying $(\exists E)$ has produced the parameter {\tt y} and stripped the
-existential quantifier from the assumption.  But the subgoal is unprovable.
-There is no way to unify {\tt ?y2(x)} with the bound variable~{\tt y}:
-assigning \verb|%x.y| to {\tt ?y2} is illegal because {\tt ?y2} is in the
-scope of the bound variable {\tt y}.  Using \ttindex{choplev} we
-can return to the mistake.  This time we apply $({\exists}E)$:
+existential quantifier from the assumption.  But the subgoal is unprovable:
+there is no way to unify {\tt ?y2(x)} with the bound variable~{\tt y}.
+Using {\tt choplev} we can return to the critical point.  This time we
+apply $({\exists}E)$:
\begin{ttbox}
choplev 2;
{\out Level 2}
@@ -431,9 +431,10 @@
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
{\out  1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
\end{ttbox}
-We now have two parameters and no scheme variables.  Parameters should be
-produced early.  Applying $({\exists}I)$ and $({\forall}E)$ will produce
-two scheme variables.
+We now have two parameters and no scheme variables.  Applying
+$({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are
+applied to those parameters.  Parameters should be produced early, as this
+example demonstrates.
\begin{ttbox}
by (resolve_tac [exI] 1);
{\out Level 4}
@@ -455,7 +456,7 @@
{\out No subgoals!}
\end{ttbox}
The theorem was proved in six tactic steps, not counting the abandoned
-ones.  But proof checking is tedious; {\tt Int.fast_tac} proves the
+ones.  But proof checking is tedious; \ttindex{Int.fast_tac} proves the
theorem in one step.
\begin{ttbox}
goal IFOL.thy "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
@@ -474,19 +475,18 @@
elimination.  Even propositional formulae can be difficult to prove from
the basic rules; the specialized rules help considerably.

-Propositional examples are easy to invent, for as Dummett notes~\cite[page
+Propositional examples are easy to invent.  As Dummett notes~\cite[page
28]{dummett}, $\neg P$ is classically provable if and only if it is
-intuitionistically provable.  Therefore, $P$ is classically provable if and
-only if $\neg\neg P$ is intuitionistically provable.  In both cases, $P$
-must be a propositional formula (no quantifiers).  Our example,
-accordingly, is the double negation of a classical tautology: $(P\imp -Q)\disj (Q\imp P)$.
+intuitionistically provable;  therefore, $P$ is classically provable if and
+only if $\neg\neg P$ is intuitionistically provable.%
+\footnote{Of course this holds only for propositional logic, not if $P$ is
+  allowed to contain quantifiers.} Proving $\neg\neg P$ intuitionistically is
+much harder than proving~$P$ classically.

-When stating the goal, we command Isabelle to expand the negation symbol,
-using the definition $\neg P\equiv P\imp\bot$.  Although negation possesses
-derived rules that effect precisely this definition --- the automatic
-tactics apply them --- it seems more straightforward to unfold the
-negations.
+Our example is the double negation of the classical tautology $(P\imp +Q)\disj (Q\imp P)$.  When stating the goal, we command Isabelle to expand
+negations to implications using the definition $\neg P\equiv P\imp\bot$.
+This allows use of the special implication rules.
\begin{ttbox}
goalw IFOL.thy [not_def] "~ ~ ((P-->Q) | (Q-->P))";
{\out Level 0}
@@ -500,9 +500,10 @@
{\out ~ ~ ((P --> Q) | (Q --> P))}
{\out  1. (P --> Q) | (Q --> P) --> False ==> False}
\end{ttbox}
-Proving $(P\imp Q)\disj (Q\imp P)$ would suffice, but this formula is
-constructively invalid.  Instead we apply \ttindex{disj_impE}.  It splits
-the assumption into two parts, one for each disjunct.
+By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but
+that formula is not a theorem of intuitionistic logic.  Instead we apply
+the specialized implication rule \tdx{disj_impE}.  It splits the
+assumption into two assumptions, one for each disjunct.
\begin{ttbox}
by (eresolve_tac [disj_impE] 1);
{\out Level 2}
@@ -510,7 +511,7 @@
{\out  1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False}
\end{ttbox}
We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but
-their negations are inconsistent.  Applying \ttindex{imp_impE} breaks down
+their negations are inconsistent.  Applying \tdx{imp_impE} breaks down
the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new
assumptions~$P$ and~$\neg Q$.
\begin{ttbox}
@@ -522,7 +523,7 @@
\end{ttbox}
Subgoal~2 holds trivially; let us ignore it and continue working on
subgoal~1.  Thanks to the assumption~$P$, we could prove $Q\imp P$;
-applying \ttindex{imp_impE} is simpler.
+applying \tdx{imp_impE} is simpler.
\begin{ttbox}
by (eresolve_tac [imp_impE] 1);
{\out Level 4}
@@ -548,12 +549,12 @@

\section{A classical example} \label{fol-cla-example}
To illustrate classical logic, we shall prove the theorem
-$\ex{y}\all{x}P(y)\imp P(x)$.  Classically, the theorem can be proved as
+$\ex{y}\all{x}P(y)\imp P(x)$.  Informally, the theorem can be proved as
follows.  Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
$\all{x}P(x)$ is true.  Either way the theorem holds.

The formal proof does not conform in any obvious way to the sketch given
-above.  The key inference is the first one, \ttindex{exCI}; this classical
+above.  The key inference is the first one, \tdx{exCI}; this classical
version of~$(\exists I)$ allows multiple instantiation of the quantifier.
\begin{ttbox}
goal FOL.thy "EX y. ALL x. P(y)-->P(x)";
@@ -566,9 +567,9 @@
{\out EX y. ALL x. P(y) --> P(x)}
{\out  1. ALL y. ~ (ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)}
\end{ttbox}
-We now can either exhibit a term {\tt?a} to satisfy the conclusion of
+We can either exhibit a term {\tt?a} to satisfy the conclusion of
subgoal~1, or produce a contradiction from the assumption.  The next
-steps routinely break down the conclusion and assumption.
+steps are routine.
\begin{ttbox}
by (resolve_tac [allI] 1);
{\out Level 2}
@@ -579,14 +580,17 @@
{\out Level 3}
{\out EX y. ALL x. P(y) --> P(x)}
{\out  1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)}
-\ttbreak
+\end{ttbox}
+By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
+effectively applies~$(\exists I)$ again.
+\begin{ttbox}
by (eresolve_tac [allE] 1);
{\out Level 4}
{\out EX y. ALL x. P(y) --> P(x)}
{\out  1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
\end{ttbox}
In classical logic, a negated assumption is equivalent to a conclusion.  To
-get this effect, we create a swapped version of $(\forall I)$ and apply it
+get this effect, we create a swapped version of~$(\forall I)$ and apply it
using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall I)$ using \ttindex{swap_res_tac}.
\begin{ttbox}
@@ -597,8 +601,7 @@
{\out EX y. ALL x. P(y) --> P(x)}
{\out  1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)}
\end{ttbox}
-The previous conclusion, {\tt P(x)}, has become a negated assumption;
-we apply~$({\imp}I)$:
+The previous conclusion, {\tt P(x)}, has become a negated assumption.
\begin{ttbox}
by (resolve_tac [impI] 1);
{\out Level 6}
@@ -606,8 +609,8 @@
{\out  1. !!x xa. [| P(?a); ~ P(x); P(?y3(x)) |] ==> P(xa)}
\end{ttbox}
The subgoal has three assumptions.  We produce a contradiction between the
-assumptions~\verb|~P(x)| and~{\tt P(?y3(x))}.  The proof never instantiates
-the unknown~{\tt?a}.
+  P(?y3(x))}.  The proof never instantiates the unknown~{\tt?a}.
\begin{ttbox}
by (eresolve_tac [notE] 1);
{\out Level 7}
@@ -648,7 +651,7 @@

Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$
directly, without reference to its definition.  The simple identity
-$if(P,Q,R) \bimp (P\imp Q)\conj (\neg P\imp R)$
+$if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R)$
suggests that the
$if$-introduction rule should be
$\infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}}$
@@ -658,8 +661,8 @@
& \infer*{S}{[\neg P,R]}}
\]
Having made these plans, we get down to work with Isabelle.  The theory of
-classical logic, \ttindex{FOL}, is extended with the constant
-$if::[o,o,o]\To o$.  The axiom \ttindexbold{if_def} asserts the
+classical logic, {\tt FOL}, is extended with the constant
+$if::[o,o,o]\To o$.  The axiom \tdx{if_def} asserts the
equation~$(if)$.
\begin{ttbox}
If = FOL +
@@ -669,7 +672,7 @@
\end{ttbox}
The derivations of the introduction and elimination rules demonstrate the
methods for rewriting with definitions.  Classical reasoning is required,
-so we use \ttindex{fast_tac}.
+so we use {\tt fast_tac}.

\subsection{Deriving the introduction rule}
@@ -721,10 +724,12 @@
{\out No subgoals!}
val ifE = result();
\end{ttbox}
-As you may recall from {\em Introduction to Isabelle}, there are other
+As you may recall from
+\iflabelundefined{definitions}{{\em Introduction to Isabelle}}%
+        {\S\ref{definitions}}, there are other
ways of treating definitions when deriving a rule.  We can start the
-proof using \ttindex{goal}, which does not expand definitions, instead of
-\ttindex{goalw}.  We can use \ttindex{rewrite_goals_tac}
+proof using {\tt goal}, which does not expand definitions, instead of
+{\tt goalw}.  We can use \ttindex{rewrite_goals_tac}
to expand definitions in the subgoals --- perhaps after calling
\ttindex{cut_facts_tac} to insert the rule's premises.  We can use
\ttindex{rewrite_rule}, which is a meta-inference rule, to expand
@@ -732,15 +737,15 @@

\subsection{Using the derived rules}
-The rules just derived have been saved with the {\ML} names \ttindex{ifI}
-and~\ttindex{ifE}.  They permit natural proofs of theorems such as the
+The rules just derived have been saved with the {\ML} names \tdx{ifI}
+and~\tdx{ifE}.  They permit natural proofs of theorems such as the
following:
\begin{eqnarray*}
if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\
if(if(P,Q,R), A, B)         & \bimp & if(P,if(Q,A,B),if(R,A,B))
\end{eqnarray*}
Proofs also require the classical reasoning rules and the $\bimp$
-introduction rule (called~\ttindex{iffI}: do not confuse with~\ttindex{ifI}).
+introduction rule (called~\tdx{iffI}: do not confuse with~{\tt ifI}).

To display the $if$-rules in action, let us analyse a proof step by step.
\begin{ttbox}
@@ -921,3 +926,5 @@

Expanding definitions causes a great increase in complexity.  This is why
the classical prover has been designed to accept derived rules.
+
+\index{first-order logic|)}