doc-src/Logics/FOL.tex
 changeset 1388 7705e6211865 parent 874 2432820efbfe child 2495 82ec47e0a8d3
equal inserted replaced
   658 classical logic, {\tt FOL}, is extended with the constant
   658 classical logic, {\tt FOL}, is extended with the constant
   659 $if::[o,o,o]\To o$.  The axiom \tdx{if_def} asserts the
   659 $if::[o,o,o]\To o$.  The axiom \tdx{if_def} asserts the
   660 equation~$(if)$.
   660 equation~$(if)$.
   661 \begin{ttbox}
   661 \begin{ttbox}
   662 If = FOL +
   662 If = FOL +
   663 consts  if     :: "[o,o,o]=>o"
   663 consts  if     :: [o,o,o]=>o
   664 rules   if_def "if(P,Q,R) == P&Q | ~P&R"
   664 rules   if_def "if(P,Q,R) == P&Q | ~P&R"
   665 end
   665 end
   666 \end{ttbox}
   666 \end{ttbox}
   667 The derivations of the introduction and elimination rules demonstrate the
   667 The derivations of the introduction and elimination rules demonstrate the
   668 methods for rewriting with definitions.  Classical reasoning is required,
   668 methods for rewriting with definitions.  Classical reasoning is required,