Lógica/Cálculo Proposicional Clássico/Dedução Natural - Parte II/Resolução dos Exercícios

De testwiki
Ir para a navegação Ir para a procura

Resolução de algumas Regras de Inferência Derivadas

¬β→¬α⊢α→β

 
1.   ¬β→¬α   Premissa
 
2.     α   Hipótese
3.     ¬¬α   2 DN
4.     ¬¬β   1,3 MT
5.     β   4 DN
6.   α→β   2,5 RPC

α⊢¬α→β

 
1.   α   Premissa
 
2.     ¬α   Hipótese
3.     β   1,2 CTR
4.   ¬α→β   2,3 RPC

¬α∧¬β⊢¬(α∨β)

 
1.   ¬α∧¬β   Premissa
 
2.     α∨β   Hipótese
3.     ¬α   1 S
4.     ¬β   1 S
5.     β   2,3 SD
6.     β∧¬β   5,4 C
7.   ¬(α∨β)   2,6 RAA

¬α∨¬β⊢¬(α∧β)

 
1.   ¬α∨¬β   Premissa
 
2.     α∧β   Hipótese
3.     α   2 S
4.     ¬¬α   3 DN
5.     ¬β   1,4 SD
6.     β   2 S
7.     β∧¬β   5,6 C
8.   ¬(α∧β)   2,7 RAA

1

{(A∧B)→C,¬C}⊢¬A∨¬B

 
1.   (A∧B)→C   Premissa
2.   ¬C   Premissa
3.   ¬(A∧B)   1,2 MT
4.   ¬A∨¬B   3 DM

2

¬(A∧¬B)⊢A→B

 
1.   ¬(A∧¬B)   Premissa
2.   ¬A∨¬¬B   1 DM
 
3.     A   Hipótese
4.     ¬¬A   3 DN
5.     ¬¬B   2,4 SD
6.     B   5 DN
7.   A→B   3,6 RPC

3

¬A→B⊢A∨B

 
1.   ¬A→B        Premissa
 
2.     ¬(A∨B)   Hipótese
3.     ¬A∧¬B   2 DM
4.     ¬A   3 S
5.     ¬B   3 S
6.     B   1,4 MP
7.     B∧¬B   6,5 C
8.   ¬¬(A∨B)       2,7 RAA
9.   A∨B       8 DN

4

{A→C,B→C}⊢(A∨B)→C

 
1.   A→C        Premissa
2.   B→C        Premissa
 
3.     ¬C   Hipótese
4.     ¬A   1,3 MT
5.     ¬B   2,3 MT
6.     ¬A∧¬B   4,5 C
7.     ¬(A∨B)   6 DM
8.   ¬C→¬(A∨B)   3,7 RPC
9.   (A∨B)→C   8 CT

5

¬(A→B)⊢A∧¬B

 
01.   ¬(A→B)        Premissa
 
02.     ¬(A∧¬B)       Hipótese
03.     ¬A∨¬¬B       2 DM
   
04.       A   Hipótese  
05.       ¬¬A   4 DN
06.       ¬¬B   3,5 SD
07.       B   6 DN
08.     A→B             4,7 RPC
09.     (A→B)∧¬(A→B)             8,1 C
10.   ¬¬(A∧¬B)                         2,9 RAA
11.   A∧¬B                         10 DN

6

A→B⊢(A∨C)→(B∨C)

 
01.   A→B        Premissa
 
02.     A∨C       Hipótese
   
03.       ¬(B∨C)   Hipótese  
04.       ¬B∧¬C   3 DM
05.       ¬C   4 S
06.       ¬B   4 S
07.       A   2,5 SD
08.       B   1,7 MP
09.       B∧¬B   1,7 MP
10.     ¬¬(B∨C)        3,9 RAA
11.     B∨C        10 DN
12.   (A∨C)→(B∨C)   2,11 RPC

Resolução dos Exercícios de Demonstração de Teoremas

1

⊢A↔A

 
1.     A           Hipótese
   
2.     A           1 R
3.   A→A   1,2 RPC
4.   A↔A   3,3 CB

2

⊢A↔¬¬A

 
1.     A         Hipótese
   
2.     ¬¬A         1 DN
3.   A→¬¬A   1,2 RPC
4.     ¬¬A         Hipótese
   
5.     A         4 DN
6.   ¬¬A→A   4,5 RPC
7.   A↔¬¬A   3,6 CB

3

