[notA]1         notA -> notB  
       ---------------------------------------
                          notB                    [B]2                    
                       -----------------------------------
                                     bot
                               -------------- 1
                                      A
                                 ---------- 2
                                    B -> A



    [B]1
   ------
    A->B      not(A->B)
   ----------------------
            bot
         -------- 1
           notB



   A   B  |  not(A->B) |  notB
-------------------------------
   1   1  |     0      |   0
   1   0  |     1      |   1
   0   1  |     0      |   0
   0   0  |     0      |   1


notB e' una conseguenza tautologica di not(A->B), cioe' not(A->B)|= notB,
(poiche' per tutti gli assegnamenti proposizionali per cui not(A->B)
e' vero anche notB e' vero)
quindi per il teorema di completezza e correttezza vale not(A->B)|- notB