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 \isa{logic}.
16 No types of individuals are provided, but extensions can define types such
17 as \isa{nat::term} and type constructors such as \isa{list::(term)term}
18 (see the examples directory, \texttt{FOL/ex}). Below, the type variable
19 $\alpha$ ranges over class \isa{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 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 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
45 \isa{conj\_impE}, etc., support the intuitionistic proof procedure
46 (see~\S\ref{fol-int-prover}).
48 See the on-line theory library for complete listings of the rules and
54 \it name &\it meta-type & \it description \\
55 \cdx{Trueprop}& $o\To prop$ & coercion to $prop$\\
56 \cdx{Not} & $o\To o$ & negation ($\neg$) \\
57 \cdx{True} & $o$ & tautology ($\top$) \\
58 \cdx{False} & $o$ & absurdity ($\bot$)
61 \subcaption{Constants}
64 \begin{tabular}{llrrr}
65 \it symbol &\it name &\it meta-type & \it priority & \it description \\
66 \sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 &
67 universal quantifier ($\forall$) \\
68 \sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 &
69 existential quantifier ($\exists$) \\
70 \isa{EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 &
71 unique existence ($\exists!$)
73 \index{*"E"X"! symbol}
79 \index{&@{\tt\&} symbol}
81 \index{*"-"-"> symbol}
82 \index{*"<"-"> symbol}
84 \it symbol & \it meta-type & \it priority & \it description \\
85 \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\
86 \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\
87 \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\
88 \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\
89 \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$)
96 formula & = & \hbox{expression of type~$o$} \\
97 & | & term " = " term \quad| \quad term " \ttilde= " term \\
98 & | & "\ttilde\ " formula \\
99 & | & formula " \& " formula \\
100 & | & formula " | " formula \\
101 & | & formula " --> " formula \\
102 & | & formula " <-> " formula \\
103 & | & "ALL~" id~id^* " . " formula \\
104 & | & "EX~~" id~id^* " . " formula \\
105 & | & "EX!~" id~id^* " . " formula
109 \caption{Syntax of \texttt{FOL}} \label{fol-syntax}
116 \tdx{subst} [| a=b; P(a) |] ==> P(b)
117 \subcaption{Equality rules}
119 \tdx{conjI} [| P; Q |] ==> P&Q
120 \tdx{conjunct1} P&Q ==> P
121 \tdx{conjunct2} P&Q ==> Q
123 \tdx{disjI1} P ==> P|Q
124 \tdx{disjI2} Q ==> P|Q
125 \tdx{disjE} [| P|Q; P ==> R; Q ==> R |] ==> R
127 \tdx{impI} (P ==> Q) ==> P-->Q
128 \tdx{mp} [| P-->Q; P |] ==> Q
130 \tdx{FalseE} False ==> P
131 \subcaption{Propositional rules}
133 \tdx{allI} (!!x. P(x)) ==> (ALL x.P(x))
134 \tdx{spec} (ALL x.P(x)) ==> P(x)
136 \tdx{exI} P(x) ==> (EX x.P(x))
137 \tdx{exE} [| EX x.P(x); !!x. P(x) ==> R |] ==> R
138 \subcaption{Quantifier rules}
140 \tdx{True_def} True == False-->False
141 \tdx{not_def} ~P == P-->False
142 \tdx{iff_def} P<->Q == (P-->Q) & (Q-->P)
143 \tdx{ex1_def} EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)
144 \subcaption{Definitions}
147 \caption{Rules of intuitionistic logic} \label{fol-rules}
153 \tdx{sym} a=b ==> b=a
154 \tdx{trans} [| a=b; b=c |] ==> a=c
155 \tdx{ssubst} [| b=a; P(a) |] ==> P(b)
156 \subcaption{Derived equality rules}
160 \tdx{notI} (P ==> False) ==> ~P
161 \tdx{notE} [| ~P; P |] ==> R
163 \tdx{iffI} [| P ==> Q; Q ==> P |] ==> P<->Q
164 \tdx{iffE} [| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R
165 \tdx{iffD1} [| P <-> Q; P |] ==> Q
166 \tdx{iffD2} [| P <-> Q; Q |] ==> P
168 \tdx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)
169 \tdx{ex1E} [| EX! x.P(x); !!x.[| P(x); ALL y. P(y) --> y=x |] ==> R
171 \subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)}
173 \tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
174 \tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
175 \tdx{allE} [| ALL x.P(x); P(x) ==> R |] ==> R
176 \tdx{all_dupE} [| ALL x.P(x); [| P(x); ALL x.P(x) |] ==> R |] ==> R
177 \subcaption{Sequent-style elimination rules}
179 \tdx{conj_impE} [| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R
180 \tdx{disj_impE} [| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R
181 \tdx{imp_impE} [| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R
182 \tdx{not_impE} [| ~P --> S; P ==> False; S ==> R |] ==> R
183 \tdx{iff_impE} [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P;
185 \tdx{all_impE} [| (ALL x.P(x))-->S; !!x.P(x); S ==> R |] ==> R
186 \tdx{ex_impE} [| (EX x.P(x))-->S; P(a)-->S ==> R |] ==> R
188 \subcaption{Intuitionistic simplification of implication}
189 \caption{Derived rules for intuitionistic logic} \label{fol-int-derived}
193 \section{Generic packages}
194 FOL instantiates most of Isabelle's generic packages.
197 It instantiates the simplifier, which is invoked through the method
198 \isa{simp}. Both equality ($=$) and the biconditional
199 ($\bimp$) may be used for rewriting.
202 It instantiates the classical reasoner, which is invoked mainly through the
203 methods \isa{blast} and \isa{auto}. See~\S\ref{fol-cla-prover}
206 %\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for
207 % an equality throughout a subgoal and its hypotheses. This tactic uses FOL's
208 % general substitution rule.
211 \begin{warn}\index{simplification!of conjunctions}%
212 Simplifying $a=b\conj P(a)$ to $a=b\conj P(b)$ is often advantageous. The
213 left part of a conjunction helps in simplifying the right part. This effect
214 is not available by default: it can be slow. It can be obtained by
215 including the theorem \isa{conj_cong}\index{*conj_cong (rule)}%
216 as a congruence rule in
217 simplification, \isa{simp cong:\ conj\_cong}.
221 \section{Intuitionistic proof procedures} \label{fol-int-prover}
222 Implication elimination (the rules~\isa{mp} and~\isa{impE}) pose
223 difficulties for automated proof. In intuitionistic logic, the assumption
224 $P\imp Q$ cannot be treated like $\neg P\disj Q$. Given $P\imp Q$, we may
225 use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated
226 use of $P\imp Q$. If the proof of~$P$ fails then the whole branch of the
227 proof must be abandoned. Thus intuitionistic propositional logic requires
230 For an elementary example, consider the intuitionistic proof of $Q$ from
231 $P\imp Q$ and $(P\imp Q)\imp P$. The implication $P\imp Q$ is needed
233 \[ \infer[({\imp}E)]{Q}{P\imp Q &
234 \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}}
236 The theorem prover for intuitionistic logic does not use~\isa{impE}.\@
237 Instead, it simplifies implications using derived rules
238 (Fig.\ts\ref{fol-int-derived}). It reduces the antecedents of implications
239 to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$.
240 The rules \tdx{conj_impE} and \tdx{disj_impE} are
241 straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and
242 $(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp
243 S$. The other \ldots\isa{\_impE} rules are unsafe; the method requires
244 backtracking. All the rules are derived in the same simple manner.
246 Dyckhoff has independently discovered similar rules, and (more importantly)
247 has demonstrated their completeness for propositional
248 logic~\cite{dyckhoff}. However, the tactics given below are not complete
249 for first-order logic because they discard universally quantified
250 assumptions after a single use. These are \ML{} functions, and are listed
251 below with their \ML{} type:
253 mp_tac : int -> tactic
254 eq_mp_tac : int -> tactic
255 IntPr.safe_step_tac : int -> tactic
256 IntPr.safe_tac : tactic
257 IntPr.inst_step_tac : int -> tactic
258 IntPr.step_tac : int -> tactic
259 IntPr.fast_tac : int -> tactic
260 IntPr.best_tac : int -> tactic
262 Most of these belong to the structure \ML{} \texttt{IntPr} and resemble the
263 tactics of Isabelle's classical reasoner. Note that you can use the
264 \isa{tactic} method to call \ML{} tactics in an Isar script:
266 \isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*})
268 Here is a description of each tactic:
270 \begin{ttdescription}
271 \item[\ttindexbold{mp_tac} {\it i}]
272 attempts to use \tdx{notE} or \tdx{impE} within the assumptions in
273 subgoal $i$. For each assumption of the form $\neg P$ or $P\imp Q$, it
274 searches for another assumption unifiable with~$P$. By
275 contradiction with $\neg P$ it can solve the subgoal completely; by Modus
276 Ponens it can replace the assumption $P\imp Q$ by $Q$. The tactic can
277 produce multiple outcomes, enumerating all suitable pairs of assumptions.
279 \item[\ttindexbold{eq_mp_tac} {\it i}]
280 is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
283 \item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on
284 subgoal~$i$. This may include proof by assumption or Modus Ponens (taking
285 care not to instantiate unknowns), or \texttt{hyp_subst_tac}.
287 \item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all
288 subgoals. It is deterministic, with at most one outcome.
290 \item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac},
291 but allows unknowns to be instantiated.
293 \item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt
294 inst_step_tac}, or applies an unsafe rule. This is the basic step of
295 the intuitionistic proof procedure.
297 \item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using
298 depth-first search, to solve subgoal~$i$.
300 \item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using
301 best-first search (guided by the size of the proof state) to solve subgoal~$i$.
303 Here are some of the theorems that \texttt{IntPr.fast_tac} proves
304 automatically. The latter three date from {\it Principia Mathematica}
305 (*11.53, *11.55, *11.61)~\cite{principia}.
307 ~~P & ~~(P --> Q) --> ~~Q
308 (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))
309 (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))
310 (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))
317 \tdx{excluded_middle} ~P | P
319 \tdx{disjCI} (~Q ==> P) ==> P|Q
320 \tdx{exCI} (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)
321 \tdx{impCE} [| P-->Q; ~P ==> R; Q ==> R |] ==> R
322 \tdx{iffCE} [| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
323 \tdx{notnotD} ~~P ==> P
324 \tdx{swap} ~P ==> (~Q ==> P) ==> Q
326 \caption{Derived rules for classical logic} \label{fol-cla-derived}
330 \section{Classical proof procedures} \label{fol-cla-prover}
331 The classical theory, \thydx{FOL}, consists of intuitionistic logic plus
333 $$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$
335 Natural deduction in classical logic is not really all that natural. FOL
336 derives classical introduction rules for $\disj$ and~$\exists$, as well as
337 classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see
338 Fig.\ts\ref{fol-cla-derived}).
340 The classical reasoner is installed. The most useful methods are
341 \isa{blast} (pure classical reasoning) and \isa{auto} (classical reasoning
342 combined with simplification), but the full range of
343 methods is available, including \isa{clarify},
344 \isa{fast}, \isa{best} and \isa{force}.
346 \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
347 {Chap.\ts\ref{chap:classical}}
348 and the \emph{Tutorial}~\cite{isa-tutorial}
349 for more discussion of classical proof methods.
352 \section{An intuitionistic example}
353 Here is a session similar to one in {\em Logic and Computation}
354 \cite[pages~222--3]{paulson87}. Isabelle treats quantifiers differently
355 from {\sc lcf}-based theorem provers such as {\sc hol}.
357 The theory header must specify that we are working in intuitionistic
360 \isacommand{theory}\ IFOL\_examples\ =\ IFOL:
362 The proof begins by entering the goal, then applying the rule $({\imp}I)$.
364 \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline
365 \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
366 \isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
368 \isacommand{apply}\ (rule\ impI)\isanewline
369 \ 1.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
370 \isasymLongrightarrow \ \isasymforall x.\ \isasymexists y.\ Q(x,\ y)
372 Isabelle's output is shown as it would appear using Proof General.
373 In this example, we shall never have more than one subgoal. Applying
374 $({\imp}I)$ replaces~\isa{\isasymlongrightarrow}
375 by~\isa{\isasymLongrightarrow}, so that
376 \(\ex{y}\all{x}Q(x,y)\) becomes an assumption. We have the choice of
377 $({\exists}E)$ and $({\forall}I)$; let us try the latter.
379 \isacommand{apply}\ (rule\ allI)\isanewline
380 \ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
381 \isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)\hfill\((*)\)
383 Applying $({\forall}I)$ replaces the \isa{\isasymforall
384 x} (in ASCII, \isa{ALL~x}) by \isa{\isasymAnd x}
385 (or \isa{!!x}), replacing FOL's universal quantifier by Isabelle's
386 meta universal quantifier. The bound variable is a {\bf parameter} of
387 the subgoal. We now must choose between $({\exists}I)$ and
388 $({\exists}E)$. What happens if the wrong rule is chosen?
390 \isacommand{apply}\ (rule\ exI)\isanewline
391 \ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
392 \isasymLongrightarrow \ Q(x,\ ?y2(x))
394 The new subgoal~1 contains the function variable \isa{?y2}. Instantiating
395 \isa{?y2} can replace~\isa{?y2(x)} by a term containing~\isa{x}, even
396 though~\isa{x} is a bound variable. Now we analyse the assumption
397 \(\exists y.\forall x. Q(x,y)\) using elimination rules:
399 \isacommand{apply}\ (erule\ exE)\isanewline
400 \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ \isasymLongrightarrow \ Q(x,\ ?y2(x))
402 Applying $(\exists E)$ has produced the parameter \isa{y} and stripped the
403 existential quantifier from the assumption. But the subgoal is unprovable:
404 there is no way to unify \isa{?y2(x)} with the bound variable~\isa{y}.
405 Using Proof General, we can return to the critical point, marked
406 $(*)$ above. This time we apply $({\exists}E)$:
408 \isacommand{apply}\ (erule\ exE)\isanewline
409 \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\
410 \isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)
412 We now have two parameters and no scheme variables. Applying
413 $({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are
414 applied to those parameters. Parameters should be produced early, as this
415 example demonstrates.
417 \isacommand{apply}\ (rule\ exI)\isanewline
418 \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\
419 \isasymLongrightarrow \ Q(x,\ ?y3(x,\ y))
421 \isacommand{apply}\ (erule\ allE)\isanewline
422 \ 1.\ \isasymAnd x\ y.\ Q(?x4(x,\ y),\ y)\ \isasymLongrightarrow \
425 The subgoal has variables \isa{?y3} and \isa{?x4} applied to both
426 parameters. The obvious projection functions unify \isa{?x4(x,y)} with~\isa{
427 x} and \isa{?y3(x,y)} with~\isa{y}.
429 \isacommand{apply}\ assumption\isanewline
430 No\ subgoals!\isanewline
433 The theorem was proved in six method invocations, not counting the
434 abandoned ones. But proof checking is tedious, and the \ML{} tactic
435 \ttindex{IntPr.fast_tac} can prove the theorem in one step.
437 \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline
438 \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
439 \isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
441 \isacommand{by} (tactic {*IntPr.fast_tac 1*})\isanewline
446 \section{An example of intuitionistic negation}
447 The following example demonstrates the specialized forms of implication
448 elimination. Even propositional formulae can be difficult to prove from
449 the basic rules; the specialized rules help considerably.
451 Propositional examples are easy to invent. As Dummett notes~\cite[page
452 28]{dummett}, $\neg P$ is classically provable if and only if it is
453 intuitionistically provable; therefore, $P$ is classically provable if and
454 only if $\neg\neg P$ is intuitionistically provable.%
455 \footnote{This remark holds only for propositional logic, not if $P$ is
456 allowed to contain quantifiers.}
458 Proving $\neg\neg P$ intuitionistically is
459 much harder than proving~$P$ classically.
461 Our example is the double negation of the classical tautology $(P\imp
462 Q)\disj (Q\imp P)$. The first step is apply the
463 \isa{unfold} method, which expands
464 negations to implications using the definition $\neg P\equiv P\imp\bot$
465 and allows use of the special implication rules.
467 \isacommand{lemma}\ "\isachartilde \ \isachartilde \ ((P-->Q)\ |\ (Q-->P))"\isanewline
468 \ 1.\ \isasymnot \ \isasymnot \ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P))
470 \isacommand{apply}\ (unfold\ not\_def)\isanewline
471 \ 1.\ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False)\ \isasymlongrightarrow \ False%
473 The next step is a trivial use of $(\imp I)$.
475 \isacommand{apply}\ (rule\ impI)\isanewline
476 \ 1.\ (P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\ \isasymLongrightarrow \ False%
478 By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but
479 that formula is not a theorem of intuitionistic logic. Instead, we
480 apply the specialized implication rule \tdx{disj_impE}. It splits the
481 assumption into two assumptions, one for each disjunct.
483 \isacommand{apply}\ (erule\ disj\_impE)\isanewline
484 \ 1.\ \isasymlbrakk (P\ \isasymlongrightarrow \ Q)\ \isasymlongrightarrow \ False;\ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \
487 We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but
488 their negations are inconsistent. Applying \tdx{imp_impE} breaks down
489 the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new
490 assumptions~$P$ and~$\neg Q$.
492 \isacommand{apply}\ (erule\ imp\_impE)\isanewline
493 \ 1.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ P;\ Q\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
494 \ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \
497 Subgoal~2 holds trivially; let us ignore it and continue working on
498 subgoal~1. Thanks to the assumption~$P$, we could prove $Q\imp P$;
499 applying \tdx{imp_impE} is simpler.
501 \ \isacommand{apply}\ (erule\ imp\_impE)\isanewline
502 \ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ Q;\ P\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ P\isanewline
503 \ 2.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
504 \ 3.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ False%
506 The three subgoals are all trivial.
508 \isacommand{apply}\ assumption\ \isanewline
509 \ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\
510 False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
511 \ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\
512 \isasymlongrightarrow \ False;\ False\isasymrbrakk \
513 \isasymLongrightarrow \ False%
515 \isacommand{apply}\ (erule\ FalseE)+\isanewline
516 No\ subgoals!\isanewline
519 This proof is also trivial for the \ML{} tactic \isa{IntPr.fast_tac}.
522 \section{A classical example} \label{fol-cla-example}
523 To illustrate classical logic, we shall prove the theorem
524 $\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as
525 follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
526 $\all{x}P(x)$ is true. Either way the theorem holds. First, we must
527 work in a theory based on classical logic:
529 \isacommand{theory}\ FOL\_examples\ =\ FOL:
532 The formal proof does not conform in any obvious way to the sketch given
533 above. Its key step is its first rule, \tdx{exCI}, a classical
534 version of~$(\exists I)$ that allows multiple instantiation of the
537 \isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline
538 \ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)
540 \isacommand{apply}\ (rule\ exCI)\isanewline
541 \ 1.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ \isasymforall x.\ P(?a)\ \isasymlongrightarrow \ P(x)
543 We can either exhibit a term \isa{?a} to satisfy the conclusion of
544 subgoal~1, or produce a contradiction from the assumption. The next
547 \isacommand{apply}\ (rule\ allI)\isanewline
548 \ 1.\ \isasymAnd x.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ P(?a)\ \isasymlongrightarrow \ P(x)
550 \isacommand{apply}\ (rule\ impI)\isanewline
551 \ 1.\ \isasymAnd x.\ \isasymlbrakk \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x));\ P(?a)\isasymrbrakk \ \isasymLongrightarrow \ P(x)
553 By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
554 is equivalent to applying~$(\exists I)$ again.
556 \isacommand{apply}\ (erule\ allE)\isanewline
557 \ 1.\ \isasymAnd x.\ \isasymlbrakk P(?a);\ \isasymnot \ (\isasymforall xa.\ P(?y3(x))\ \isasymlongrightarrow \ P(xa))\isasymrbrakk \ \isasymLongrightarrow \ P(x)
559 In classical logic, a negated assumption is equivalent to a conclusion. To
560 get this effect, we create a swapped version of $(\forall I)$ and apply it
561 using \ttindex{erule}.
563 \isacommand{apply}\ (erule\ allI\ [THEN\ [2]\ swap])\isanewline
564 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x)\isasymrbrakk \ \isasymLongrightarrow \ P(?y3(x))\ \isasymlongrightarrow \ P(xa)
566 The operand of \isa{erule} above denotes the following theorem:
568 \ \ \ \ \isasymlbrakk \isasymnot \ (\isasymforall x.\ ?P1(x));\
569 \isasymAnd x.\ \isasymnot \ ?P\ \isasymLongrightarrow \
570 ?P1(x)\isasymrbrakk \
571 \isasymLongrightarrow \ ?P%
573 The previous conclusion, \isa{P(x)}, has become a negated assumption.
575 \isacommand{apply}\ (rule\ impI)\isanewline
576 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(xa)
578 The subgoal has three assumptions. We produce a contradiction between the
579 \index{assumptions!contradictory} assumptions~\isa{\isasymnot P(x)}
580 and~\isa{P(?y3(x))}. The proof never instantiates the
583 \isacommand{apply}\ (erule\ notE)\isanewline
584 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(x)
586 \isacommand{apply}\ assumption\isanewline
587 No\ subgoals!\isanewline
590 The civilised way to prove this theorem is using the
591 \methdx{blast} method, which automatically uses the classical form
592 of the rule~$(\exists I)$:
594 \isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline
595 \ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)
597 \isacommand{by}\ blast\isanewline
600 If this theorem seems counterintuitive, then perhaps you are an
601 intuitionist. In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$
602 requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$,
603 which we cannot do without further knowledge about~$P$.
606 \section{Derived rules and the classical tactics}
607 Classical first-order logic can be extended with the propositional
608 connective $if(P,Q,R)$, where
609 $$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$
610 Theorems about $if$ can be proved by treating this as an abbreviation,
611 replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals. But
612 this duplicates~$P$, causing an exponential blowup and an unreadable
613 formula. Introducing further abbreviations makes the problem worse.
615 Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$
616 directly, without reference to its definition. The simple identity
617 \[ if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R) \]
619 $if$-introduction rule should be
620 \[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}} \]
621 The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the
622 elimination rules for~$\disj$ and~$\conj$.
623 \[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}
624 & \infer*{S}{[\neg P,R]}}
626 Having made these plans, we get down to work with Isabelle. The theory of
627 classical logic, \texttt{FOL}, is extended with the constant
628 $if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the
631 \isacommand{theory}\ If\ =\ FOL:\isanewline
632 \isacommand{constdefs}\isanewline
633 \ \ if\ ::\ "[o,o,o]=>o"\isanewline
634 \ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R"
636 We create the file \texttt{If.thy} containing these declarations. (This file
637 is on directory \texttt{FOL/ex} in the Isabelle distribution.) Typing
641 loads that theory and sets it to be the current context.
644 \subsection{Deriving the introduction rule}
646 The derivations of the introduction and elimination rules demonstrate the
647 methods for rewriting with definitions. Classical reasoning is required,
648 so we use \isa{blast}.
650 The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,
651 concludes $if(P,Q,R)$. We propose this lemma and immediately simplify
652 using \isa{if\_def} to expand the definition of \isa{if} in the
655 \isacommand{lemma}\ ifI: "[|\ P\ ==>\ Q;\ \isachartilde P\ ==>\ R\
656 |]\ ==>\ if(P,Q,R)"\isanewline
657 \ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ Q,\ R)
659 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
660 \ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \
663 The rule's premises, although expressed using meta-level implication
664 (\isa{\isasymLongrightarrow}) are passed as ordinary implications to
667 \isacommand{apply}\ blast\isanewline
668 No\ subgoals!\isanewline
673 \subsection{Deriving the elimination rule}
674 The elimination rule has three premises, two of which are themselves rules.
675 The conclusion is simply $S$.
677 \isacommand{lemma}\ ifE:\isanewline
678 \ \ \ "[|\ if(P,Q,R);\ \ [|P;\ Q|]\ ==>\ S;\ [|\isachartilde P;\ R|]\ ==>\ S\ |]\ ==>\ S"\isanewline
679 \ 1.\ \isasymlbrakk if(P,\ Q,\ R);\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S%
681 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
682 \ 1.\ \isasymlbrakk P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R;\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S%
684 The proof script is the same as before: \isa{simp} followed by
687 \isacommand{apply}\ blast\isanewline
688 No\ subgoals!\isanewline
693 \subsection{Using the derived rules}
694 Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural
695 proofs of theorems such as the following:
697 if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\
698 if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B))
700 Proofs also require the classical reasoning rules and the $\bimp$
701 introduction rule (called~\tdx{iffI}: do not confuse with~\isa{ifI}).
703 To display the $if$-rules in action, let us analyse a proof step by step.
705 \isacommand{lemma}\ if\_commute:\isanewline
706 \ \ \ \ \ "if(P,\ if(Q,A,B),\
707 if(Q,C,D))\ <->\ if(Q,\ if(P,A,C),\ if(P,B,D))"\isanewline
708 \isacommand{apply}\ (rule\ iffI)\isanewline
709 \ 1.\ if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))\ \isasymLongrightarrow \isanewline
710 \isaindent{\ 1.\ }if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
711 \ 2.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
712 \isaindent{\ 2.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
714 The $if$-elimination rule can be applied twice in succession.
716 \isacommand{apply}\ (erule\ ifE)\isanewline
717 \ 1.\ \isasymlbrakk P;\ if(Q,\ A,\ B)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
718 \ 2.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
719 \ 3.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
720 \isaindent{\ 3.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
722 \isacommand{apply}\ (erule\ ifE)\isanewline
723 \ 1.\ \isasymlbrakk P;\ Q;\ A\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
724 \ 2.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
725 \ 3.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
726 \ 4.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
727 \isaindent{\ 4.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
730 In the first two subgoals, all assumptions have been reduced to atoms. Now
731 $if$-introduction can be applied. Observe how the $if$-rules break down
732 occurrences of $if$ when they become the outermost connective.
734 \isacommand{apply}\ (rule\ ifI)\isanewline
735 \ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ A,\ C)\isanewline
736 \ 2.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline
737 \ 3.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
738 \ 4.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
739 \ 5.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
740 \isaindent{\ 5.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
742 \isacommand{apply}\ (rule\ ifI)\isanewline
743 \ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
744 \ 2.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ C\isanewline
745 \ 3.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline
746 \ 4.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
747 \ 5.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
748 \ 6.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
749 \isaindent{\ 6.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
751 Where do we stand? The first subgoal holds by assumption; the second and
752 third, by contradiction. This is getting tedious. We could use the classical
753 reasoner, but first let us extend the default claset with the derived rules
756 \isacommand{declare}\ ifI\ [intro!]\isanewline
757 \isacommand{declare}\ ifE\ [elim!]
759 With these declarations, we could have proved this theorem with a single
760 call to \isa{blast}. Here is another example:
762 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline
763 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B))
765 \isacommand{by}\ blast
769 \subsection{Derived rules versus definitions}
770 Dispensing with the derived rules, we can treat $if$ as an
771 abbreviation, and let \ttindex{blast_tac} prove the expanded formula. Let
772 us redo the previous proof:
774 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline
775 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B))
777 This time, we simply unfold using the definition of $if$:
779 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
780 \ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline
781 \isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ A\ \isasymor \ \isasymnot \ R\ \isasymand \ B)
783 We are left with a subgoal in pure first-order logic, and it falls to
786 \isacommand{apply}\ blast\isanewline
789 Expanding definitions reduces the extended logic to the base logic. This
790 approach has its merits, but it can be slow. In these examples, proofs
791 using the derived rules for~\isa{if} run about six
792 times faster than proofs using just the rules of first-order logic.
794 Expanding definitions can also make it harder to diagnose errors.
795 Suppose we are having difficulties in proving some goal. If by expanding
796 definitions we have made it unreadable, then we have little hope of
797 diagnosing the problem.
799 Attempts at program verification often yield invalid assertions.
800 Let us try to prove one:
802 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline
803 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\
806 Calling \isa{blast} yields an uninformative failure message. We can
807 get a closer look at the situation by applying \methdx{auto}.
809 \isacommand{apply}\ auto\isanewline
810 \ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline
811 \ 2.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
812 \ 3.\ \isasymlbrakk B;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
813 \ 4.\ \isasymlbrakk \isasymnot \ R;\ A;\ \isasymnot \ B;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \
816 Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false
817 while~$R$ and~$A$ are true. This truth assignment reduces the main goal to
818 $true\bimp false$, which is of course invalid.
820 We can repeat this analysis by expanding definitions, using just the rules of
823 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline
824 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\
827 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
828 \ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline
829 \isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ B\ \isasymor \ \isasymnot \ R\ \isasymand \ A)
831 Again \isa{blast} would fail, so we try \methdx{auto}:
833 \isacommand{apply}\ (auto)\ \isanewline
834 \ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline
835 \ 2.\ \isasymlbrakk A;\ \isasymnot \ P;\ R;\ \isasymnot \ B\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
836 \ 3.\ \isasymlbrakk B;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
837 \ 4.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ A;\ \isasymnot \ R;\ Q\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
838 \ 5.\ \isasymlbrakk B;\ \isasymnot \ Q;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
839 \ 6.\ \isasymlbrakk B;\ \isasymnot \ A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
840 \ 7.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
841 \ 8.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ Q%
843 Subgoal~1 yields the same countermodel as before. But each proof step has
844 taken six times as long, and the final result contains twice as many subgoals.
846 Expanding your definitions usually makes proofs more difficult. This is
847 why the classical prover has been designed to accept derived rules.
849 \index{first-order logic|)}