diff -r f40d61cd6b32 -r 5fe77b9b5185 doc-src/ZF/FOL.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/ZF/FOL.tex Wed Jan 13 16:36:36 1999 +0100 @@ -0,0 +1,936 @@ +%% $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|)}