Mostrar código-fonte de Lógica/Cálculo Proposicional Clássico/Dedução Natural - Parte II

==Regras de Inferência Derivadas==

Por meio das regras de inferência diretas e hipotéticas podemos demonstrar vários raciocínios bastante recorrentes. Estes raciocíonios, uma vez demonstrados, podem ser usados como regras de inferência diretas. Elas não são necessárias, mas são bastante úteis, tornando nossas derivações muito mais sucintas. Anteriormente demonstramos dois raciocínios que nos serão úteis como regras de inferência derivadas:

*'''Dupla Negação em ambas direções (DN)'''
: <math>\frac{\neg \neg \varphi\,}{\overline{\varphi\quad\;\,}}</math>

*'''Silogismo Hipotético (SH)'''
: <math>\alpha \to \beta</math>
: <math>\underline{\beta \to \gamma}</math>
: <math>\alpha \to \gamma</math>

Vamos ampliar nossa lista de regras de inferência derivadas, demonstrado uma por uma:

===Repetição (R)===
<math>\alpha \vdash \alpha</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 1.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\alpha</math>
| &nbsp;
| '''Premissa'''
|- style="height:10px"
| 2.
| style="border-right:2px solid black" | &nbsp;
| <math>\neg\neg\alpha</math>
| width="15px" | &nbsp;
| '''1 DN'''
|-
| 3.
| style="border-right:2px solid black" | &nbsp;
| <math>\alpha</math>
| width="15px" | &nbsp;
| '''2 DN'''
|}
|}

===Modus Tollens (MT)===

<math>\left\{\alpha \to \beta , \neg \beta \right\} \vdash \neg \alpha</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 1.
| style="border-right:2px solid black" | &nbsp;
| <math>\alpha \to \beta</math>
| width="15px" | &nbsp;
| '''Premissa'''
|-
| 2.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg \beta</math>
| &nbsp;
| '''Premissa'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 3. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\alpha</math>
| width="15px" | &nbsp;
| '''Hipótese'''
|-
| 4.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\beta</math>
| &nbsp;
| '''1,3 MP''' 
|-
| 5.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\beta \land \neg \beta</math>
| &nbsp;
| '''2,4 C''' 
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 6.
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \alpha</math>
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp;
| '''3,5 RAA'''
|}
|}

===Prefixação (PRF)===
<math>\alpha\vdash\beta\to\alpha</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 1.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\alpha</math>
| &nbsp;
| '''Premissa'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 2. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\beta</math>
| width="15px" | &nbsp;
| '''Hipótese''' 
|-
| 3.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\alpha</math>
| &nbsp;
| '''1 R''' 
|-
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 4.
| style="border-right:2px solid black" | &nbsp;
| <math>\beta\to\alpha</math>
| &nbsp;
| '''2,3 RPC'''
|}
|}

===Contraposição (CT)===
Aproveitaremos o ''Modus Tollens'' como regra de inferência.

<math>\alpha \to \beta \vdash \neg \beta \to \neg \alpha</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 1.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\alpha \to \beta</math>
| &nbsp;
| '''Premissa'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 2. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg \beta</math>
| width="15px" | &nbsp;
| '''Hipótese'''
|-
| 3.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \alpha</math>
| &nbsp;
| '''1,2 MT''' 
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 4.
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \beta \to \neg \alpha</math>
| &nbsp;
| '''2,3 RPC'''
|}
|}

Agora tente você provar a recíproca, ou seja, que <math>\neg \beta \to \neg \alpha \vdash \alpha \to \beta</math>

[[Lógica/Cálculo Proposicional Clássico/Dedução Natural - Parte II/Resolução dos Exercícios#Contraposição|Confira aqui sua resposta]].

===Contradição (CTR)===

<math>\left\{\alpha , \neg \alpha \right\}\vdash \beta</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 1.
| style="border-right:2px solid black" | &nbsp;
| <math>\alpha</math>
| width="15px" | &nbsp;
| '''Premissa'''
|-
| 2.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg \alpha</math>
| width="15px" | &nbsp;
| '''Premissa'''
|-
| 3.
| style="border-right:2px solid black" | &nbsp;
| <math>\alpha \lor \beta</math>
| width="15px" | &nbsp;
| '''1 E'''
|-
| 4.
| style="border-right:2px solid black" | &nbsp;
| <math>\beta</math>
| &nbsp;
| '''2,3 SD'''
|}
|}

===Lei de Duns Scot (DS)===
<math>\neg \alpha\vdash \alpha\to\beta </math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 1.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg\alpha</math>
| &nbsp;
| '''Premissa'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 2. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\alpha</math>
| width="15px" | &nbsp;
| '''Hipótese''' 
|-
| 3.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\beta</math>
| &nbsp;
| '''1,2 CTR''' 
|-
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 4.
| style="border-right:2px solid black" | &nbsp;
| <math>\alpha\to\beta</math>
| &nbsp;
| '''2,3 RPC'''
|}
|}

