%% $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 \texttt{logic}.

No types of individuals are provided, but extensions can define types such

as \texttt{nat::term} and type constructors such as \texttt{list::(term)term}

(see the examples directory, \texttt{FOL/ex}).  Below, the type variable

$\alpha$ ranges over class \texttt{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~\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

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 \ML\ 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 {\tt

conj_impE}, etc., support the intuitionistic proof procedure

(see~\S\ref{fol-int-prover}).

See the files \texttt{FOL/IFOL.thy}, \texttt{FOL/IFOL.ML} and

\texttt{FOL/intprover.ML} 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$) \\

  \texttt{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.  Both equality ($=$) and the biconditional

($\bimp$) may be used for rewriting.  Tactics such as \texttt{Asm_simp_tac} and

\texttt{Full_simp_tac} refer to the default simpset (\texttt{simpset()}), which works for

most purposes.  Named simplification sets include \ttindexbold{IFOL_ss},

for intuitionistic first-order logic, and \ttindexbold{FOL_ss},

for classical logic.  See the file

\texttt{FOL/simpdata.ML} for a complete listing of the simplification

rules%

\iflabelundefined{sec:setting-up-simp}{}%

        {, and \S\ref{sec:setting-up-simp} for discussion}.

\item 

It instantiates the classical reasoner.  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}%

  Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes 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 \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.

\end{warn}

\section{Intuitionistic proof procedures} \label{fol-int-prover}

Implication elimination (the rules~\texttt{mp} and~\texttt{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~\texttt{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{\tt_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.

\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 \texttt{IntPr} and resemble the

tactics of Isabelle's classical reasoner.

\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.  Tactics such as \texttt{Blast_tac} and {\tt

Best_tac} refer to the default claset (\texttt{claset()}), which works for most

purposes.  Named clasets include \ttindexbold{prop_cs}, which includes the

propositional rules, and \ttindexbold{FOL_cs}, which also includes quantifier

rules.  See the file \texttt{FOL/cladata.ML} for lists of the

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}

Here is a session similar to one in {\em Logic and Computation}

\cite[pages~222--3]{paulson87}.  Isabelle treats quantifiers differently

from {\sc lcf}-based theorem provers such as {\sc hol}.  

First, we specify that we are working in intuitionistic logic:

\begin{ttbox}

context IFOL.thy;

\end{ttbox}

The proof begins by entering the goal, then applying the rule $({\imp}I)$.

\begin{ttbox}

Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";

{\out Level 0}

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

\ttbreak

by (resolve_tac [impI] 1);

{\out Level 1}

{\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 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.

\begin{ttbox}

by (resolve_tac [allI] 1);

{\out Level 2}

{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}

{\out  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}

\end{ttbox}

Applying $({\forall}I)$ replaces the \texttt{ALL~x} by \hbox{\tt!!x},

changing the universal quantifier from object~($\forall$) to

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}

by (resolve_tac [exI] 1);

{\out Level 3}

{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}

{\out  1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))}

\end{ttbox}

The new subgoal~1 contains the function variable {\tt?y2}.  Instantiating

{\tt?y2} can replace~{\tt?y2(x)} by a term containing~\texttt{x}, even

though~\texttt{x} is a bound variable.  Now we analyse the assumption

\(\exists y.\forall x. Q(x,y)\) using elimination rules:

\begin{ttbox}

by (eresolve_tac [exE] 1);

{\out Level 4}

{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}

{\out  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))}

\end{ttbox}

Applying $(\exists E)$ has produced the parameter \texttt{y} and stripped the

existential quantifier from the assumption.  But the subgoal is unprovable:

there is no way to unify \texttt{?y2(x)} with the bound variable~\texttt{y}.

Using \texttt{choplev} we can return to the critical point.  This time we

apply $({\exists}E)$:

\begin{ttbox}

choplev 2;

{\out Level 2}

{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}

{\out  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}

\ttbreak

by (eresolve_tac [exE] 1);

{\out Level 3}

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

{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}

{\out  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))}

\ttbreak

by (eresolve_tac [allE] 1);

{\out Level 5}

{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}

{\out  1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))}

\end{ttbox}

The subgoal has variables \texttt{?y3} and \texttt{?x4} applied to both

parameters.  The obvious projection functions unify {\tt?x4(x,y)} with~{\tt

x} and \verb|?y3(x,y)| with~\texttt{y}.

\begin{ttbox}

by (assume_tac 1);

{\out Level 6}

{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}

{\out No subgoals!}

\end{ttbox}

The theorem was proved in six tactic steps, not counting the abandoned

ones.  But proof checking is tedious; \ttindex{IntPr.fast_tac} proves the

theorem in one step.

\begin{ttbox}

Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";

