doc-src/ZF/FOL.tex

removed obsolete support for polyml-4.9.1;

%% $Id$
\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~\texttt{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 \cldx{term} and is a subclass of \isa{logic}.
No types of individuals are provided, but extensions can define types such
as \isa{nat::term} and type constructors such as \isa{list::(term)term}
(see the examples directory, \texttt{FOL/ex}).  Below, the type variable
$\alpha$ ranges over class \isa{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)$.

Figure~\ref{fol-rules} shows the inference rules with their 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
quantifications.  For instance, $\exists!x\;y.P(x,y)$ abbreviates
$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
exists a unique pair $(x,y)$ satisfying~$P(x,y)$.

Some intuitionistic derived rules are shown in
Fig.\ts\ref{fol-int-derived}, again with their names.  These include
rules for the defined symbols $\neg$, $\bimp$ and $\exists!$.  Natural
deduction typically involves a combination of forward and backward
reasoning, particularly with the destruction rules $(\conj E)$,
$({\imp}E)$, and~$(\forall E)$.  Isabelle's backward style handles these
rules badly, so sequent-style rules are derived to eliminate conjunctions,
implications, and universal quantifiers.  Used with elim-resolution,
\tdx{allE} eliminates a universal quantifier while \tdx{all_dupE}
re-inserts the quantified formula for later use.  The rules
\isa{conj\_impE}, etc., support the intuitionistic proof procedure
(see~\S\ref{fol-int-prover}).

See the on-line theory library for complete listings of the rules and
derived rules.

\begin{figure} 
\begin{center}
\begin{tabular}{rrr} 
  \it name      &\it meta-type  & \it description \\ 
  \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 priority & \it description \\
  \sdx{ALL}  & \cdx{All}  & $(\alpha\To o)\To o$ & 10 & 
        universal quantifier ($\forall$) \\
  \sdx{EX}   & \cdx{Ex}   & $(\alpha\To o)\To o$ & 10 & 
        existential quantifier ($\exists$) \\
  \isa{EX!}  & \cdx{Ex1}  & $(\alpha\To o)\To o$ & 10 & 
        unique existence ($\exists!$)
\end{tabular}
\index{*"E"X"! symbol}
\end{center}
\subcaption{Binders} 

\begin{center}
\index{*"= symbol}
\index{&@{\tt\&} symbol}
\index{*"| symbol}
\index{*"-"-"> symbol}
\index{*"<"-"> symbol}
\begin{tabular}{rrrr} 
  \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$) \\
  \tt -->       & $[o,o]\To o$          & Right 25 & implication ($\imp$) \\
  \tt <->       & $[o,o]\To o$          & Right 25 & biconditional ($\bimp$) 
\end{tabular}
\end{center}
\subcaption{Infixes}

\dquotes
\[\begin{array}{rcl}
 formula & = & \hbox{expression of type~$o$} \\
         & | & term " = " term \quad| \quad term " \ttilde= " term \\
         & | & "\ttilde\ " formula \\
         & | & formula " \& " formula \\
         & | & formula " | " formula \\
         & | & formula " --> " formula \\
         & | & formula " <-> " formula \\
         & | & "ALL~" id~id^* " . " formula \\
         & | & "EX~~" id~id^* " . " formula \\
         & | & "EX!~" id~id^* " . " formula
  \end{array}
\]
\subcaption{Grammar}
\caption{Syntax of \texttt{FOL}} \label{fol-syntax}
\end{figure}


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

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

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

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

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

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

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

\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 logic} \label{fol-rules}
\end{figure}


\begin{figure} 
\begin{ttbox}
\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}

\tdx{TrueI}     True

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

\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

\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!\)}

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

\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
\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 intuitionistic logic} \label{fol-int-derived}
\end{figure}


\section{Generic packages}
FOL instantiates most of Isabelle's generic packages.
\begin{itemize}
\item 
It instantiates the simplifier, which is invoked through the method 
\isa{simp}.  Both equality ($=$) and the biconditional
($\bimp$) may be used for rewriting.  

\item 
It instantiates the classical reasoner, which is invoked mainly through the 
methods \isa{blast} and \isa{auto}.  See~\S\ref{fol-cla-prover}
for details. 
%
%\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for
%  an equality throughout a subgoal and its hypotheses.  This tactic uses FOL's
%  general substitution rule.
\end{itemize}

\begin{warn}\index{simplification!of conjunctions}%
  Simplifying $a=b\conj P(a)$ to $a=b\conj P(b)$ is often advantageous.  The
  left part of a conjunction helps in simplifying the right part.  This effect
  is not available by default: it can be slow.  It can be obtained by
  including the theorem \isa{conj_cong}\index{*conj_cong (rule)}%
  as a congruence rule in
  simplification, \isa{simp cong:\ conj\_cong}.
\end{warn}


\section{Intuitionistic proof procedures} \label{fol-int-prover}
Implication elimination (the rules~\isa{mp} and~\isa{impE}) pose
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~\isa{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 \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\isa{\_impE} rules are unsafe; the method requires
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
logic~\cite{dyckhoff}.  However, the tactics given below are not complete
for first-order logic because they discard universally quantified
assumptions after a single use. These are \ML{} functions, and are listed
below with their \ML{} type:
\begin{ttbox} 
mp_tac              : int -> tactic
eq_mp_tac           : int -> tactic
IntPr.safe_step_tac : int -> tactic
IntPr.safe_tac      :        tactic
IntPr.inst_step_tac : int -> tactic
IntPr.step_tac      : int -> tactic
IntPr.fast_tac      : int -> tactic
IntPr.best_tac      : int -> tactic
\end{ttbox}
Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the
tactics of Isabelle's classical reasoner.  There are no corresponding
Isar methods, but you can use the 
\isa{tactic} method to call \ML{} tactics in an Isar script:
\begin{isabelle}
\isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*})
\end{isabelle}
Here is a description of each tactic:

\begin{ttdescription}
\item[\ttindexbold{mp_tac} {\it i}] 
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
Ponens it can replace the assumption $P\imp Q$ by $Q$.  The tactic can
produce multiple outcomes, enumerating all suitable pairs of assumptions.

\item[\ttindexbold{eq_mp_tac} {\it i}] 
is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
is safe.

\item[\ttindexbold{IntPr.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 \texttt{hyp_subst_tac}. 

\item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all 
subgoals.  It is deterministic, with at most one outcome.

\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac},
but allows unknowns to be instantiated.

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

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

\item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using
best-first search (guided by the size of the proof state) to solve subgoal~$i$.
\end{ttdescription}
Here are some of the theorems that \texttt{IntPr.fast_tac} proves
automatically.  The latter three date from {\it Principia Mathematica}
(*11.53, *11.55, *11.61)~\cite{principia}.
\begin{ttbox}
~~P & ~~(P --> Q) --> ~~Q
(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))
(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))
(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))
\end{ttbox}



\begin{figure} 
\begin{ttbox}
\tdx{excluded_middle}    ~P | P

\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, \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.  FOL
derives classical introduction rules for $\disj$ and~$\exists$, as well as
classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see
Fig.\ts\ref{fol-cla-derived}).

The classical reasoner is installed.  The most useful methods are
\isa{blast} (pure classical reasoning) and \isa{auto} (classical reasoning
combined with simplification), but the full range of
methods is available, including \isa{clarify},
\isa{fast}, \isa{best} and \isa{force}. 
 See the 
\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
        {Chap.\ts\ref{chap:classical}} 
and the \emph{Tutorial}~\cite{isa-tutorial}
for more discussion of classical proof methods.