doc-src/Logics/FOL.tex
changeset 1388 7705e6211865
parent 874 2432820efbfe
child 2495 82ec47e0a8d3
equal deleted inserted replaced
1387:9bcad9c22fd4 1388:7705e6211865
   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,