{\out Level 0}

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

by (IntPr.fast_tac 1);

{\out Level 1}

{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}

{\out No subgoals!}

\end{ttbox}

\section{An example of intuitionistic negation}

The following example demonstrates the specialized forms of implication

elimination.  Even propositional formulae can be difficult to prove from

the basic rules; the specialized rules help considerably.  

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.%

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

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 [not_def] "~ ~ ((P-->Q) | (Q-->P))";

{\out Level 0}

{\out ~ ~ ((P --> Q) | (Q --> P))}

{\out  1. ((P --> Q) | (Q --> P) --> False) --> False}

\end{ttbox}

The first step is trivial.

\begin{ttbox}

by (resolve_tac [impI] 1);

{\out Level 1}

{\out ~ ~ ((P --> Q) | (Q --> P))}

{\out  1. (P --> Q) | (Q --> P) --> False ==> False}

\end{ttbox}

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}

{\out ~ ~ ((P --> Q) | (Q --> P))}

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

by (eresolve_tac [imp_impE] 1);

{\out Level 3}

{\out ~ ~ ((P --> Q) | (Q --> P))}

{\out  1. [| (Q --> P) --> False; P; Q --> False |] ==> Q}

{\out  2. [| (Q --> P) --> False; False |] ==> False}

\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 \tdx{imp_impE} is simpler.

\begin{ttbox}

by (eresolve_tac [imp_impE] 1);

{\out Level 4}

{\out ~ ~ ((P --> Q) | (Q --> P))}

{\out  1. [| P; Q --> False; Q; P --> False |] ==> P}

{\out  2. [| P; Q --> False; False |] ==> Q}

{\out  3. [| (Q --> P) --> False; False |] ==> False}

\end{ttbox}

The three subgoals are all trivial.

\begin{ttbox}

by (REPEAT (eresolve_tac [FalseE] 2));

{\out Level 5}

{\out ~ ~ ((P --> Q) | (Q --> P))}

{\out  1. [| P; Q --> False; Q; P --> False |] ==> P}

\ttbreak

by (assume_tac 1);

{\out Level 6}

{\out ~ ~ ((P --> Q) | (Q --> P))}

{\out No subgoals!}

\end{ttbox}

This proof is also trivial for \texttt{IntPr.fast_tac}.

\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)$.  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.  First, we switch to

classical logic:

\begin{ttbox}

context FOL.thy;

\end{ttbox}

The formal proof does not conform in any obvious way to the sketch given

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 "EX y. ALL x. P(y)-->P(x)";

{\out Level 0}

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

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

\ttbreak

by (resolve_tac [exCI] 1);

{\out Level 1}

{\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 can either exhibit a term {\tt?a} to satisfy the conclusion of

subgoal~1, or produce a contradiction from the assumption.  The next

steps are routine.

\begin{ttbox}

by (resolve_tac [allI] 1);

{\out Level 2}

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

by (resolve_tac [impI] 1);

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

\end{ttbox}

By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$

in effect 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

using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall

I)$ using \ttindex{swap_res_tac}.

\begin{ttbox}

allI RSN (2,swap);

{\out val it = "[| ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}

by (eresolve_tac [it] 1);

{\out Level 5}

{\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, \texttt{P(x)}, has become a negated assumption.

\begin{ttbox}

by (resolve_tac [impI] 1);

{\out Level 6}

{\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 subgoal has three assumptions.  We produce a contradiction between the

\index{assumptions!contradictory} assumptions~\verb|~P(x)| and~{\tt

  P(?y3(x))}.  The proof never instantiates the unknown~{\tt?a}.

\begin{ttbox}

by (eresolve_tac [notE] 1);

{\out Level 7}

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

{\out  1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)}

\ttbreak

by (assume_tac 1);

{\out Level 8}

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

{\out No subgoals!}

\end{ttbox}

The civilised way to prove this theorem is through \ttindex{Blast_tac},

which automatically uses the classical version of~$(\exists I)$:

\begin{ttbox}

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

{\out Level 0}

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

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

by (Blast_tac 1);

{\out Depth = 0}

{\out Depth = 1}

{\out Depth = 2}

{\out Level 1}

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

{\out No subgoals!}

\end{ttbox}

If this theorem seems counterintuitive, then perhaps you are an

intuitionist.  In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$

requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$,

which we cannot do without further knowledge about~$P$.

\section{Derived rules and the classical tactics}

Classical first-order logic can be extended with the propositional

connective $if(P,Q,R)$, where 

$$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$

Theorems about $if$ can be proved by treating this as an abbreviation,

replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals.  But

this duplicates~$P$, causing an exponential blowup and an unreadable

formula.  Introducing further abbreviations makes the problem worse.

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) \]

