diff -r 7ceea59b4748 -r a45ae7b38672 doc-src/Logics/FOL.tex --- 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}. +\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} @@ -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|)}