Logics_ZF/document/FOL.tex

9 provided.  The intuitionistic prover works with derived rules to simplify
13 \section{Syntax and rules of inference}
24 Figure~\ref{fol-rules} shows the inference rules with their names.
27 $\conj$ and~$\imp$; introduction and elimination rules are derived for it.
35 Some intuitionistic derived rules are shown in
37 rules for the defined symbols $\neg$, $\bimp$ and $\exists!$.  Natural
39 reasoning, particularly with the destruction rules $(\conj E)$,
41 rules badly, so sequent-style rules are derived to eliminate conjunctions,
44 re-inserts the quantified formula for later use.  The rules
48 See the on-line theory library for complete listings of the rules and
49 derived rules.
117 \subcaption{Equality rules}
131 \subcaption{Propositional rules}
138 \subcaption{Quantifier rules}
147 \caption{Rules of intuitionistic logic} \label{fol-rules}
156 \subcaption{Derived equality rules}
171 \subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)}
177 \subcaption{Sequent-style elimination rules}
189 \caption{Derived rules for intuitionistic logic} \label{fol-int-derived}
222 Implication elimination (the rules~\isa{mp} and~\isa{impE}) pose
237 Instead, it simplifies implications using derived rules
240 The rules \tdx{conj_impE} and \tdx{disj_impE} are
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)
327 \caption{Derived rules for classical logic} \label{fol-cla-derived}
337 derives classical introduction rules for $\disj$ and~$\exists$, as well as
338 classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see
401 \(\exists y.\forall x. Q(x,y)\) using elimination rules:
453 the basic rules; the specialized rules help considerably.
469 and allows use of the special implication rules.
611 \section{Derived rules and the classical tactics}
620 Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$
627 elimination rules for~$\disj$ and~$\conj$.
652 The derivations of the introduction and elimination rules demonstrate the
680 The elimination rule has three premises, two of which are themselves rules.
699 \subsection{Using the derived rules}
700 Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural
706 Proofs also require the classical reasoning rules and the $\bimp$
709 To display the $if$-rules in action, let us analyse a proof step by step.
737 $if$-introduction can be applied.  Observe how the $if$-rules break down
759 reasoner, but first let us extend the default claset with the derived rules
775 \subsection{Derived rules versus definitions}
776 Dispensing with the derived rules, we can treat $if$ as an
797 using the derived rules for~\isa{if} run about six
798 times faster  than proofs using just the rules of first-order logic.
826 We can repeat this analysis by expanding definitions, using just the rules of
853 why the classical prover has been designed to accept derived rules.