doc-src/Logics/FOL.tex
 changeset 157 8258c26ae084 parent 111 1b3cddf41b2d child 287 6b62a6ddbe15
equal 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 \]`