doc-src/ZF/FOL.tex
 changeset 30099 dde11464969c parent 14158 15bab630ae31 child 43077 7d69154d824b
equal inserted replaced
29960:9d5c6f376768 30099:dde11464969c
     1 %% $Id$
     1 %!TEX root = logics-ZF.tex
     2 \chapter{First-Order Logic}
     2 \chapter{First-Order Logic}
     3 \index{first-order logic|(}
     3 \index{first-order logic|(}
     4
     4
     5 Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc
     5 Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc
     6   nk}.  Intuitionistic first-order logic is defined first, as theory
     6   nk}.  Intuitionistic first-order logic is defined first, as theory
   358
   358
   359 The theory header specifies that we are working in intuitionistic
   359 The theory header specifies that we are working in intuitionistic
   360 logic by designating \isa{IFOL} rather than \isa{FOL} as the parent
   360 logic by designating \isa{IFOL} rather than \isa{FOL} as the parent
   361 theory:
   361 theory:
   362 \begin{isabelle}
   362 \begin{isabelle}
   363 \isacommand{theory}\ IFOL\_examples\ =\ IFOL:
   363 \isacommand{theory}\ IFOL\_examples\ \isacommand{imports}\ IFOL\isanewline

   364 \isacommand{begin}
   364 \end{isabelle}
   365 \end{isabelle}
   365 The proof begins by entering the goal, then applying the rule $({\imp}I)$.
   366 The proof begins by entering the goal, then applying the rule $({\imp}I)$.
   366 \begin{isabelle}
   367 \begin{isabelle}
   367 \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline
   368 \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline
   368 \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
   369 \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
   439 \begin{isabelle}
   440 \begin{isabelle}
   440 \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline
   441 \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline
   441 \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
   442 \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
   442 \isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
   443 \isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
   443 \isanewline
   444 \isanewline
   444 \isacommand{by} (tactic {*IntPr.fast_tac 1*})\isanewline
   445 \isacommand{by} (tactic \ttlbrace*IntPr.fast_tac 1*\ttrbrace)\isanewline
   445 No\ subgoals!
   446 No\ subgoals!
   446 \end{isabelle}
   447 \end{isabelle}
   447
   448
   448
   449
   449 \section{An example of intuitionistic negation}
   450 \section{An example of intuitionistic negation}
   527 $\ex{y}\all{x}P(y)\imp P(x)$.  Informally, the theorem can be proved as
   528 $\ex{y}\all{x}P(y)\imp P(x)$.  Informally, the theorem can be proved as
   528 follows.  Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
   529 follows.  Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
   529 $\all{x}P(x)$ is true.  Either way the theorem holds.  First, we must
   530 $\all{x}P(x)$ is true.  Either way the theorem holds.  First, we must
   530 work in a theory based on classical logic, the theory \isa{FOL}:
   531 work in a theory based on classical logic, the theory \isa{FOL}:
   531 \begin{isabelle}
   532 \begin{isabelle}
   532 \isacommand{theory}\ FOL\_examples\ =\ FOL:
   533 \isacommand{theory}\ FOL\_examples\ \isacommand{imports}\ FOL\isanewline

   534 \isacommand{begin}
   533 \end{isabelle}
   535 \end{isabelle}
   534
   536
   535 The formal proof does not conform in any obvious way to the sketch given
   537 The formal proof does not conform in any obvious way to the sketch given
   536 above.  Its key step is its first rule, \tdx{exCI}, a classical
   538 above.  Its key step is its first rule, \tdx{exCI}, a classical
   537 version of~$(\exists I)$ that allows multiple instantiation of the
   539 version of~$(\exists I)$ that allows multiple instantiation of the
   629 Having made these plans, we get down to work with Isabelle.  The theory of
   631 Having made these plans, we get down to work with Isabelle.  The theory of
   630 classical logic, \texttt{FOL}, is extended with the constant
   632 classical logic, \texttt{FOL}, is extended with the constant
   631 $if::[o,o,o]\To o$.  The axiom \tdx{if_def} asserts the
   633 $if::[o,o,o]\To o$.  The axiom \tdx{if_def} asserts the
   632 equation~$(if)$.
   634 equation~$(if)$.
   633 \begin{isabelle}
   635 \begin{isabelle}
   634 \isacommand{theory}\ If\ =\ FOL:\isanewline
   636 \isacommand{theory}\ If\ \isacommand{imports}\ FOL\isanewline

   637 \isacommand{begin}\isanewline
   635 \isacommand{constdefs}\isanewline
   638 \isacommand{constdefs}\isanewline
   636 \ \ if\ ::\ "[o,o,o]=>o"\isanewline
   639 \ \ if\ ::\ "[o,o,o]=>o"\isanewline
   637 \ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R"
   640 \ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R"
   638 \end{isabelle}
   641 \end{isabelle}
   639 We create the file \texttt{If.thy} containing these declarations.  (This file
   642 We create the file \texttt{If.thy} containing these declarations.  (This file