Mostrar código-fonte de Lógica/Cálculo Quantificacional Clássico/Dedução Natural no CQC/Resolução dos exercícios

<math>\left\{\forall x\left(Px\lor Qx\right) , \neg Qa\right\}\vdash Pa</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 1.
| style="border-right:2px solid black" | &nbsp;
| <math>\forall x\left(Px\lor Qx\right)</math>
| width="15px" | &nbsp;
| '''Premissa'''
|-
| 2.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\neg Qa\,\!</math>
| &nbsp;
| '''Premissa'''
|-
| 3.
| style="border-right:2px solid black" | &nbsp;
| <math>Pa\lor Qa\,\!</math>
| width="15px" | &nbsp;
| '''1''' <math>\mathcal{E}\forall</math>
|-
| 4.
| style="border-right:2px solid black" | &nbsp;
| <math>Pa\,\!</math>
| width="15px" | &nbsp;
| '''3,2 SD'''
|}
|}



<math>\left\{\forall x\left(Ax\land Bx\right) , \left(Cx\land Dx\right)\right\}\vdash \left(Ax\land Cx\right)</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 1.
| style="border-right:2px solid black" | &nbsp;
| <math>\forall x\left(Ax\land Bx\right)</math>
| width="15px" | &nbsp;
| '''Premissa'''
|-
| 2.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\forall x\left(Bx\land Cx\right)</math>
| &nbsp;
| '''Premissa'''
|-
| 3.
| style="border-right:2px solid black" | &nbsp;
| <math>Ad\land Bd\,\!</math>
| width="15px" | &nbsp;
| '''1''' <math>\mathcal{E}\forall</math>
|-
| 4.
| style="border-right:2px solid black" | &nbsp;
| <math>Cd\land Dd\,\!</math>
| width="15px" | &nbsp;
| '''2''' <math>\mathcal{E}\forall</math>
|-
| 5.
| style="border-right:2px solid black" | &nbsp;
| <math>Ad\,\!</math>
| width="15px" | &nbsp;
| '''3 S'''
|-
| 6.
| style="border-right:2px solid black" | &nbsp;
| <math>Cd\,\!</math>
| width="15px" | &nbsp;
| '''4 S'''
|-
| 7.
| style="border-right:2px solid black" | &nbsp;
| <math>Ad\land Cd\,\!</math>
| width="15px" | &nbsp;
| '''5,6 C'''
|-
| 8.
| style="border-right:2px solid black" | &nbsp;
| <math>\forall x\left(Ax\land Cx\right)\,\!</math>
| width="15px" | &nbsp;
| '''7''' <math>\mathcal{I}\forall</math>
|}
|}


<math>\left\{\forall x\left(Ax\to Bx\right) , Al\right\}\vdash \exists x Bx</math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 1.
| style="border-right:2px solid black" | &nbsp;
| <math>\forall x\left(Ax\to Bx\right)</math>
| width="15px" | &nbsp;
| '''Premissa'''
|-
| 2.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>Al\,\!</math>
| &nbsp;
| '''Premissa'''
|-
| 3.
| style="border-right:2px solid black" | &nbsp;
| <math>Al\to Bl\,\!</math>
| width="15px" | &nbsp;
| '''1''' <math>\mathcal{E}\forall</math>
|-
| 4.
| style="border-right:2px solid black" | &nbsp;
| <math>Bl\,\!</math>
| width="15px" | &nbsp;
| '''3,2 MP'''
|-
| 5.
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x Bx\,\!</math>
| width="15px" | &nbsp;
| '''5''' <math>\mathcal{I}\exists</math>
|}
|}


