Lógica/Cálculo Quantificacional Clássico/Dedução Natural no CQC/Resolução dos exercícios

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

{∀x(Px∨Qx),¬Qa}⊢Pa

 
1.   ∀x(Px∨Qx)   Premissa
2.   ¬Qa   Premissa
3.   Pa∨Qa   1 ℰ∀
4.   Pa   3,2 SD


{∀x(Ax∧Bx),(Cx∧Dx)}⊢(Ax∧Cx)

 
1.   ∀x(Ax∧Bx)   Premissa
2.   ∀x(Bx∧Cx)   Premissa
3.   Ad∧Bd   1 ℰ∀
4.   Cd∧Dd   2 ℰ∀
5.   Ad   3 S
6.   Cd   4 S
7.   Ad∧Cd   5,6 C
8.   ∀x(Ax∧Cx)   7 ℐ∀


{∀x(Ax→Bx),Al}⊢∃xBx

 
1.   ∀x(Ax→Bx)   Premissa
2.   Al   Premissa
3.   Al→Bl   1 ℰ∀
4.   Bl   3,2 MP
5.   ∃xBx   5 ℐ∃


∃x(Px∧Qx)⊢∃xPx∧∃xQx

 
1.   ∃x(Px∧Qx)   Premissa
 
2.     Pa∧Qa   Hipótese para ℰ∃
3.     Pa   2 S
4.     Qa   2 S
5.     ∃xPx   3 ℐ∃
6.     ∃xQx   4 ℐ∃
7.     ∃xPx∧∃xQx   5,6 C
8.   ∃xPx∧∃xQx   1,2-7 ℰ∃


{∃xPx,∀xQx}⊢∃x(Px∧Qx)

 
1.   ∃xPx   Premissa
2.   ∀xQx   Premissa
 
3.     Pa   Hipótese para ℰ∃
4.     Qa   2 ℰ∀
5.     Pa∧Qa   3,4 C
6.     ∃x(Px∧Qx)   5 ℐ∃
7.   ∃x(Px∧Qx)         1,3-6 ℰ∃

Exercícios de teoremas

⊢∃xPx→¬∀x¬Px

 
1.     ∃xPx           Hipótese
   
2.       ∀x¬Px   Hipótese
3.       ¬∃xPx   2 IQ
4.       ∃xPx∧¬∃xPx   1,3 C
5.     ¬∀x¬Px     2,4 RAA
6.   ∃xPx→¬∀x¬Px   1,5 RPC


⊢∀x(Px→Q)→∃x(Px→Q)

 
1.     ∀x(Px→Q)   Hipótese
   
2.     Pa→Q   1 ℰ∀
3.     ∃x(Px→Q)   2 ℐ∃
4.   ∀x(Px→Q)→∃x(Px→Q)   1,3 RPC


⊢∃x∃yPxy↔∃y∃xPxy

 
01.     ∃x∃yPxy   Hipótese
   
02.       ∃yPxy               Hipótese para ℰ∃
     
03.         Pab   Hipótese para ℰ∃
04.         ∃xPxb   3 ℐ∃
05.         ∃y∃xPxy   4 ℐ∃
       
06.       ∃y∃xPxy   2,3-5 ℰ∃
     
07.     ∃y∃xPxy   1,2-6 ℰ∃
 
08.   ∃y∃xPxy→∃y∃xPxy   1,7 RPC
 
 
09.     ∃x∃yPxy   Hipótese
   
10.       ∃xPxa               Hipótese para ℰ∃
     
11.         Pba   Hipótese para ℰ∃
12.         ∃yPyb   11 ℐ∃
13.         ∃x∃yPxy   12 ℐ∃
       
14.       ∃x∃yPxy   10,11-13 ℰ∃
     
15.     ∃x∃yPxy   9,10-14 ℰ∃
 
08.   ∃y∃xPxy→∃x∃yPxy   1,7 RPC
 
17.   ∃x∃yPxy↔∃y∃xPxy   8,16 CB


⊢(∀xPx∧∀xQx)↔∀x(Px∧Qx)

 
01.     ∀xPx∧∀xQx         Hipótese
   
