lógica lista 4

regras alfa (não bifurcam)

T (A ^ B)      T A  T B
F (A v B)      F A  F B
F (A -> B)     T A  F B
T ¬A           F A


regras beta (bifurcam)

F (A ^ B)      F A  F B
T (A v B)      T A  T B
T (A -> B)     F A  T B
F ¬A           T A





1)
a) A -> (B -> ¬C), C, A |- ¬B

\1  T A -> (B -> ¬C)                         (premissa)
\2  T C                                      (premissa)
\3  T A                                      (premissa)
\4  F ¬B                                     (sequente)
\5  T B                                      (beta¬  4)
\6  F A               T (B -> ¬C)            (beta-> 1)
\7   X(3,6)           F B          T ¬C      (beta-> 6)
\8                     X(5,7)      F C       (alfa¬  7)
\9                                  X(2,8)



b) ((A ^ B) -> (C v B)) |- (A -> (B -> C))

\ 1  T ((A ^ B) -> (C v B))               (premissa)
\ 2  F (A -> (B -> C))                    (sequente)
\ 3  T A                                  (alfa-> 2)
\ 4  F (B -> C)                           (alfa-> 2)
\ 5  T B                                  (alfa-> 4)
\ 6  F C                                  (alfa-> 4)
\ 7  F (A ^ B)            T (C v B)       (beta-> 1)
\ 8  F A     F B          T (C v B)       (beta^  7)
\ 9  X(3,8)  X(5,8)       T C     T B     (betav  8)
\10                        X(6,9)  O
tableau aberto - falsificável pela valoração A=1, B=1, C=0



c) (A v B) |- ¬(¬A ^ ¬B)

\ 1  T (A v B)            (premissa)
\ 2  F ¬(¬A ^ ¬B)         (sequente)
\ 3  T (¬A ^ ¬B)          (beta¬  2)
\ 4  T ¬A                 (alfa^  3)
\ 5  T ¬B                 (alfa^  3)
\ 6  F A                  (alfa¬  4)
\ 7  F B                  (alfa¬  5)
\ 8  T A          T B     (betav  1)
\ 9   X(6,8)       X(7,8)



d) ((A -> B) -> A) |- A ^ B

\ 1  T ((A -> B) -> A)                    (premissa)
\ 2  F (A ^ B)                            (sequente)
\ 3  F (A -> B)           T A             (beta-> 1)
\ 4  T A                  ...             (alfa-> 3)
\ 5  F B                  ...             (alfa-> 3)
\ 6  F A     F B          F A     F B     (beta^  2)
\ 7   X(4,6)  O            X(3,6)  O
tableau aberto - falsificável pela valoração A=1, B=0



e) A -> B |- ¬A v B

\ 1  T (A -> B)         (premissa)
\ 2  F (¬A v B)         (sequente)
\ 3  F ¬A               (alfav  2)
\ 4  F B                (alfav  2)
\ 5  T A                (beta¬  3)
\ 6  F A        T B     (beta-> 1)
\ 7   X(5,6)     X(4,6)





2)
a) |- (A v B) ^ (¬B -> ¬A)
\ 1  F ((A v B) ^ (¬B -> ¬A))            (sequente)
\ 2  F (A v B)          F (¬B -> ¬A)     (beta^  1)
\ 3  F A                ...              (alfav  2)
\ 4  F B                ...              (alfav  2)
\ 5  ...                T ¬B             (alfa-> 2)
\ 6  ...                F ¬A             (alfa-> 2)
\ 7  ...                F B              (alfa¬  5)
\ 8  ...                T A              (beta¬  6)
\ 9   O                  O
tableau aberto - falsificável pelas valorações A=0, B=0 ou A=1, B=0



b) |- (A -> (B -> C)) -> (B -> (A -> B))
\ 1  F ((A -> (B -> C)) -> (B -> (A -> B)))     (sequente)
\ 2  T (A -> (B -> C))                          (alfa-> 1)
\ 3  F (B -> (A -> B))                          (alfa-> 1)
\ 4  T B                                        (alfa-> 3)
\ 5  F (A -> B)                                 (alfa-> 3)
\ 6  T A                                        (alfa-> 5)
\ 7  F B                                        (alfa-> 5)
      X(4,7)



c) |- (A -> B) -> (¬B ^ ¬A)
\ 1  F ((A -> B) -> (¬B ^ ¬A))            (sequente)
\ 2  T (A -> B)                           (alfa-> 1)
\ 3  F (¬B ^ ¬A)                          (alfa-> 1)
\ 4  F ¬B                 F ¬A            (beta^  3)
\ 5  T B                  ...             (beta¬  4)
\ 6  ...                  T A             (beta¬  4)
\ 7  F A     T B          F A     T B     (beta-> 2)
      O       O            X(6,7)  O
tableau aberto - falsificável pelas valorações A=0, B=1 ou A=1, B=1



d) |- (A ^ B) v (¬A ^ ¬B)
\ 1  F ((A ^ B) v (¬A ^ ¬B))              (premissa)
\ 2  F (A ^ B)                            (alfav  1)
\ 3  F (¬A ^ ¬B)                          (alfav  1)
\ 4  F ¬A                 F ¬B            (beta^  3)
\ 5  T A                  ...             (beta¬  4)
\ 6  ...                  T B             (beta¬  4)
\ 7  F A     F B          F A     F B     (beta^  2)
  8   X(5,7)  O            O       X(6,7)
tableau aberto - falsificável pelas valorações A=1, B=0 ou A=0, B=1