Prove que também vale <math>\alpha\vdash \neg \alpha\to\beta </math> .

[[Lógica/Cálculo Proposicional Clássico/Dedução Natural - Parte II/Resolução dos Exercícios#Lei de Dun Scot|Confira aqui sua resposta]].

===Lei De Morgan I (DM)===
<math>\neg \left( \alpha \lor \beta \right)\vdash \neg \alpha \land \neg \beta</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 01.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg \left( \alpha \lor \beta \right)</math>
| &nbsp;
| '''Premissa'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 02. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\alpha</math>
| width="15px" | &nbsp;
| '''Hipótese'''
|-
| 03.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\alpha \lor \beta</math>
| &nbsp;
| '''2 E'''
|-
| 04.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\left(\alpha \lor \beta\right)\land \neg \left( \alpha \lor \beta \right)</math>
| &nbsp;
| '''1,3 C''' 
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 05.
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \alpha</math>
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; '''2,4 RAA'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 06. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\beta</math>
| width="15px" | &nbsp;
| '''Hipótese'''
|-
| 07.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\alpha \lor \beta</math>
| &nbsp;
| '''6 E''' 
|-
| 08.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\left(\alpha \lor \beta\right)\land \neg \left( \alpha \lor \beta \right)</math>
| &nbsp;
| '''1,7 C''' 
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 09.
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \beta</math>
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp; &nbsp; &nbsp; '''6,8 RAA'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 10.
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \alpha \land \neg \beta</math>
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp;
| &nbsp; &nbsp; &nbsp; '''5,9 C'''
|}
|}

Agora tente você provar a recíproca, ou seja, que <math>\neg \alpha \land \neg \beta \vdash \neg \left( \alpha \lor \beta \right)</math>

[[Lógica/Cálculo Proposicional Clássico/Dedução Natural - Parte II/Resolução dos Exercícios#Lei De Morgan I|Confira aqui sua resposta]]

===Lei De Morgan II (DM)===
<math>\neg \left(\alpha\land \beta\right)\vdash \neg \alpha \lor \neg \beta</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 01.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg \left(\alpha\land \beta\right)</math>
| &nbsp;
|  &nbsp; &nbsp; &nbsp;'''Premissa'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 02. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg \left(\neg \alpha \lor \neg \beta \right)</math>
| width="15px" | &nbsp;
| &nbsp; &nbsp; '''Hipótese'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 03.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg \alpha</math>
| &nbsp;
| '''Hipótese''' 
| &nbsp;
|-
| 04.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \alpha \lor \neg \beta</math>
| &nbsp;
| '''3 E''' 
|-
| 05.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\left(\neg \alpha \lor \neg \beta\right)\land \neg \left(\neg \alpha \lor \neg \beta \right)</math>
| &nbsp;
| '''5,2 C''' 
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 06.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \neg \alpha</math>
| &nbsp;
| &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;'''3,5 RAA''' 
|-
| 07.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\alpha</math>
| &nbsp;
| &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;&nbsp; &nbsp; &nbsp;'''6 DN''' 
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 08.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg \beta</math>
| &nbsp;
| '''Hipótese''' 
| &nbsp;
|-
| 09.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \alpha \lor \neg \beta</math>
| &nbsp;
| '''8 E''' 
|-
| 10.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\left(\neg \alpha \lor \neg \beta\right)\land \neg \left(\neg \alpha \lor \neg \beta \right)</math>
| &nbsp;
| '''9,2 C''' 
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 11.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \neg \beta</math>
| &nbsp;
| &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; '''8,10 RAA''' 
|-
| 12.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\beta</math>
| &nbsp;
| &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; '''11 DN''' 
|-
| 13.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\alpha\land\beta</math>
| &nbsp;
| &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; '''7,12 C''' 
|-
| 14.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\left(\alpha\land\beta\right)\land \neg \left(\alpha\land \beta\right)</math>
| &nbsp;
| &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; '''13,1 C''' 
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 15. 
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \neg \left(\neg \alpha \lor \neg \beta \right)</math>
| width="15px" | &nbsp;
|  &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; '''2,14 RAA'''
|-
| 16. 
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \alpha \lor \neg \beta </math>
| width="15px" | &nbsp;
|  &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; '''15 DN'''
|}
|}

Tente você agora provar a recíprova, ou seja, que <math>\neg \alpha \lor \neg \beta\vdash \neg \left(\alpha\land \beta\right)</math>

[[Lógica/Cálculo Proposicional Clássico/Dedução Natural - Parte II/Resolução dos Exercícios#Lei De Morgan II|Confira aqui sua resposta]]

===Lista das Regras Derivadas===
[[Imagem:Regras Derivadas2.png]]

===Exercícios===
Valendo-se das regras derivadas, prove que:

#  <math>\left \{\left(A\land B\right)\to C , \neg C\right \}\vdash \neg A \lor \neg B</math>
#  <math>\neg \left(A\land \neg B\right)\vdash A\to B</math>
#  <math>\neg A\to B\vdash A\lor B</math>
#  <math>\left\{A\to C , B\to C\right\}\vdash \left(A\lor B\right)\to C</math>
#  <math>\neg \left(A\to B\right)\vdash A\land \neg B</math>
#  <math>A\to B\vdash \left(A\lor C\right)\to \left(B\lor C\right)</math>

[[Lógica/Cálculo Proposicional Clássico/Dedução Natural - Parte II/Resolução dos Exercícios#Resolução dos Exercícios de Aplicação das Regras de Inferência Derivadas|Resolução dos Exercícios]]

==Teoremas==
Agora não temos mais premissas para trabalhar, devemos nos limitar às hipóteses. Algumas estratégias para provar teoremas podem ser traçadas:

*'''Por redução ao absurdo'''
Para provar <math>\neg\varphi</math>, levante a hipótese <math>\varphi</math> e derive dela uma contradição e aplique RAA. 

Para provar <math>\varphi</math> , levante a hipótese <math>\neg \varphi</math> e derive dela uma contradição, aplique RAA e então DN.

*'''Por regra para condicionais'''
Para provar <math>\varphi\to \psi</math>, levante o antecedente <math>\varphi</math> como hipótese, derive <math>\psi</math> e então aplique RPC.

Para provar <math>\varphi\leftrightarrow \psi</math>, prove <math>\varphi\to \psi</math> e <math>\psi\to \varphi</math>, como explicado acima, e então aplique CB.

===Exemplo 1===
<math>\vdash \neg\left(A\land\neg A\right)</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 1. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>A\land\neg A</math>
| width="10px" | &nbsp;
| '''Hipótese'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 2.
| style="border-right:2px solid black" | &nbsp;
| <math>\neg\left(A\land\neg A\right)</math>
| width="10px" | &nbsp;
| '''1 RAA'''
|}
|}

