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 \] |