<math>\exists x \left(Px \land Qx\right) \vdash \exists x Px \land \exists x Qx </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>\exists x \left(Px \land Qx\right)\,\!</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>Pa\land Qa\,\!</math>
| width="15px" | &nbsp;
| '''Hipótese para''' <math>\mathcal{E}\exists</math>
|-
| 3.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>Pa \,\!</math>
| &nbsp;
| '''2 S''' 
|-
| 4.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>Qa \,\!</math>
| &nbsp;
| '''2 S''' 
|-
| 5.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x Px \,\!</math>
| &nbsp;
| '''3''' <math>\mathcal{I}\exists</math>
|-
| 6.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x Qx \,\!</math>
| &nbsp;
| '''4''' <math>\mathcal{I}\exists</math>
|-
| 7.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x Px\land \exists x Qx \,\!</math>
| &nbsp;
| '''5,6 C'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 8.
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x Px\land \exists x Qx \,\!</math>
| &nbsp;
| '''1,2-7''' <math>\mathcal{E}\exists</math>
|}
|}


<math>\left\{\exists x Px , \forall x Qx \right\}\vdash \exists x \left(Px \land Qx\right) </math>

{|- cellspacing="0" cellpadding="0"
| width="20px" | &nbsp; ||
{|- cellspacing="0" cellpadding="4" border="0"
| 1.
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x Px\,\!</math>
| width="15px" | &nbsp;
| '''Premissa'''
|-
| 2.
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\forall x Qx \,\!</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>Pa\,\!</math>
| width="15px" | &nbsp;
| '''Hipótese para''' <math>\mathcal{E}\exists</math>
|-
| 4.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>Qa \,\!</math>
| &nbsp;
| '''2''' <math>\mathcal{E}\forall</math>
|-
| 5.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>Pa\land Qa \,\!</math>
| &nbsp;
| '''3,4 C''' 
|-
| 6.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x \left(Px\land Qx\right)</math>
| &nbsp;
| '''5''' <math>\mathcal{I}\exists</math>
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 7.
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x \left(Px\land Qx\right)</math>
| &nbsp;
| &nbsp; &nbsp; &nbsp; '''1,3-6''' <math>\mathcal{E}\exists</math>
|}
|}
===Exercícios de teoremas===

<math>\vdash \exists x Px\to \neg \forall x\neg Px</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>\exists x Px \,\!</math>
| width="10px" | &nbsp;
| &nbsp;  &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"
| 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>\forall x\neg Px\,\!</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> \neg \exists x Px\,\!</math>
| &nbsp;
|
| '''2 IQ'''
|-
| 4.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x Px\land \neg \exists x Px\,\!</math>
| &nbsp;
|
| '''1,3 C'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 5.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \forall x\neg Px\,\!</math>
| width="10px" | &nbsp;
| &nbsp;
|
| '''2,4 RAA'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 6.
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x Px\to \neg \forall x\neg Px</math>
| width="10px" | &nbsp;
| '''1,5 RPC'''
|}
|}


<math>\vdash \forall x\left(Px\to Q\right)\to \exists x\left(Px\to Q\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>\forall x\left(Px\to Q\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>Pa\to Q\,\!</math>
| width="10px" | &nbsp;
| '''1''' <math>\mathcal{E}\forall</math>
|- 
| width="15px" | 3.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>\exists x\left(Px\to Q\right)\,\!</math>
| width="10px" | &nbsp;
| '''2''' <math>\mathcal{I}\exists</math>
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 4.
| style="border-right:2px solid black" | &nbsp;
| <math>\forall x\left(Px\to Q\right)\to \exists x\left(Px\to Q\right)</math>
| width="10px" | &nbsp;
| '''1,3 RPC'''
|}
|}


<math>\vdash \exists x \exists y Pxy \leftrightarrow \exists y \exists x Pxy</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>\exists x \exists y Pxy\,\!</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>\exists y Pxy\,\!</math>
| width="10px" | &nbsp;
| &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;'''Hipótese para''' <math>\mathcal{E}\exists</math>
|- 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>Pab\,\!</math>
| width="15px" | &nbsp;
| '''Hipótese para''' <math>\mathcal{E}\exists</math>
|-
| 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>\exists x Pxb\,\!</math>
| &nbsp;
| '''3''' <math>\mathcal{I}\exists</math>
|-
| 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>\exists y \exists x Pxy\,\!</math>
| &nbsp;
| '''4''' <math>\mathcal{I}\exists</math> 
|- 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>\exists y \exists x Pxy\,\!</math>
| width="10px" | &nbsp;
| '''2,3-5''' <math>\mathcal{E}\exists</math>
|- 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>\exists y \exists x Pxy\,\!\,\!</math>
| width="10px" | &nbsp;
| '''1,2-6''' <math>\mathcal{E}\exists</math>
|- 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>\exists y \exists x Pxy \to \exists y \exists x Pxy\,\!</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>\exists x \exists y Pxy\,\!</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>\exists x Pxa\,\!</math>
| width="10px" | &nbsp;
| &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;'''Hipótese para''' <math>\mathcal{E}\exists</math>
|- 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" | 11. 
| 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>Pba\,\!</math>
| width="15px" | &nbsp;
| '''Hipótese para''' <math>\mathcal{E}\exists</math>
|-
| 12.
| 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>\exists y Pyb\,\!</math>
| &nbsp;
| '''11''' <math>\mathcal{I}\exists</math>
|-
| 13.
| 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>\exists x \exists y Pxy\,\!</math>
| &nbsp;
| '''12''' <math>\mathcal{I}\exists</math> 
|- 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" | 14.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x \exists y Pxy\,\!</math>
| width="10px" | &nbsp;
| '''10,11-13''' <math>\mathcal{E}\exists</math>
|- 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>\exists x \exists y Pxy\,\!\,\!</math>
| width="10px" | &nbsp;
| '''9,10-14''' <math>\mathcal{E}\exists</math>
|- 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>\exists y \exists x Pxy\to \exists x \exists y Pxy \,\!</math>
| width="10px" | &nbsp;
| '''1,7 RPC'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
|17.
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x \exists y Pxy \leftrightarrow \exists y \exists x Pxy\,\!</math>
| width="10px" | &nbsp;
| '''8,16 CB'''
|}
|}