===Exemplo 2===
<math>\vdash A\lor\neg A</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 1. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg\left(A\lor\neg A\right)</math>
| width="10px" | &nbsp;
| '''Hipótese'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|
|
|
|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 2.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>\neg A\land \neg \neg A</math>
| width="10px" | &nbsp;
| '''1 DM'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 3.
| style="border-right:2px solid black" | &nbsp;
| <math>\neg\neg\left(A\lor\neg A\right)</math>
| width="10px" | &nbsp;
| '''1,2 RAA'''
|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 4.
| style="border-right:2px solid black" | &nbsp;
| <math>A\lor\neg A</math>
| width="10px" | &nbsp;
| '''3 DN'''
|}
|}

===Exemplo 3===
<math>\vdash \left(A\to\left(A\to B\right)\right)\to\left(A\to B\right)</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 1. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>A\to\left(A\to B\right)</math>
| width="10px" | &nbsp;
| '''Hipótese'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 2. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>A</math>
| width="15px" | &nbsp;
|
| '''Hipótese'''
|-
| 3.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>A\to B</math>
| &nbsp;
|
| '''1,2 MP'''
|- style="height:10px"
| width="15px" | 4.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>B</math>
|
|
| &nbsp;&nbsp;&nbsp;'''3,2 MP'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 5.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>A\to B</math>
| width="10px" | &nbsp;
|
| '''2,6 RPC'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 6.
| style="border-right:2px solid black" | &nbsp;
| <math>\left(A\to\left(A\to B\right)\right)\to\left(A\to B\right)</math>
| width="10px" | &nbsp;
| '''1,7 RPC'''
|}
|}

===Exemplo 4===
<math>\vdash \left(A\to B\right)\lor \left(B\to A\right)</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 01. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg\left(\left(A\to B\right)\lor \left(B\to A\right)\right)</math>
| width="10px" | &nbsp;
| '''Hipótese'''
|
|- 
| 02.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg\left(A\to B\right)\land \neg\left(B\to A\right)</math>
| &nbsp;
| '''1 DM'''
|- 
| 03.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg\left(A\to B\right)</math>
| &nbsp;
| '''2 S'''
|- 
| 04.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg\left(B\to A\right)</math>
| &nbsp;
| '''2 S'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 05. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>A</math>
| width="15px" | &nbsp;
|
| '''Hipótese'''
|-
| 06.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>B\to A</math>
| &nbsp;
|
| '''5 PRF'''
|- 
| 07.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg\left(B\to A\right)\land\left(B\to A\right)</math>
| &nbsp;
| &nbsp;
| '''4,5 C'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 08.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg A</math>
| width="10px" | &nbsp;
| &nbsp;
|
| '''5,7 RAA'''
|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 09.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>A\to B</math>
| width="10px" | &nbsp;
| &nbsp;
|
| '''8 DS'''
|- 
| 10.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\left(A\to B\right)\land \neg\left(A\to B\right)</math>
| &nbsp;
| &nbsp;
|
| '''9,3 C'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 11.
| style="border-right:2px solid black" | &nbsp;
| <math>\neg\neg\left(\left(A\to B\right)\lor \left(B\to A\right)\right)</math>
| width="10px" | &nbsp;
| '''1,10 RAA'''
|- 
| width="15px" | 12.
| style="border-right:2px solid black" | &nbsp;
| <math>\left(A\to B\right)\lor \left(B\to A\right)</math>
| width="10px" | &nbsp;
| '''11 DN'''
|}
|}

