doc-src/Logics/FOL.tex
changeset 157 8258c26ae084
parent 111 1b3cddf41b2d
child 287 6b62a6ddbe15
equal deleted inserted replaced
156:ab4dcb9285e0 157:8258c26ae084
   648 Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$
   648 Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$
   649 directly, without reference to its definition.  The simple identity
   649 directly, without reference to its definition.  The simple identity
   650 \[ if(P,Q,R) \bimp (P\imp Q)\conj (\neg P\imp R) \]
   650 \[ if(P,Q,R) \bimp (P\imp Q)\conj (\neg P\imp R) \]
   651 suggests that the
   651 suggests that the
   652 $if$-introduction rule should be
   652 $if$-introduction rule should be
   653 \[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{P}  &  \infer*{R}{\neg P}} \]
   653 \[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]}  &  \infer*{R}{[\neg P]}} \]
   654 The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the
   654 The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the
   655 elimination rules for~$\disj$ and~$\conj$.
   655 elimination rules for~$\disj$ and~$\conj$.
   656 \[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}
   656 \[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}
   657                                   & \infer*{S}{[\neg P,R]}} 
   657                                   & \infer*{S}{[\neg P,R]}} 
   658 \]
   658 \]