suggests that the

$if$-introduction rule should be

\[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]}  &  \infer*{R}{[\neg P]}} \]

The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the

elimination rules for~$\disj$ and~$\conj$.

\[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}

                                  & \infer*{S}{[\neg P,R]}} 

\]

Having made these plans, we get down to work with Isabelle.  The theory of

classical logic, \texttt{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 +

consts  if     :: [o,o,o]=>o

rules   if_def "if(P,Q,R) == P&Q | ~P&R"

end

\end{ttbox}

We create the file \texttt{If.thy} containing these declarations.  (This file

is on directory \texttt{FOL/ex} in the Isabelle distribution.)  Typing

\begin{ttbox}

use_thy "If";  

\end{ttbox}

loads that theory and sets it to be the current context.

\subsection{Deriving the introduction rule}

The derivations of the introduction and elimination rules demonstrate the

methods for rewriting with definitions.  Classical reasoning is required,

so we use \texttt{blast_tac}.

The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,

concludes $if(P,Q,R)$.  We propose the conclusion as the main goal

using~\ttindex{Goalw}, which uses \texttt{if_def} to rewrite occurrences

of $if$ in the subgoal.

\begin{ttbox}

val prems = Goalw [if_def]

    "[| P ==> Q; ~ P ==> R |] ==> if(P,Q,R)";

{\out Level 0}

{\out if(P,Q,R)}

{\out  1. P & Q | ~ P & R}

\end{ttbox}

The premises (bound to the {\ML} variable \texttt{prems}) are passed as

introduction rules to \ttindex{blast_tac}.  Remember that \texttt{claset()} refers

to the default classical set.

\begin{ttbox}

by (blast_tac (claset() addIs prems) 1);

{\out Level 1}

{\out if(P,Q,R)}

{\out No subgoals!}

qed "ifI";

\end{ttbox}

\subsection{Deriving the elimination rule}

The elimination rule has three premises, two of which are themselves rules.

The conclusion is simply $S$.

\begin{ttbox}

val major::prems = Goalw [if_def]

   "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~ P; R |] ==> S |] ==> S";

{\out Level 0}

{\out S}

{\out  1. S}

\end{ttbox}

The major premise contains an occurrence of~$if$, but the version returned

by \ttindex{Goalw} (and bound to the {\ML} variable~\texttt{major}) has the

definition expanded.  Now \ttindex{cut_facts_tac} inserts~\texttt{major} as an

assumption in the subgoal, so that \ttindex{blast_tac} can break it down.

\begin{ttbox}

by (cut_facts_tac [major] 1);

{\out Level 1}

{\out S}

{\out  1. P & Q | ~ P & R ==> S}

\ttbreak

by (blast_tac (claset() addIs prems) 1);

{\out Level 2}

{\out S}

{\out No subgoals!}

qed "ifE";

\end{ttbox}

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 \texttt{Goal}, which does not expand definitions, instead of

\texttt{Goalw}.  We can use \ttindex{rew_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

definitions in the premises directly.

\subsection{Using the derived rules}

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~\tdx{iffI}: do not confuse with~\texttt{ifI}). 

To display the $if$-rules in action, let us analyse a proof step by step.

\begin{ttbox}

Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";

{\out Level 0}

{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}

{\out  1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}

\ttbreak

by (resolve_tac [iffI] 1);

{\out Level 1}

{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}

{\out  1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))}

{\out  2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}

\end{ttbox}

The $if$-elimination rule can be applied twice in succession.

\begin{ttbox}

by (eresolve_tac [ifE] 1);

{\out Level 2}

{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}

{\out  1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))}

{\out  2. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}

{\out  3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}

\ttbreak

by (eresolve_tac [ifE] 1);

{\out Level 3}

{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}

{\out  1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))}

{\out  2. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}

{\out  3. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}

{\out  4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}

\end{ttbox}

%

In the first two subgoals, all assumptions have been reduced to atoms.  Now

$if$-introduction can be applied.  Observe how the $if$-rules break down

occurrences of $if$ when they become the outermost connective.

\begin{ttbox}

by (resolve_tac [ifI] 1);

{\out Level 4}

{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}

{\out  1. [| P; Q; A; Q |] ==> if(P,A,C)}

{\out  2. [| P; Q; A; ~ Q |] ==> if(P,B,D)}

{\out  3. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}

{\out  4. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}

{\out  5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}

\ttbreak

by (resolve_tac [ifI] 1);

{\out Level 5}

{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}

{\out  1. [| P; Q; A; Q; P |] ==> A}

{\out  2. [| P; Q; A; Q; ~ P |] ==> C}

{\out  3. [| P; Q; A; ~ Q |] ==> if(P,B,D)}