===Exemplo 5===
<math>\vdash \left(\left(P\to Q\right)\to P\right)\to P</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 01. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\left(P\to Q\right)\to P</math>
| width="10px" | &nbsp;
| '''Hipótese'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 02.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg P</math>
| width="10px" | &nbsp;
| &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;'''Hipótese'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 03. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>P</math>
| width="15px" | &nbsp;
| '''Hipótese'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 04. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg Q</math>
| width="15px" | &nbsp;
| '''Hipótese'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|-
| width="15px" | 05. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>P\land \neg P</math>
| width="15px" | &nbsp;
| '''3,2 C'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 06. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \neg Q</math>
| width="15px" | &nbsp;
| '''4,5 RAA'''
|-
| width="15px" | 07. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>Q</math>
| width="15px" | &nbsp;
| '''6 DN'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 08. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>P\to Q</math>
| width="15px" | &nbsp;
| '''3,7 RPC'''
|-
| width="15px" | 09. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>P</math>
| width="15px" | &nbsp;
| '''1,8 MP'''
|-
| width="15px" | 10. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg P\land P</math>
| width="15px" | &nbsp;
| '''2,9 C'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 11. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg\neg P</math>
| width="15px" | &nbsp;
| '''2, 10 RAA'''
|-
| width="15px" | 12. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>P</math>
| width="15px" | &nbsp;
| '''11 DN'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 13. 
| style="border-right:2px solid black" | &nbsp;
| <math>\left(\left(P\to Q\right)\to P\right)\to P\,\!</math>
| width="15px" | &nbsp;
| '''1, 12 RPC'''
|}
|}

