Logics_ZF/document/FOL.tex

5 Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc
13 \section{Syntax and rules of inference}
15 first-order terms is called \cldx{term} and is a subclass of \isa{logic}.
17 as \isa{nat::term} and type constructors such as \isa{list::(term)term}
19 $\alpha$ ranges over class \isa{term}; the equality symbol and quantifiers
27 $\conj$ and~$\imp$; introduction and elimination rules are derived for it.
30 of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
37 rules for the defined symbols $\neg$, $\bimp$ and $\exists!$.  Natural
38 deduction typically involves a combination of forward and backward
40 $({\imp}E)$, and~$(\forall E)$.  Isabelle's backward style handles these
42 implications, and universal quantifiers.  Used with elim-resolution,
48 See the on-line theory library for complete listings of the rules and
171 \subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)}
198 \isa{simp}.  Both equality ($=$) and the biconditional
203 methods \isa{blast} and \isa{auto}.  See~\S\ref{fol-cla-prover}
207 %  an equality throughout a subgoal and its hypotheses.  This tactic uses FOL's
222 Implication elimination (the rules~\isa{mp} and~\isa{impE}) pose
231 $P\imp Q$ and $(P\imp Q)\imp P$.  The implication $P\imp Q$ is needed
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
246 Dyckhoff has independently discovered similar rules, and (more importantly)
250 assumptions after a single use. These are \ML{} functions, and are listed
262 Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the
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
342 \isa{blast} (pure classical reasoning) and \isa{auto} (classical reasoning
345 \isa{fast}, \isa{best} and \isa{force}.
349 and the \emph{Tutorial}~\cite{isa-tutorial}
354 Here is a session similar to one in the book {\em Logic and Computation}
381 $({\exists}E)$ and $({\forall}I)$; let us try the latter.
391 the subgoal.  We now must choose between $({\exists}I)$ and
406 Applying $(\exists E)$ has produced the parameter \isa{y} and stripped the
416 We now have two parameters and no scheme variables.  Applying
417 $({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are
429 The subgoal has variables \isa{?y3} and \isa{?x4} applied to both
431 x} and \isa{?y3(x,y)} with~\isa{y}.
438 abandoned ones.  But proof checking is tedious, and the \ML{} tactic
456 28]{dummett}, $\neg P$ is classically provable if and only if it is
457 intuitionistically provable;  therefore, $P$ is classically provable if and
469 and allows use of the special implication rules.
494 assumptions~$P$ and~$\neg Q$.
501 Subgoal~2 holds trivially; let us ignore it and continue working on
558 By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
565 get this effect, we create a swapped version of $(\forall I)$ and apply it
585 and~\isa{P(?y3(x))}.   The proof never instantiates the
611 \section{Derived rules and the classical tactics}
617 this duplicates~$P$, causing an exponential blowup and an unreadable
620 Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$
626 The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the
627 elimination rules for~$\disj$ and~$\conj$.
647 loads that theory and sets it to be the current context.
652 The derivations of the introduction and elimination rules demonstrate the
656 The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,
657 concludes $if(P,Q,R)$.  We propose this lemma and immediately simplify
700 Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural
706 Proofs also require the classical reasoning rules and the $\bimp$
757 Where do we stand?  The first subgoal holds by assumption; the second and
777 abbreviation, and let \ttindex{blast_tac} prove the expanded formula.  Let
789 We are left with a subgoal in pure first-order logic, and it falls to
822 Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false
823 while~$R$ and~$A$ are true.  This truth assignment reduces the main goal to
850 taken six times as long, and the final result contains twice as many subgoals.