⊢¬(A↔¬A)

 
01.     A↔¬A           Hipótese
02.     A→¬A         1 BC
03.       A   Hipótese
04.       ¬A   2,3 MP
05.       A∧¬A     3,4 C
06.     ¬A     3,5 RAA
07.     ¬A→A     1 BC
08.     A     7,6 MP
09.     A∧¬A     8,6 C
 
10.   ¬(A↔¬A)   1,9 RAA

4

⊢A→(B→A)

 
1.     A           Hipótese
   
2.       B   Hipótese
3.       A   1 R
4.     B→A     2,3 RPC
5.   A→(B→A)   1,4 RPC

5

⊢(¬A→A)→A

 
1.     ¬A→A           Hipótese
   
2.       ¬A   Hipótese
3.       A   1,2 MP
4.       A∧¬A   3,2 C
5.     ¬¬A           2,4 RAA
6.     A           5 DN
7.   (¬A→A)→A   1,6 RPC

6

⊢P→(Q→(P∧Q))

 
1.     P           Hipótese
   
2.       Q   Hipótese
3.       P∧Q   1,2 C
4.     Q→(P∧Q)     2,3 RPC
5.   P→(Q→(P∧Q))   1,4 RPC

7

⊢((A∧B)→C)↔((A∧¬C)→¬B)

 
01.     (A∧B)→C   Hipótese
   
02.       A∧¬C                Hipótese
03.       A                2 S
04.       ¬C                2 S
05.       ¬(A∧B)                1,4 MT
06.       ¬A∨¬B                5 DM
07.       ¬¬A                3 DN
08.       ¬B                6,7 SD
     
09.     ((A∧¬C)→¬B)   2,8 RPC
   
10.   ((A∧B)→C)→((A∧¬C)→¬B)   1,9 RPC
 
 
11.     (A∧¬C)→¬B   Hipótese
   
12.       A∧B         

      Hipótese

13.       A   12 S
14.       B   12 S
15.       ¬¬B   14 DN
16.       ¬(A∧¬C)   11,15 MT
17.       ¬A∨¬¬C   16 DM
18.       ¬¬A   13 DN
19.       ¬¬C   17,18 SD
20.       C   19 DN
     
21.     (A∧B)→C   12,20 RPC
 
22.   ((A∧¬C)→¬B)→((A∧B)→C)   9,15 RPC
23.   ((A∧B)→C)↔((A∧¬C)→¬B)   10,22 CB

8

⊢(A→(B→C))→((A→B)→(A→C))

 
1.     A→(B→C)   Hipótese
   
2.       A→B         Hipótese
     
3.         A   Hipótese
4.         B→C   1,3 MP
5.         B   2,3 MP
6.         C   4,5 MP
       
7.       A→C   3,6 RPC
     
8.     (A→B)→(A→C)   2,7 RPC
 
9.   (A→(B→C))→((A→B)→(A→C))   1,8 RPC

9

⊢(D→(B→A))→(B→(D→A))

 
1.     D→(B→A)   Hipótese
   
2.       B         Hipótese
     
3.         D   Hipótese
4.         B→A   1,3 MP
5.         A   4,2 MP
       
6.       D→A   3,5 RPC
     
7.     B→(D→A)   2,6 RPC
 
8.   (D→(B→A))→(B→(D→A))   1,7 RPC

10

⊢(P→Q)→((P→¬Q)→¬P)

 
1.     P→Q   Hipótese
   
2.       P→¬Q         Hipótese
     
3.         P   Hipótese
4.         Q   1,3 MP
5.         ¬Q   2,3 MP
6.         Q∧¬Q   4,5 C
       
7.       ¬P   3,6 RAA
     
8.     (P→¬Q)→¬P   2,7 RPC
 
9.   (P→Q)→((P→¬Q)→¬P)   1,8 RPC

11

⊢(A→B)→((C→B)→((A∨C)→B))

 
01.     A→B   Hipótese
   
02.       C→B         Hipótese
     
03.         ¬B   Hipótese
04.         ¬A   1,3 MT
05.         ¬C   2,3 MT
06.         ¬A∧¬C   4,5 C
07.         ¬(A∨C)   6 DM
       
08.       ¬B→¬(A∨C)   3,7 RPC
09.       (A∨C)→B   8 CT
     
10.     (C→B)→((A∨C)→B)   2,7 RPC
 
11.   (A→B)→((C→B)→((A∨C)→B))   1,10 RPC

Predefinição:AutoCat