{\out  4. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}

{\out  5. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}

{\out  6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}

\end{ttbox}

Where do we stand?  The first subgoal holds by assumption; the second and

third, by contradiction.  This is getting tedious.  We could use the classical

reasoner, but first let us extend the default claset with the derived rules

for~$if$.

\begin{ttbox}

AddSIs [ifI];

AddSEs [ifE];

\end{ttbox}

Now we can revert to the

initial proof state and let \ttindex{blast_tac} solve it.  

\begin{ttbox}

choplev 0;

{\out Level 0}

{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}

{\out  1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}

by (Blast_tac 1);

{\out Level 1}

{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}

{\out No subgoals!}

\end{ttbox}

This tactic also solves the other example.

\begin{ttbox}

Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";

{\out Level 0}

{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}

{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}

\ttbreak

by (Blast_tac 1);

{\out Level 1}

{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}

{\out No subgoals!}

\end{ttbox}

\subsection{Derived rules versus definitions}

Dispensing with the derived rules, we can treat $if$ as an

abbreviation, and let \ttindex{blast_tac} prove the expanded formula.  Let

us redo the previous proof:

\begin{ttbox}

choplev 0;

{\out Level 0}

{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}

{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}

\end{ttbox}

This time, simply unfold using the definition of $if$:

\begin{ttbox}

by (rewtac if_def);

{\out Level 1}

{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}

{\out  1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}

{\out     P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)}

\end{ttbox}

We are left with a subgoal in pure first-order logic, which is why the 

classical reasoner can prove it given \texttt{FOL_cs} alone.  (We could, of 

course, have used \texttt{Blast_tac}.)

\begin{ttbox}

by (blast_tac FOL_cs 1);

{\out Level 2}

{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}

{\out No subgoals!}

\end{ttbox}

Expanding definitions reduces the extended logic to the base logic.  This

approach has its merits --- especially if the prover for the base logic is

good --- but can be slow.  In these examples, proofs using the default

claset (which includes the derived rules) run about six times faster 

than proofs using \texttt{FOL_cs}.

Expanding definitions also complicates error diagnosis.  Suppose we are having

difficulties in proving some goal.  If by expanding definitions we have

made it unreadable, then we have little hope of diagnosing the problem.

Attempts at program verification often yield invalid assertions.

Let us try to prove one:

\begin{ttbox}

Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";

{\out Level 0}

{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}

{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}

by (Blast_tac 1);

{\out by: tactic failed}

\end{ttbox}

This failure message is uninformative, but we can get a closer look at the

situation by applying \ttindex{Step_tac}.

\begin{ttbox}

by (REPEAT (Step_tac 1));

{\out Level 1}

{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}

{\out  1. [| A; ~ P; R; ~ P; R |] ==> B}

{\out  2. [| B; ~ P; ~ R; ~ P; ~ R |] ==> A}

{\out  3. [| ~ P; R; B; ~ P; R |] ==> A}

{\out  4. [| ~ P; ~ R; A; ~ B; ~ P |] ==> R}

\end{ttbox}

Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false

while~$R$ and~$A$ are true.  This truth assignment reduces the main goal to

$true\bimp false$, which is of course invalid.

We can repeat this analysis by expanding definitions, using just

the rules of {\FOL}:

\begin{ttbox}

choplev 0;

{\out Level 0}

{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}

{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}

\ttbreak

by (rewtac if_def);

{\out Level 1}

{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}

{\out  1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}

{\out     P & (Q & A | ~ Q & B) | ~ P & (R & B | ~ R & A)}

by (blast_tac FOL_cs 1);

{\out by: tactic failed}

\end{ttbox}

Again we apply \ttindex{step_tac}:

\begin{ttbox}

by (REPEAT (step_tac FOL_cs 1));

{\out Level 2}

{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}

{\out  1. [| A; ~ P; R; ~ P; R; ~ False |] ==> B}

{\out  2. [| A; ~ P; R; R; ~ False; ~ B; ~ B |] ==> Q}

{\out  3. [| B; ~ P; ~ R; ~ P; ~ A |] ==> R}

{\out  4. [| B; ~ P; ~ R; ~ Q; ~ A |] ==> R}

{\out  5. [| B; ~ R; ~ P; ~ A; ~ R; Q; ~ False |] ==> A}

{\out  6. [| ~ P; R; B; ~ P; R; ~ False |] ==> A}

{\out  7. [| ~ P; ~ R; A; ~ B; ~ R |] ==> P}

{\out  8. [| ~ P; ~ R; A; ~ B; ~ R |] ==> Q}

\end{ttbox}

Subgoal~1 yields the same countermodel as before.  But each proof step has

taken six times as long, and the final result contains twice as many subgoals.

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