===Exemplo 6===
<math>\vdash\left(\left(A\land B\right)\to C\right)\leftrightarrow \left(A\to \left(B\to C\right)\right)</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 01. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\left(A\land B\right)\to C</math>
| width="10px" | &nbsp;
| '''Hipótese'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 02.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>A</math>
| width="10px" | &nbsp;
| &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;'''Hipótese'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 03. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>B</math>
| width="15px" | &nbsp;
| '''Hipótese'''
|-
| 04.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>A\land B</math>
| &nbsp;
| '''2,3 C'''
|-
| 05.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>C</math>
| &nbsp;
| '''1,4 MP'''  
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 06.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>B\to C</math>
| width="10px" | &nbsp;
| '''3,5 RPC'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 07.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>A\to \left(B\to C\right)</math>
| width="10px" | &nbsp;
| '''2,6 RPC'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 08.
| style="border-right:2px solid black" | &nbsp;
| <math>\left(\left(A\land B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)</math>
| width="10px" | &nbsp;
| '''1,7 RPC'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
|}
{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 09. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>A\to \left(B \to C\right)</math>
| width="10px" | &nbsp;
| '''Hipótese'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 10.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>A\land B</math>
| width="10px" | &nbsp;
| &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;'''Hipótese'''
|-
| 11.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>A</math>
| &nbsp;
| '''10 S'''
|-
| 12.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>B\to C</math>
| &nbsp;
| '''9,11 MP'''
|-
| 13.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>B</math>
| &nbsp;
| '''10 S'''
|-
| 14.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>C</math>
| &nbsp;
| '''12,13 MP'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 15.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\left(A\land B\right)\to C</math>
| width="10px" | &nbsp;
| '''10,14 RPC'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 16.
| style="border-right:2px solid black" | &nbsp;
| <math>\left(A\to \left(B\to C\right)\right)\to \left(\left(A\land B\right)\to C\right)</math>
| width="10px" | &nbsp;
| '''9,15 RPC'''
|-
|17.
| style="border-right:2px solid black" | &nbsp;
| <math>\left(\left(A\land B\right)\to C\right)\leftrightarrow \left(A\to \left(B\to C\right)\right)</math>
| width="10px" | &nbsp;
| '''8,16 CB'''
|}
|}

===Exercícios===
Prove os seguintes teoremas por dedução natural:

# <math>\vdash A\leftrightarrow A</math>
# <math>\vdash A\leftrightarrow \neg \neg A</math>
# <math>\vdash \neg\left(A\leftrightarrow \neg A\right)</math>
# <math>\vdash A\to\left(B\to A\right)</math>
# <math>\vdash \left(\neg A\to A\right)\to A</math>
# <math>\vdash P\to \left(Q\to \left(P\land Q\right)\right)</math>
# <math>\vdash \left(\left(A\land B\right)\to C\right)\leftrightarrow \left(\left(A\land \neg C\right)\to \neg B\right)</math>
# <math>\vdash\left(A \to \left(B \to C \right) \ \right)\to \left(\left( A \to B \right) \to \left(A \to C \right)\right)</math>
# <math>\vdash \left( D \to \left(B \to A \right) \right) \to \left( B \to \left( D \to A \right) \right)</math>
# <math>\vdash \left(P\to Q\right)\to \left(\left(P\to \neg Q\right)\to \neg P\right)</math>
# <math>\vdash \left(A\to B\right)\to \left(\left(C\to B\right)\to \left(\left(A \lor C\right)\to B\right)\right)</math>

[[Lógica/Cálculo Proposicional Clássico/Dedução Natural - Parte II/Resolução dos Exercícios#Resolução dos Exercícios de Demonstração de Teoremas|Resolução dos Exercícios]]

{{AutoCat}}