doc-src/Logics/LK.tex
changeset 841 14b96e3bd4ab
parent 333 2ca08f62df33
child 3137 786faf45f1f3
equal deleted inserted replaced
840:5716e174b591 841:14b96e3bd4ab
   162 \tdx{conjL}   $H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E
   162 \tdx{conjL}   $H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E
   163 
   163 
   164 \tdx{disjR}   $H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F
   164 \tdx{disjR}   $H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F
   165 \tdx{disjL}   [| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E
   165 \tdx{disjL}   [| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E
   166             
   166             
   167 \tdx{impR}    $H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $
   167 \tdx{impR}    $H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F
   168 \tdx{impL}    [| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E
   168 \tdx{impL}    [| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E
   169             
   169             
   170 \tdx{notR}    $H, P |- $E, $F ==> $H |- $E, ~P, $F
   170 \tdx{notR}    $H, P |- $E, $F ==> $H |- $E, ~P, $F
   171 \tdx{notL}    $H, $G |- $E, P ==> $H, ~P, $G |- $E
   171 \tdx{notL}    $H, $G |- $E, P ==> $H, ~P, $G |- $E
   172 
   172