02.     ∀xPx         1 S
03.     ∀xQx         1 S
04.     Pa         2 ℰ∀
05.     Qa         3 ℰ∀
06.     Pa∧Qa         4,5 C
07.     ∀x(Px∧Qx)         2 ℐ∀
08.   (∀xPx∧∀xQx)→∀x(Px∧Qx)   1,7 RPC
09.     ∀x(Px∧Qx)         Hipótese
   
10.     Pa∧Qa         9 ℰ∀
11.     Pa         10 S
12.     ∀xPx         11 ℐ∀
13.     Qa         10 S
14.     ∀xQx         13 ℐ∀
15.     ∀xQx         13 ℐ∀
16.   ∀x(Px∧Qx)→(∀xPx∧∀xQx)   4,5 RPC
17.   (∀xPx∧∀xQx)↔∀x(Px∧Qx)   8,16 CB


⊢(P∧∃xQx)↔∃x(P∧Qx)

 
01.     P∧∃xQx           Hipótese
02.     ∃xQx         1 S
03.       Qa   Hipótese para ℰ∃
04.       P   1 S
05.       P∧Qa     4,3 C
06.       ∃x(P∧Qa)     5 ℐ∃
07.     ∃x(P∧Qa)     2,3-6 ℰ∃
08.   (P∧∃xQx)→∃x(P∧Qx)   1,7 RPC
09.     ∃x(P∧Qx)           Hipótese
           
10.       P∧Qa   Hipótese para ℰ∃
11.       Qa   10 S
12.       ∃xQx     11 ℐ∃
13.       P     10 S
14.       P∧∃xQx     12,13 C
15.     P∧∃xQx     9,10-14 ℰ∃
16.   ∃x(P∧Qx)→(P∧∃xQx)   9,15 RPC
17.   (P∧∃xQx)↔∃x(P∧Qx)   8,16 CB


⊢(P∨∀xQx)↔∀x(P∨Qx)

 
01.     P∨∀xQx   Hipótese
   
02.       ¬∀x(P∨Qx)         Hipótese
03.       ∃x¬(P∨Qx)         2 IQ
     
04.         ¬(P∨Qa)   Hipótese para ℰ∃
05.         ¬P∧¬Qa   4 DM
06.         ¬Qa   5 S
07.         ¬P   5 S
08.         ∀xQx   1,7 SD
09.         ∃x¬Qx   6 ℐ∃
10.         ¬∀xQx   9 IQ
11.         ∀xQx∧¬∀xQx   8,10 C
       
12.       ∀xQx∧¬∀xQx   3,4-11 ℰ∃
     
13.     ¬¬∀x(P∨Qx)   2,17 RAA
14.     ∃x(Px∨Qx)   13 DN
 
15.   (P∨∀xQx)→∀x(P∨Qx)   1,19 RPC
16.     ∀x(P∨Qx)   Hipótese
17.     P∨Qa   16 ℰ∀
   
18.       ¬(P∨∀xQx)         Hipótese
19.       ¬P∧¬∀xQx         18 DM
20.       ¬P         19 S
21.       Qa         17,20 SD
22.       ∀Qx         21 ℐ∀
23.       ¬∀Qx         19 S
24.       ∀Qx∧¬∀Qx         22,23 C
     
25.     ¬¬(P∨∀xQx)         18,24 RAA
26.     (P∨∀xQx)         25 DN
27.   ∀x(P∨Qx)→(P∨∀xQx)         16,26 RPC
28.   (P∨∀xQx)↔∀x(P∨Qx)         15,27 CB


⊢∃x(Px→Q)→(∀xPx→Q)

 
1.     ∃x(Px→Q)   Hipótese
   
2.       ∀xPx         Hipótese
3.       Pa         2 ℰ∀
     
4.         Pa→Q   Hipótese para ℰ∃
5.         Q 4,3 MP
       
6.       Q   1,4-5 ℰ∃
     
7.     ∀xPx→Q   2,6 RPC
 
8.   ∃x(Px→Q)→(∀xPx→Q)   1,7 RPC

Predefinição:AutoCat