<math>\vdash \left(\forall x Px \land \forall x Qx\right) \leftrightarrow \forall x \left(Px \land Qx\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>\forall x Px \land \forall x Qx\,\!</math>
| width="10px" | &nbsp;
|   &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"
| width="15px" | 02.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>\forall x Px\,\!</math>
| width="10px" | &nbsp;
|   &nbsp; &nbsp; &nbsp; '''1 S'''
|- 
| 03.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>\forall x Qx\,\!</math>
| width="10px" | &nbsp;
|   &nbsp; &nbsp; &nbsp; '''1 S'''
|- 
| 04.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>Pa\,\!</math>
| width="10px" | &nbsp;
|   &nbsp; &nbsp; &nbsp; '''2''' <math>\mathcal{E}\forall</math>
|- 
| 05.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>Qa\,\!</math>
| width="10px" | &nbsp;
|   &nbsp; &nbsp; &nbsp; '''3''' <math>\mathcal{E}\forall</math>
|- 
| 06.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>Pa\land Qa\,\!</math>
| width="10px" | &nbsp;
|   &nbsp; &nbsp; &nbsp; '''4,5 C'''
|- 
| 07.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>\forall x\left(Px\land Qx\right)\,\!</math>
| width="10px" | &nbsp;
|   &nbsp; &nbsp; &nbsp; '''2''' <math>\mathcal{I}\forall</math>
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 08.
| style="border-right:2px solid black" | &nbsp;
| <math>\left(\forall x Px \land \forall x Qx\right) \to \forall x \left(Px \land Qx\right)\,\!</math>
| width="10px" | &nbsp;
| '''1,7 RPC'''
|}
{|- 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>\forall x \left(Px \land Qx\right)\,\!</math>
| width="10px" | &nbsp;
|  &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"
| width="15px" | 10.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>Pa\land Qa\,\!</math>
| width="10px" | &nbsp;
|  &nbsp; &nbsp;  &nbsp; '''9''' <math>\mathcal{E}\forall</math>
|- 
| 11.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>Pa\,\!</math>
| width="10px" | &nbsp;
|  &nbsp; &nbsp;  &nbsp; '''10 S'''
|- 
| 12.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>\forall x Px\,\!</math>
| width="10px" | &nbsp;
|  &nbsp; &nbsp;  &nbsp; '''11''' <math>\mathcal{I}\forall</math>
|- 
| 13.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>Qa\,\!</math>
| width="10px" | &nbsp;
|  &nbsp; &nbsp;  &nbsp; '''10 S'''
|- 
| 14.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>\forall x Qx\,\!</math>
| width="10px" | &nbsp;
|  &nbsp; &nbsp;  &nbsp; '''13''' <math>\mathcal{I}\forall</math>
|- 
| 15.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
|<math>\forall x Qx\,\!</math>
| width="10px" | &nbsp;
|  &nbsp; &nbsp;  &nbsp; '''13''' <math>\mathcal{I}\forall</math>
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 16.
| style="border-right:2px solid black" | &nbsp;
| <math>\forall x \left(Px \land Qx\right)\to \left(\forall x Px \land \forall x Qx\right)\,\!</math>
| width="10px" | &nbsp;
| '''4,5 RPC'''
|-
| width="15px" | 17.
| style="border-right:2px solid black" | &nbsp;
| <math>\left(\forall x Px \land \forall x Qx\right) \leftrightarrow \forall x \left(Px \land Qx\right)</math>
| width="10px" | &nbsp;
| '''8,16 CB'''
|}
|}


