2 \chapter{First-Order Logic}
3 \index{first-order logic|(}
5 Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc
6 nk}. Intuitionistic first-order logic is defined first, as theory
7 \thydx{IFOL}. Classical logic, theory \thydx{FOL}, is
8 obtained by adding the double negation rule. Basic proof procedures are
9 provided. The intuitionistic prover works with derived rules to simplify
10 implications in the assumptions. Classical~\texttt{FOL} employs Isabelle's
11 classical reasoner, which simulates a sequent calculus.
13 \section{Syntax and rules of inference}
14 The logic is many-sorted, using Isabelle's type classes. The class of
15 first-order terms is called \cldx{term} and is a subclass of \texttt{logic}.
16 No types of individuals are provided, but extensions can define types such
17 as \texttt{nat::term} and type constructors such as \texttt{list::(term)term}
18 (see the examples directory, \texttt{FOL/ex}). Below, the type variable
19 $\alpha$ ranges over class \texttt{term}; the equality symbol and quantifiers
20 are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which
21 belongs to class~\cldx{logic}. Figure~\ref{fol-syntax} gives the syntax.
22 Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$.
24 Figure~\ref{fol-rules} shows the inference rules with their~\ML\ names.
25 Negation is defined in the usual way for intuitionistic logic; $\neg P$
26 abbreviates $P\imp\bot$. The biconditional~($\bimp$) is defined through
27 $\conj$ and~$\imp$; introduction and elimination rules are derived for it.
29 The unique existence quantifier, $\exists!x.P(x)$, is defined in terms
30 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
31 quantifications. For instance, $\exists!x\;y.P(x,y)$ abbreviates
32 $\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
33 exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
35 Some intuitionistic derived rules are shown in
36 Fig.\ts\ref{fol-int-derived}, again with their \ML\ names. These include
37 rules for the defined symbols $\neg$, $\bimp$ and $\exists!$. Natural
38 deduction typically involves a combination of forward and backward
39 reasoning, particularly with the destruction rules $(\conj E)$,
40 $({\imp}E)$, and~$(\forall E)$. Isabelle's backward style handles these
41 rules badly, so sequent-style rules are derived to eliminate conjunctions,
42 implications, and universal quantifiers. Used with elim-resolution,
43 \tdx{allE} eliminates a universal quantifier while \tdx{all_dupE}
44 re-inserts the quantified formula for later use. The rules {\tt
45 conj_impE}, etc., support the intuitionistic proof procedure
46 (see~\S\ref{fol-int-prover}).
48 See the files \texttt{FOL/IFOL.thy}, \texttt{FOL/IFOL.ML} and
49 \texttt{FOL/intprover.ML} for complete listings of the rules and
55 \it name &\it meta-type & \it description \\
56 \cdx{Trueprop}& $o\To prop$ & coercion to $prop$\\
57 \cdx{Not} & $o\To o$ & negation ($\neg$) \\
58 \cdx{True} & $o$ & tautology ($\top$) \\
59 \cdx{False} & $o$ & absurdity ($\bot$)
62 \subcaption{Constants}
65 \begin{tabular}{llrrr}
66 \it symbol &\it name &\it meta-type & \it priority & \it description \\
67 \sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 &
68 universal quantifier ($\forall$) \\
69 \sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 &
70 existential quantifier ($\exists$) \\
71 \texttt{EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 &
72 unique existence ($\exists!$)
74 \index{*"E"X"! symbol}
80 \index{&@{\tt\&} symbol}
82 \index{*"-"-"> symbol}
83 \index{*"<"-"> symbol}
85 \it symbol & \it meta-type & \it priority & \it description \\
86 \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\
87 \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\
88 \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\
89 \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\
90 \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$)
97 formula & = & \hbox{expression of type~$o$} \\
98 & | & term " = " term \quad| \quad term " \ttilde= " term \\
99 & | & "\ttilde\ " formula \\
100 & | & formula " \& " formula \\
101 & | & formula " | " formula \\
102 & | & formula " --> " formula \\
103 & | & formula " <-> " formula \\
104 & | & "ALL~" id~id^* " . " formula \\
105 & | & "EX~~" id~id^* " . " formula \\
106 & | & "EX!~" id~id^* " . " formula
110 \caption{Syntax of \texttt{FOL}} \label{fol-syntax}
117 \tdx{subst} [| a=b; P(a) |] ==> P(b)
118 \subcaption{Equality rules}
120 \tdx{conjI} [| P; Q |] ==> P&Q
121 \tdx{conjunct1} P&Q ==> P
122 \tdx{conjunct2} P&Q ==> Q
124 \tdx{disjI1} P ==> P|Q
125 \tdx{disjI2} Q ==> P|Q
126 \tdx{disjE} [| P|Q; P ==> R; Q ==> R |] ==> R
128 \tdx{impI} (P ==> Q) ==> P-->Q
129 \tdx{mp} [| P-->Q; P |] ==> Q
131 \tdx{FalseE} False ==> P
132 \subcaption{Propositional rules}
134 \tdx{allI} (!!x. P(x)) ==> (ALL x.P(x))
135 \tdx{spec} (ALL x.P(x)) ==> P(x)
137 \tdx{exI} P(x) ==> (EX x.P(x))
138 \tdx{exE} [| EX x.P(x); !!x. P(x) ==> R |] ==> R
139 \subcaption{Quantifier rules}
141 \tdx{True_def} True == False-->False
142 \tdx{not_def} ~P == P-->False
143 \tdx{iff_def} P<->Q == (P-->Q) & (Q-->P)
144 \tdx{ex1_def} EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)
145 \subcaption{Definitions}
148 \caption{Rules of intuitionistic logic} \label{fol-rules}
154 \tdx{sym} a=b ==> b=a
155 \tdx{trans} [| a=b; b=c |] ==> a=c
156 \tdx{ssubst} [| b=a; P(a) |] ==> P(b)
157 \subcaption{Derived equality rules}
161 \tdx{notI} (P ==> False) ==> ~P
162 \tdx{notE} [| ~P; P |] ==> R
164 \tdx{iffI} [| P ==> Q; Q ==> P |] ==> P<->Q
165 \tdx{iffE} [| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R
166 \tdx{iffD1} [| P <-> Q; P |] ==> Q
167 \tdx{iffD2} [| P <-> Q; Q |] ==> P
169 \tdx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)
170 \tdx{ex1E} [| EX! x.P(x); !!x.[| P(x); ALL y. P(y) --> y=x |] ==> R
172 \subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)}
174 \tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
175 \tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
176 \tdx{allE} [| ALL x.P(x); P(x) ==> R |] ==> R
177 \tdx{all_dupE} [| ALL x.P(x); [| P(x); ALL x.P(x) |] ==> R |] ==> R
178 \subcaption{Sequent-style elimination rules}
180 \tdx{conj_impE} [| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R
181 \tdx{disj_impE} [| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R
182 \tdx{imp_impE} [| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R
183 \tdx{not_impE} [| ~P --> S; P ==> False; S ==> R |] ==> R
184 \tdx{iff_impE} [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P;
186 \tdx{all_impE} [| (ALL x.P(x))-->S; !!x.P(x); S ==> R |] ==> R
187 \tdx{ex_impE} [| (EX x.P(x))-->S; P(a)-->S ==> R |] ==> R
189 \subcaption{Intuitionistic simplification of implication}
190 \caption{Derived rules for intuitionistic logic} \label{fol-int-derived}
194 \section{Generic packages}
195 \FOL{} instantiates most of Isabelle's generic packages.
198 It instantiates the simplifier. Both equality ($=$) and the biconditional
199 ($\bimp$) may be used for rewriting. Tactics such as \texttt{Asm_simp_tac} and
200 \texttt{Full_simp_tac} refer to the default simpset (\texttt{simpset()}), which works for
201 most purposes. Named simplification sets include \ttindexbold{IFOL_ss},
202 for intuitionistic first-order logic, and \ttindexbold{FOL_ss},
203 for classical logic. See the file
204 \texttt{FOL/simpdata.ML} for a complete listing of the simplification
206 \iflabelundefined{sec:setting-up-simp}{}%
207 {, and \S\ref{sec:setting-up-simp} for discussion}.
210 It instantiates the classical reasoner. See~\S\ref{fol-cla-prover}
213 \item \FOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
214 for an equality throughout a subgoal and its hypotheses. This tactic uses
215 \FOL's general substitution rule.
218 \begin{warn}\index{simplification!of conjunctions}%
219 Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The
220 left part of a conjunction helps in simplifying the right part. This effect
221 is not available by default: it can be slow. It can be obtained by
222 including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
226 \section{Intuitionistic proof procedures} \label{fol-int-prover}
227 Implication elimination (the rules~\texttt{mp} and~\texttt{impE}) pose
228 difficulties for automated proof. In intuitionistic logic, the assumption
229 $P\imp Q$ cannot be treated like $\neg P\disj Q$. Given $P\imp Q$, we may
230 use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated
231 use of $P\imp Q$. If the proof of~$P$ fails then the whole branch of the
232 proof must be abandoned. Thus intuitionistic propositional logic requires
235 For an elementary example, consider the intuitionistic proof of $Q$ from
236 $P\imp Q$ and $(P\imp Q)\imp P$. The implication $P\imp Q$ is needed
238 \[ \infer[({\imp}E)]{Q}{P\imp Q &
239 \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}}
241 The theorem prover for intuitionistic logic does not use~\texttt{impE}.\@
242 Instead, it simplifies implications using derived rules
243 (Fig.\ts\ref{fol-int-derived}). It reduces the antecedents of implications
244 to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$.
245 The rules \tdx{conj_impE} and \tdx{disj_impE} are
246 straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and
247 $(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp
248 S$. The other \ldots{\tt_impE} rules are unsafe; the method requires
249 backtracking. All the rules are derived in the same simple manner.
251 Dyckhoff has independently discovered similar rules, and (more importantly)
252 has demonstrated their completeness for propositional
253 logic~\cite{dyckhoff}. However, the tactics given below are not complete
254 for first-order logic because they discard universally quantified
255 assumptions after a single use.
257 mp_tac : int -> tactic
258 eq_mp_tac : int -> tactic
259 IntPr.safe_step_tac : int -> tactic
260 IntPr.safe_tac : tactic
261 IntPr.inst_step_tac : int -> tactic
262 IntPr.step_tac : int -> tactic
263 IntPr.fast_tac : int -> tactic
264 IntPr.best_tac : int -> tactic
266 Most of these belong to the structure \texttt{IntPr} and resemble the
267 tactics of Isabelle's classical reasoner.
269 \begin{ttdescription}
270 \item[\ttindexbold{mp_tac} {\it i}]
271 attempts to use \tdx{notE} or \tdx{impE} within the assumptions in
272 subgoal $i$. For each assumption of the form $\neg P$ or $P\imp Q$, it
273 searches for another assumption unifiable with~$P$. By
274 contradiction with $\neg P$ it can solve the subgoal completely; by Modus
275 Ponens it can replace the assumption $P\imp Q$ by $Q$. The tactic can
276 produce multiple outcomes, enumerating all suitable pairs of assumptions.
278 \item[\ttindexbold{eq_mp_tac} {\it i}]
279 is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
282 \item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on
283 subgoal~$i$. This may include proof by assumption or Modus Ponens (taking
284 care not to instantiate unknowns), or \texttt{hyp_subst_tac}.
286 \item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all
287 subgoals. It is deterministic, with at most one outcome.
289 \item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac},
290 but allows unknowns to be instantiated.
292 \item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt
293 inst_step_tac}, or applies an unsafe rule. This is the basic step of
294 the intuitionistic proof procedure.
296 \item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using
297 depth-first search, to solve subgoal~$i$.
299 \item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using
300 best-first search (guided by the size of the proof state) to solve subgoal~$i$.
302 Here are some of the theorems that \texttt{IntPr.fast_tac} proves
303 automatically. The latter three date from {\it Principia Mathematica}
304 (*11.53, *11.55, *11.61)~\cite{principia}.
306 ~~P & ~~(P --> Q) --> ~~Q
307 (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))
308 (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))
309 (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))
316 \tdx{excluded_middle} ~P | P
318 \tdx{disjCI} (~Q ==> P) ==> P|Q
319 \tdx{exCI} (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)
320 \tdx{impCE} [| P-->Q; ~P ==> R; Q ==> R |] ==> R
321 \tdx{iffCE} [| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
322 \tdx{notnotD} ~~P ==> P
323 \tdx{swap} ~P ==> (~Q ==> P) ==> Q
325 \caption{Derived rules for classical logic} \label{fol-cla-derived}
329 \section{Classical proof procedures} \label{fol-cla-prover}
330 The classical theory, \thydx{FOL}, consists of intuitionistic logic plus
332 $$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$
334 Natural deduction in classical logic is not really all that natural.
335 {\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as
336 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
337 rule (see Fig.\ts\ref{fol-cla-derived}).
339 The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt
340 Best_tac} refer to the default claset (\texttt{claset()}), which works for most
341 purposes. Named clasets include \ttindexbold{prop_cs}, which includes the
342 propositional rules, and \ttindexbold{FOL_cs}, which also includes quantifier
343 rules. See the file \texttt{FOL/cladata.ML} for lists of the
345 \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
346 {Chap.\ts\ref{chap:classical}}
347 for more discussion of classical proof methods.
350 \section{An intuitionistic example}
351 Here is a session similar to one in {\em Logic and Computation}
352 \cite[pages~222--3]{paulson87}. Isabelle treats quantifiers differently
353 from {\sc lcf}-based theorem provers such as {\sc hol}.
355 First, we specify that we are working in intuitionistic logic:
359 The proof begins by entering the goal, then applying the rule $({\imp}I)$.
361 Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
363 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
364 {\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
366 by (resolve_tac [impI] 1);
368 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
369 {\out 1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)}
371 In this example, we shall never have more than one subgoal. Applying
372 $({\imp}I)$ replaces~\verb|-->| by~\verb|==>|, making
373 \(\ex{y}\all{x}Q(x,y)\) an assumption. We have the choice of
374 $({\exists}E)$ and $({\forall}I)$; let us try the latter.
376 by (resolve_tac [allI] 1);
378 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
379 {\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
381 Applying $({\forall}I)$ replaces the \texttt{ALL~x} by \hbox{\tt!!x},
382 changing the universal quantifier from object~($\forall$) to
383 meta~($\Forall$). The bound variable is a {\bf parameter} of the
384 subgoal. We now must choose between $({\exists}I)$ and $({\exists}E)$. What
385 happens if the wrong rule is chosen?
387 by (resolve_tac [exI] 1);
389 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
390 {\out 1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
392 The new subgoal~1 contains the function variable {\tt?y2}. Instantiating
393 {\tt?y2} can replace~{\tt?y2(x)} by a term containing~\texttt{x}, even
394 though~\texttt{x} is a bound variable. Now we analyse the assumption
395 \(\exists y.\forall x. Q(x,y)\) using elimination rules:
397 by (eresolve_tac [exE] 1);
399 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
400 {\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
402 Applying $(\exists E)$ has produced the parameter \texttt{y} and stripped the
403 existential quantifier from the assumption. But the subgoal is unprovable:
404 there is no way to unify \texttt{?y2(x)} with the bound variable~\texttt{y}.
405 Using \texttt{choplev} we can return to the critical point. This time we
406 apply $({\exists}E)$:
410 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
411 {\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
413 by (eresolve_tac [exE] 1);
415 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
416 {\out 1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
418 We now have two parameters and no scheme variables. Applying
419 $({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are
420 applied to those parameters. Parameters should be produced early, as this
421 example demonstrates.
423 by (resolve_tac [exI] 1);
425 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
426 {\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))}
428 by (eresolve_tac [allE] 1);
430 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
431 {\out 1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))}
433 The subgoal has variables \texttt{?y3} and \texttt{?x4} applied to both
434 parameters. The obvious projection functions unify {\tt?x4(x,y)} with~{\tt
435 x} and \verb|?y3(x,y)| with~\texttt{y}.
439 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
442 The theorem was proved in six tactic steps, not counting the abandoned
443 ones. But proof checking is tedious; \ttindex{IntPr.fast_tac} proves the
446 Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
448 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
449 {\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
450 by (IntPr.fast_tac 1);
452 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
457 \section{An example of intuitionistic negation}
458 The following example demonstrates the specialized forms of implication
459 elimination. Even propositional formulae can be difficult to prove from
460 the basic rules; the specialized rules help considerably.
462 Propositional examples are easy to invent. As Dummett notes~\cite[page
463 28]{dummett}, $\neg P$ is classically provable if and only if it is
464 intuitionistically provable; therefore, $P$ is classically provable if and
465 only if $\neg\neg P$ is intuitionistically provable.%
466 \footnote{Of course this holds only for propositional logic, not if $P$ is
467 allowed to contain quantifiers.} Proving $\neg\neg P$ intuitionistically is
468 much harder than proving~$P$ classically.
470 Our example is the double negation of the classical tautology $(P\imp
471 Q)\disj (Q\imp P)$. When stating the goal, we command Isabelle to expand
472 negations to implications using the definition $\neg P\equiv P\imp\bot$.
473 This allows use of the special implication rules.
475 Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
477 {\out ~ ~ ((P --> Q) | (Q --> P))}
478 {\out 1. ((P --> Q) | (Q --> P) --> False) --> False}
480 The first step is trivial.
482 by (resolve_tac [impI] 1);
484 {\out ~ ~ ((P --> Q) | (Q --> P))}
485 {\out 1. (P --> Q) | (Q --> P) --> False ==> False}
487 By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but
488 that formula is not a theorem of intuitionistic logic. Instead we apply
489 the specialized implication rule \tdx{disj_impE}. It splits the
490 assumption into two assumptions, one for each disjunct.
492 by (eresolve_tac [disj_impE] 1);
494 {\out ~ ~ ((P --> Q) | (Q --> P))}
495 {\out 1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False}
497 We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but
498 their negations are inconsistent. Applying \tdx{imp_impE} breaks down
499 the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new
500 assumptions~$P$ and~$\neg Q$.
502 by (eresolve_tac [imp_impE] 1);
504 {\out ~ ~ ((P --> Q) | (Q --> P))}
505 {\out 1. [| (Q --> P) --> False; P; Q --> False |] ==> Q}
506 {\out 2. [| (Q --> P) --> False; False |] ==> False}
508 Subgoal~2 holds trivially; let us ignore it and continue working on
509 subgoal~1. Thanks to the assumption~$P$, we could prove $Q\imp P$;
510 applying \tdx{imp_impE} is simpler.
512 by (eresolve_tac [imp_impE] 1);
514 {\out ~ ~ ((P --> Q) | (Q --> P))}
515 {\out 1. [| P; Q --> False; Q; P --> False |] ==> P}
516 {\out 2. [| P; Q --> False; False |] ==> Q}
517 {\out 3. [| (Q --> P) --> False; False |] ==> False}
519 The three subgoals are all trivial.
521 by (REPEAT (eresolve_tac [FalseE] 2));
523 {\out ~ ~ ((P --> Q) | (Q --> P))}
524 {\out 1. [| P; Q --> False; Q; P --> False |] ==> P}
528 {\out ~ ~ ((P --> Q) | (Q --> P))}
531 This proof is also trivial for \texttt{IntPr.fast_tac}.
534 \section{A classical example} \label{fol-cla-example}
535 To illustrate classical logic, we shall prove the theorem
536 $\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as
537 follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
538 $\all{x}P(x)$ is true. Either way the theorem holds. First, we switch to
544 The formal proof does not conform in any obvious way to the sketch given
545 above. The key inference is the first one, \tdx{exCI}; this classical
546 version of~$(\exists I)$ allows multiple instantiation of the quantifier.
548 Goal "EX y. ALL x. P(y)-->P(x)";
550 {\out EX y. ALL x. P(y) --> P(x)}
551 {\out 1. EX y. ALL x. P(y) --> P(x)}
553 by (resolve_tac [exCI] 1);
555 {\out EX y. ALL x. P(y) --> P(x)}
556 {\out 1. ALL y. ~ (ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)}
558 We can either exhibit a term {\tt?a} to satisfy the conclusion of
559 subgoal~1, or produce a contradiction from the assumption. The next
562 by (resolve_tac [allI] 1);
564 {\out EX y. ALL x. P(y) --> P(x)}
565 {\out 1. !!x. ALL y. ~ (ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)}
567 by (resolve_tac [impI] 1);
569 {\out EX y. ALL x. P(y) --> P(x)}
570 {\out 1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)}
572 By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
573 in effect applies~$(\exists I)$ again.
575 by (eresolve_tac [allE] 1);
577 {\out EX y. ALL x. P(y) --> P(x)}
578 {\out 1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
580 In classical logic, a negated assumption is equivalent to a conclusion. To
581 get this effect, we create a swapped version of~$(\forall I)$ and apply it
582 using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall
583 I)$ using \ttindex{swap_res_tac}.
586 {\out val it = "[| ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
587 by (eresolve_tac [it] 1);
589 {\out EX y. ALL x. P(y) --> P(x)}
590 {\out 1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)}
592 The previous conclusion, \texttt{P(x)}, has become a negated assumption.
594 by (resolve_tac [impI] 1);
596 {\out EX y. ALL x. P(y) --> P(x)}
597 {\out 1. !!x xa. [| P(?a); ~ P(x); P(?y3(x)) |] ==> P(xa)}
599 The subgoal has three assumptions. We produce a contradiction between the
600 \index{assumptions!contradictory} assumptions~\verb|~P(x)| and~{\tt
601 P(?y3(x))}. The proof never instantiates the unknown~{\tt?a}.
603 by (eresolve_tac [notE] 1);
605 {\out EX y. ALL x. P(y) --> P(x)}
606 {\out 1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)}
610 {\out EX y. ALL x. P(y) --> P(x)}
613 The civilised way to prove this theorem is through \ttindex{Blast_tac},
614 which automatically uses the classical version of~$(\exists I)$:
616 Goal "EX y. ALL x. P(y)-->P(x)";
618 {\out EX y. ALL x. P(y) --> P(x)}
619 {\out 1. EX y. ALL x. P(y) --> P(x)}
625 {\out EX y. ALL x. P(y) --> P(x)}
628 If this theorem seems counterintuitive, then perhaps you are an
629 intuitionist. In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$
630 requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$,
631 which we cannot do without further knowledge about~$P$.
634 \section{Derived rules and the classical tactics}
635 Classical first-order logic can be extended with the propositional
636 connective $if(P,Q,R)$, where
637 $$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$
638 Theorems about $if$ can be proved by treating this as an abbreviation,
639 replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals. But
640 this duplicates~$P$, causing an exponential blowup and an unreadable
641 formula. Introducing further abbreviations makes the problem worse.
643 Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$
644 directly, without reference to its definition. The simple identity
645 \[ if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R) \]
647 $if$-introduction rule should be
648 \[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}} \]
649 The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the
650 elimination rules for~$\disj$ and~$\conj$.
651 \[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}
652 & \infer*{S}{[\neg P,R]}}
654 Having made these plans, we get down to work with Isabelle. The theory of
655 classical logic, \texttt{FOL}, is extended with the constant
656 $if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the
660 consts if :: [o,o,o]=>o
661 rules if_def "if(P,Q,R) == P&Q | ~P&R"
664 We create the file \texttt{If.thy} containing these declarations. (This file
665 is on directory \texttt{FOL/ex} in the Isabelle distribution.) Typing
669 loads that theory and sets it to be the current context.
672 \subsection{Deriving the introduction rule}
674 The derivations of the introduction and elimination rules demonstrate the
675 methods for rewriting with definitions. Classical reasoning is required,
676 so we use \texttt{blast_tac}.
678 The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,
679 concludes $if(P,Q,R)$. We propose the conclusion as the main goal
680 using~\ttindex{Goalw}, which uses \texttt{if_def} to rewrite occurrences
681 of $if$ in the subgoal.
683 val prems = Goalw [if_def]
684 "[| P ==> Q; ~ P ==> R |] ==> if(P,Q,R)";
687 {\out 1. P & Q | ~ P & R}
689 The premises (bound to the {\ML} variable \texttt{prems}) are passed as
690 introduction rules to \ttindex{blast_tac}. Remember that \texttt{claset()} refers
691 to the default classical set.
693 by (blast_tac (claset() addIs prems) 1);
701 \subsection{Deriving the elimination rule}
702 The elimination rule has three premises, two of which are themselves rules.
703 The conclusion is simply $S$.
705 val major::prems = Goalw [if_def]
706 "[| if(P,Q,R); [| P; Q |] ==> S; [| ~ P; R |] ==> S |] ==> S";
711 The major premise contains an occurrence of~$if$, but the version returned
712 by \ttindex{Goalw} (and bound to the {\ML} variable~\texttt{major}) has the
713 definition expanded. Now \ttindex{cut_facts_tac} inserts~\texttt{major} as an
714 assumption in the subgoal, so that \ttindex{blast_tac} can break it down.
716 by (cut_facts_tac [major] 1);
719 {\out 1. P & Q | ~ P & R ==> S}
721 by (blast_tac (claset() addIs prems) 1);
727 As you may recall from
728 \iflabelundefined{definitions}{{\em Introduction to Isabelle}}%
729 {\S\ref{definitions}}, there are other
730 ways of treating definitions when deriving a rule. We can start the
731 proof using \texttt{Goal}, which does not expand definitions, instead of
732 \texttt{Goalw}. We can use \ttindex{rew_tac}
733 to expand definitions in the subgoals---perhaps after calling
734 \ttindex{cut_facts_tac} to insert the rule's premises. We can use
735 \ttindex{rewrite_rule}, which is a meta-inference rule, to expand
736 definitions in the premises directly.
739 \subsection{Using the derived rules}
740 The rules just derived have been saved with the {\ML} names \tdx{ifI}
741 and~\tdx{ifE}. They permit natural proofs of theorems such as the
744 if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\
745 if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B))
747 Proofs also require the classical reasoning rules and the $\bimp$
748 introduction rule (called~\tdx{iffI}: do not confuse with~\texttt{ifI}).
750 To display the $if$-rules in action, let us analyse a proof step by step.
752 Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
754 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
755 {\out 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
757 by (resolve_tac [iffI] 1);
759 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
760 {\out 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))}
761 {\out 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
763 The $if$-elimination rule can be applied twice in succession.
765 by (eresolve_tac [ifE] 1);
767 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
768 {\out 1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))}
769 {\out 2. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
770 {\out 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
772 by (eresolve_tac [ifE] 1);
774 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
775 {\out 1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))}
776 {\out 2. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
777 {\out 3. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
778 {\out 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
781 In the first two subgoals, all assumptions have been reduced to atoms. Now
782 $if$-introduction can be applied. Observe how the $if$-rules break down
783 occurrences of $if$ when they become the outermost connective.
785 by (resolve_tac [ifI] 1);
787 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
788 {\out 1. [| P; Q; A; Q |] ==> if(P,A,C)}
789 {\out 2. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
790 {\out 3. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
791 {\out 4. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
792 {\out 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
794 by (resolve_tac [ifI] 1);
796 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
797 {\out 1. [| P; Q; A; Q; P |] ==> A}
798 {\out 2. [| P; Q; A; Q; ~ P |] ==> C}
799 {\out 3. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
800 {\out 4. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
801 {\out 5. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
802 {\out 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
804 Where do we stand? The first subgoal holds by assumption; the second and
805 third, by contradiction. This is getting tedious. We could use the classical
806 reasoner, but first let us extend the default claset with the derived rules
812 Now we can revert to the
813 initial proof state and let \ttindex{blast_tac} solve it.
817 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
818 {\out 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
821 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
824 This tactic also solves the other example.
826 Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
828 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
829 {\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
833 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
838 \subsection{Derived rules versus definitions}
839 Dispensing with the derived rules, we can treat $if$ as an
840 abbreviation, and let \ttindex{blast_tac} prove the expanded formula. Let
841 us redo the previous proof:
845 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
846 {\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
848 This time, simply unfold using the definition of $if$:
852 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
853 {\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
854 {\out P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)}
856 We are left with a subgoal in pure first-order logic, which is why the
857 classical reasoner can prove it given \texttt{FOL_cs} alone. (We could, of
858 course, have used \texttt{Blast_tac}.)
860 by (blast_tac FOL_cs 1);
862 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
865 Expanding definitions reduces the extended logic to the base logic. This
866 approach has its merits --- especially if the prover for the base logic is
867 good --- but can be slow. In these examples, proofs using the default
868 claset (which includes the derived rules) run about six times faster
869 than proofs using \texttt{FOL_cs}.
871 Expanding definitions also complicates error diagnosis. Suppose we are having
872 difficulties in proving some goal. If by expanding definitions we have
873 made it unreadable, then we have little hope of diagnosing the problem.
875 Attempts at program verification often yield invalid assertions.
876 Let us try to prove one:
878 Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
880 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
881 {\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
883 {\out by: tactic failed}
885 This failure message is uninformative, but we can get a closer look at the
886 situation by applying \ttindex{Step_tac}.
888 by (REPEAT (Step_tac 1));
890 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
891 {\out 1. [| A; ~ P; R; ~ P; R |] ==> B}
892 {\out 2. [| B; ~ P; ~ R; ~ P; ~ R |] ==> A}
893 {\out 3. [| ~ P; R; B; ~ P; R |] ==> A}
894 {\out 4. [| ~ P; ~ R; A; ~ B; ~ P |] ==> R}
896 Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false
897 while~$R$ and~$A$ are true. This truth assignment reduces the main goal to
898 $true\bimp false$, which is of course invalid.
900 We can repeat this analysis by expanding definitions, using just
905 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
906 {\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
910 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
911 {\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
912 {\out P & (Q & A | ~ Q & B) | ~ P & (R & B | ~ R & A)}
913 by (blast_tac FOL_cs 1);
914 {\out by: tactic failed}
916 Again we apply \ttindex{step_tac}:
918 by (REPEAT (step_tac FOL_cs 1));
920 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
921 {\out 1. [| A; ~ P; R; ~ P; R; ~ False |] ==> B}
922 {\out 2. [| A; ~ P; R; R; ~ False; ~ B; ~ B |] ==> Q}
923 {\out 3. [| B; ~ P; ~ R; ~ P; ~ A |] ==> R}
924 {\out 4. [| B; ~ P; ~ R; ~ Q; ~ A |] ==> R}
925 {\out 5. [| B; ~ R; ~ P; ~ A; ~ R; Q; ~ False |] ==> A}
926 {\out 6. [| ~ P; R; B; ~ P; R; ~ False |] ==> A}
927 {\out 7. [| ~ P; ~ R; A; ~ B; ~ R |] ==> P}
928 {\out 8. [| ~ P; ~ R; A; ~ B; ~ R |] ==> Q}
930 Subgoal~1 yields the same countermodel as before. But each proof step has
931 taken six times as long, and the final result contains twice as many subgoals.
933 Expanding definitions causes a great increase in complexity. This is why
934 the classical prover has been designed to accept derived rules.
936 \index{first-order logic|)}