<math>\vdash \left(P \land \exists x Qx\right) \leftrightarrow \exists x \left(P \land Qx\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>P \land \exists x Qx</math>
| width="10px" | &nbsp;
| &nbsp;  &nbsp; &nbsp;  &nbsp; '''Hipótese'''
|
|- 
| 02.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x Qx \,\!</math>
| &nbsp;
| &nbsp;  &nbsp; &nbsp;  '''1 S'''
|}
{|- 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-bottom:2px solid black;" | <math>Qa\,\!</math>
| width="15px" | &nbsp;
|
| '''Hipótese para''' <math>\mathcal{E}\exists</math>
|-
| 04.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>P\,\!</math>
| &nbsp;
|
| '''1 S'''
|- 
| 05.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>P\land Qa\,\!</math>
| &nbsp;
| &nbsp;
| '''4,3 C'''
|- 
| 06.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x\left(P\land Qa\right)\,\!</math>
| &nbsp;
| &nbsp;
| '''5''' <math>\mathcal{I}\exists</math>
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 07.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x\left(P\land Qa\right)\,\!</math>
| width="10px" | &nbsp;
| &nbsp;
|
| '''2,3-6''' <math>\mathcal{E}\exists</math>
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 08.
| style="border-right:2px solid black" | &nbsp;
| <math>\left(P \land \exists x Qx\right) \to \exists x \left(P \land Qx\right)</math>
| width="10px" | &nbsp;
| '''1,7 RPC'''
|}
{|- 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>\exists x \left(P \land Qx\right)</math>
| width="10px" | &nbsp;
| &nbsp;  &nbsp; &nbsp;  &nbsp; '''Hipótese'''
|-
|&nbsp;  &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| &nbsp;  &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>P\land Qa\,\!</math>
| width="15px" | &nbsp;
|
| '''Hipótese para''' <math>\mathcal{E}\exists</math>
|-
| 11.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>Qa\,\!</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>\exists x Qx\,\!</math>
| &nbsp;
| &nbsp;
| '''11''' <math>\mathcal{I}\exists</math>
|- 
| 13.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>P\,\!</math>
| &nbsp;
| &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>P\land \exists x Qx\,\!</math>
| &nbsp;
| &nbsp;
| '''12,13 C'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 15.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>P\land \exists x Qx\,\!</math>
| width="10px" | &nbsp;
| &nbsp;
|
| '''9,10-14''' <math>\mathcal{E}\exists</math>
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 16.
| style="border-right:2px solid black" | &nbsp;
| <math> \exists x \left(P \land Qx\right)\to \left(P \land \exists x Qx\right) </math>
| width="10px" | &nbsp;
| '''9,15 RPC'''
|- 
| width="15px" | 17.
| style="border-right:2px solid black" | &nbsp;
| <math>\left(P \land \exists x Qx\right) \leftrightarrow \exists x \left(P \land Qx\right)</math>
| width="10px" | &nbsp;
| '''8,16 CB'''
|}
|}


<math>\vdash \left(P \lor \forall x Qx\right) \leftrightarrow \forall x (P \lor Qx) </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>P \lor \forall x Qx \,\!</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 \forall x\left(P\lor Qx\right)\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''Hipótese'''
|- 
| width="15px" | 03.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x\neg\left(P\lor Qx\right)\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''2 IQ'''
|- 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" | 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-bottom:2px solid black;" | <math>\neg \left(P\lor Qa\right)\,\!</math>
| width="15px" | &nbsp;
| '''Hipótese para''' <math>\mathcal{E}\exists</math>
|-
| 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>\neg P\land \neg Qa\,\!</math>
| &nbsp;
| '''4 DM'''
|-
| 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 Qa \,\!</math>
| &nbsp;
| '''5 S'''  
|-
| 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>\neg P\,\!</math>
| &nbsp;
| '''5 S'''
|-
| 08.
| 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>\forall x Qx\,\!</math>
| &nbsp;
| '''1,7 SD'''
|-
| 09.
| 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>\exists x \neg Qx\,\!</math>
| &nbsp;
| '''6''' <math>\mathcal{I}\exists</math>
|-
| 10.
| 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 \forall x Qx\,\!</math>
| &nbsp;
| '''9 IQ''' 
|-
| 11.
| 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>\forall x Qx\land \neg \forall x Qx\,\!</math>
| &nbsp;
| '''8,10 C'''
|- 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" | 12.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\forall x Qx\land \neg \forall x Qx\,\!</math>
| width="10px" | &nbsp;
| '''3,4-11''' <math>\mathcal{E}\exists</math>
|- 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" | 13.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \neg \forall x\left(P\lor Qx\right)\,\!</math>
| width="10px" | &nbsp;
| '''2,17 RAA'''
|- 
| width="15px" | 14.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x\left(Px\lor Qx\right)\,\!</math>
| width="10px" | &nbsp;
| '''13 DN'''
|- style="height:10px"
|
| style="border-right:2px solid black" | &nbsp;
|
|
|
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 15.
| style="border-right:2px solid black" | &nbsp;
| <math>\left(P \lor \forall x Qx\right) \to \forall x \left(P \lor Qx\right)</math>
| width="10px" | &nbsp;
| '''1,19 RPC'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| width="15px" | 16. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-bottom:2px solid black;" | <math>\forall x \left(P \lor Qx\right) \,\!</math>
| width="10px" | &nbsp;
| '''Hipótese'''
|-
| width="15px" | 17. 
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>P \lor Qa \,\!</math>
| width="10px" | &nbsp;
| '''16''' <math>\mathcal{E}\forall</math>
|- 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" | 18.
| 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 \left(P\lor \forall x Qx\right)\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''Hipótese'''
|- 
| width="15px" | 19.
| 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 \neg \forall x Qx\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''18 DM'''
|- 
| 20.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg P\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''19 S'''
|- 
| 21.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>Qa\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''17,20 SD'''
|- 
| 22.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\forall Qx\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''21''' <math>\mathcal{I}\forall</math>
|- 
| 23.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \forall Qx\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''19 S'''
|- 
| 24.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\forall Qx\land \neg \forall Qx\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''22,23 C'''
|- 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"
| 25.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\neg \neg \left(P\lor \forall x Qx\right)\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''18,24 RAA'''
|- 
| 26.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\left(P\lor \forall x Qx\right)\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''25 DN'''
|}
{|- cellspacing="0" cellpadding="4" border="0"
| 27.
| style="border-right:2px solid black" | &nbsp;
| <math>\forall x\left(P\lor Qx\right)\to\left(P\lor \forall x Qx\right)\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''16,26 RPC'''
|- 
| 28.
| style="border-right:2px solid black" | &nbsp;
| <math>\left(P \lor \forall x Qx\right) \leftrightarrow \forall x (P \lor Qx)\,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''15,27 CB'''
|}
|}


<math>\vdash \exists x (Px \rightarrow Q) \to (\forall x Px \rightarrow Q) </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>\exists x (Px \rightarrow Q) \,\!</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>\forall x Px \,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &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>Pa \,\!</math>
| width="10px" | &nbsp;
| &nbsp; &nbsp; &nbsp; '''2''' <math>\mathcal{E}\forall</math>
|- 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" | 4. 
| 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>Pa\to Q \,\!</math>
| width="15px" | &nbsp;
| '''Hipótese para''' <math>\mathcal{E}\exists</math>
|-
| 5.
| 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>
| '''4,3 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" | 6.
| 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="10px" | &nbsp;
| '''1,4-5''' <math>\mathcal{E}\exists</math>
|- 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" | 7.
| style="border-right:2px solid black" | &nbsp;
| style="border-right:2px solid black" | &nbsp;
| <math>\forall x Px\to Q\,\!</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" | 8.
| style="border-right:2px solid black" | &nbsp;
| <math>\exists x (Px \rightarrow Q) \to (\forall x Px \rightarrow Q)\,\!</math>
| width="10px" | &nbsp;
| '''1,7 RPC'''
|}
|}

{{AutoCat}}