A lógica C1
m |
|||
(9 edições intermediárias de 2 usuários não apresentadas) | |||
Linha 1: | Linha 1: | ||
− | C1 é | + | C1 é historicamente importante porque foi a primeira lógica paraconsistente a ser apresentada por Newton C. A. da Costa [http://pt.wikipedia.org/wiki/Newton_da_Costa] em 1963. |
<ul> | <ul> | ||
Linha 5: | Linha 5: | ||
<li> O significado de ◦A é “A é consistente”.</li> | <li> O significado de ◦A é “A é consistente”.</li> | ||
<li> O conectivo consistência "◦" não é um conectivo primitivo, | <li> O conectivo consistência "◦" não é um conectivo primitivo, | ||
− | mas uma abreviação: </ | + | mas uma abreviação: <br /> |
− | + | ◦A = ¬(A ∧ ¬A) </li> | |
</ul> | </ul> | ||
<br /> | <br /> | ||
− | + | Axiomas de C1: | |
<ul> | <ul> | ||
Linha 24: | Linha 24: | ||
<li>(Ax10) α ∨ ¬α </li> | <li>(Ax10) α ∨ ¬α </li> | ||
<li>(Ax11) ¬¬α → α </li> | <li>(Ax11) ¬¬α → α </li> | ||
− | |||
− | |||
− | |||
− | |||
<li>(bc1) ◦α → (α → (¬α → β)) </li> | <li>(bc1) ◦α → (α → (¬α → β)) </li> | ||
<li>(ca1) (◦α ∧ ◦β) → ◦(α ∧ β)</li> | <li>(ca1) (◦α ∧ ◦β) → ◦(α ∧ β)</li> | ||
Linha 48: | Linha 44: | ||
− | Para obter a lógica proposicional clássica (CPL) de C1, removem-se os ◦- | + | Para obter a lógica proposicional clássica (CPL) de C1, removem-se os ◦-axiomas: (bc1), (ca1), (ca2) e (ca3) e adiciona-se a lei da explosão: |
(exp) α → (¬α → β) | (exp) α → (¬α → β) | ||
Linha 70: | Linha 66: | ||
</ul> | </ul> | ||
+ | <br /> | ||
+ | <br /> | ||
+ | '''Regras de implementação:''' | ||
+ | <br /> | ||
+ | |||
+ | |||
+ | <table width="420px" border="1" style="font-family:Arial;font-size:10pt;border-collapse:collapse; border:#FFF;"> | ||
+ | <tr> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;" width="70px">FA → B</td> | ||
+ | <td align="left" rowspan="3" valign="middle" width="70px">(F→)</td> | ||
+ | <td align="center" width="70px">TA → B</td> | ||
+ | <td align="left" rowspan="3" valign="middle" width="70px">(T→<sub>1</sub>)</td> | ||
+ | <td align="center" width="70px">TA → B</td> | ||
+ | <td align="left" rowspan="3" valign="middle" width="70px">(T→<sub>2</sub>)</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center">TA</td> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">TA</td> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">FB</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center">FB</td> | ||
+ | <td align="center">TB</td> | ||
+ | <td align="center">FA</td> | ||
+ | </tr> | ||
+ | <tr><td colspan="6"> </td></tr> | ||
+ | <tr> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">TA ∧ B</td> | ||
+ | <td align="left" rowspan="3" valign="middle">(T∧)</td> | ||
+ | <td align="center">FA ∧ B</td> | ||
+ | <td align="left" rowspan="3" valign="middle">(F∧<sub>1</sub>)</td> | ||
+ | <td align="center">FA ∧ B</td> | ||
+ | <td align="left" rowspan="3" valign="middle">(F∧<sub>2</sub>)</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center">TA</td> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">TA</td> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">TB</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center">TB</td> | ||
+ | <td align="center">FB</td> | ||
+ | <td align="center">FA</td> | ||
+ | </tr> | ||
+ | <tr><td colspan="6"> </td></tr> | ||
+ | <tr> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">FA ∨ B</td> | ||
+ | <td align="left" rowspan="3" valign="middle">(F∨)</td> | ||
+ | <td align="center">TA ∨ B</td> | ||
+ | <td align="left" rowspan="3" valign="middle">(T∨<sub>1</sub>)</td> | ||
+ | <td align="center">TA ∨ B</td> | ||
+ | <td align="left" rowspan="3" valign="middle">(T∨<sub>2</sub>)</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center">FA</td> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">FA</td> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">FB</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center">FB</td> | ||
+ | <td align="center">TB</td> | ||
+ | <td align="center">TA</td> | ||
+ | </tr> | ||
+ | <tr><td colspan="6"> </td></tr> | ||
+ | <tr> | ||
+ | <td align="center">/\</td> | ||
+ | <td align="left" rowspan="3" valign="middle">(PB)</td> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">F ¬A</td> | ||
+ | <td align="left" rowspan="3" valign="middle">(F¬)</td> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">T ¬¬A</td> | ||
+ | <td align="left" rowspan="3" valign="middle">(T¬¬)</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center">TA FA</td> | ||
+ | <td align="center">TA</td> | ||
+ | <td align="center">TA</td> | ||
+ | </tr> | ||
+ | <tr><td colspan="6"> </td></tr> | ||
+ | <tr> | ||
+ | <td align="center"> </td> | ||
+ | <td align="left" rowspan="4" valign="middle">(T ◦¬)</td> | ||
+ | <td align="center">T ¬(A Ø B)</td> | ||
+ | <td align="left" rowspan="4" valign="middle">(T ¯<sub>1</sub>)</td> | ||
+ | <td align="center">T ¬(A Ø B)</td> | ||
+ | <td align="left" rowspan="4" valign="middle">(T ¯<sub>2</sub>)</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center">T ◦A</td> | ||
+ | <td align="center">T A Ø B</td> | ||
+ | <td align="center">T A Ø B</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">T ¬A</td> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">T ◦A</td> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">T ◦B</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center">FA</td> | ||
+ | <td align="center">F ◦B</td> | ||
+ | <td align="center">F ◦A</td> | ||
+ | </tr> | ||
+ | </table> | ||
− | |||
<br /> | <br /> | ||
− | + | <span style="font-family:Arial;font-size:10pt;font-weight:bold;">Regras diferentes</span> | |
+ | |||
+ | <table width="280px" border="1" style="font-family:Arial;font-size:10pt;border-collapse:collapse; border:#FFF;"> | ||
+ | <tr> | ||
+ | <td align="center"> </td> | ||
+ | <td align="left" rowspan="4" valign="middle">(F ◦Ø<sub>1</sub>) --> </td> | ||
+ | <td align="center"><span style="color:#CC0033">T ¬(A Ø B)</span></td> | ||
+ | <td align="left" rowspan="4" valign="middle">(T ¯<sub>1</sub>)</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center"><span style="color:#FF0066">F ◦(A Ø B)</span></td> | ||
+ | <td align="center"><span style="color:#000099">T A Ø B</span></td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">T ◦A</td> | ||
+ | <td align="center" style="border-bottom:solid #000000 1pt;">T ◦A</td> | ||
+ | </tr> | ||
+ | <tr> | ||
+ | <td align="center">F ◦B</td> | ||
+ | <td align="center">F ◦B</td> | ||
+ | </tr> | ||
+ | </table> | ||
+ | |||
<br /> | <br /> | ||
− | + | <span style="font-family:Arial;font-size:10pt;"> | |
+ | Onde <span style="color:#FF0066">F ◦(A Ø B)</span> = F ¬((A Ø B) ∧ ¬(A Ø B)) | ||
<br /> | <br /> | ||
− | CARNIELLI, Walter;CONIGLIO, MARCELO E.;MARCOS, João. <b>Logics of formal inconsistency</b>. Disponível em: <ftp://logica.cle.unicamp.br/pub/e-prints/vol.5,n.1,2005-revised.pdf>. Acesso em 09 set. 2009. | + | Usando (F¬): T (A Ø B) ∧ ¬(A Ø B) |
+ | <br /> | ||
+ | Usando (T∧): <span style="color:#000099">T A Ø B</span> e <span style="color:#CC0033">T ¬(A Ø B)</span> | ||
+ | <br /> | ||
+ | O mesmo processo para as 2 regras: (F ◦Ø<sub>1</sub>) e (F ◦Ø<sub>2</sub>) | ||
+ | </span> | ||
+ | <br /><br /><br /> | ||
+ | |||
+ | '''Referências:''' | ||
+ | <br /> | ||
+ | <ul> | ||
+ | <li>CARNIELLI, Walter; CONIGLIO, Marcelo E.; MARCOS, João. Logics of Formal Inconsistency. 2. ed. São Paulo: Springer-Verlag, 2007 p. 15-107. </li> | ||
+ | <li>KRAUSE, Décio. <b>A Lógica Paraconsistente</b>. Disponível em: <http://www.cfh.ufsc.br/~dkrause/LogicaI/ParaconsistenteSA.htm>. Acesso em 09 set. 2009.</li> | ||
+ | <li>CARNIELLI, Walter;CONIGLIO, MARCELO E.;MARCOS, João. <b>Logics of formal inconsistency</b>. Disponível em: <ftp://logica.cle.unicamp.br/pub/e-prints/vol.5,n.1,2005-revised.pdf>. Acesso em 09 set. 2009.</li> | ||
+ | <li>NETO, ADOLFO G. S. S. ; KAESTNER, CELSO A. A. FINGER, Marcelo. <b>A KE tableau system for C1</b>. Disponível em: <http://www.dainf.ct.utfpr.edu.br/~adolfo/publications/2009/Slides_CLEAIPS_2009_NetoKaestnerFinger.pdf>. Acesso em 10 set. 2009.</li> | ||
+ | </ul> | ||
<br /> | <br /> |
Edição atual tal como 22h11min de 13 de setembro de 2009
C1 é historicamente importante porque foi a primeira lógica paraconsistente a ser apresentada por Newton C. A. da Costa [1] em 1963.
- O operador de consistência (◦) foi introduzido.
- O significado de ◦A é “A é consistente”.
- O conectivo consistência "◦" não é um conectivo primitivo,
mas uma abreviação:
◦A = ¬(A ∧ ¬A)
Axiomas de C1:
- (Ax1) α → (β → α)
- (Ax2) (α → β) → ((α → (β → γ)) → (α → γ))
- (Ax3) α → (β → (α ∧ β))
- (Ax4) (α∧ β) → α
- (Ax5) (α ∧ β) → β
- (Ax6) α → (α ∨ β)
- (Ax7) β → (α ∨ β)
- (Ax8) (α → γ) → ((β → γ) → ((α ∨ β) → γ))
- (Ax9) α ∨ (α → β)
- (Ax10) α ∨ ¬α
- (Ax11) ¬¬α → α
- (bc1) ◦α → (α → (¬α → β))
- (ca1) (◦α ∧ ◦β) → ◦(α ∧ β)
- (ca2) (◦α ∧ ◦β) → ◦(α ∨ β)
- (ca3) (◦α ∧ ◦β) → ◦(α → β)
Regra de inferência (MP:)
α, α → β |
β |
Para obter a lógica proposicional clássica (CPL) de C1, removem-se os ◦-axiomas: (bc1), (ca1), (ca2) e (ca3) e adiciona-se a lei da explosão:
(exp) α → (¬α → β)
“Princípio da Explosão”, ou Regra de Duns Scotus: uma contradição implica qualquer proposição. Dito de modo mais preciso, se em um sistema dedutivo S fundamentado na lógica clássica derivarmos duas proposições contraditórias (uma sendo a negação da outra), então toda fórmula (expressão bem formada) da linguagem de S resulta ser teorema de S. Neste caso, diz-se que S é trivial. |
Valoração para C1:
- v(α1 ∧ α2 ) = 1 ⇐⇒ v(α1 ) = 1 and v(α2) = 1;
- v(α1 ∨ α2 ) = 1 ⇐⇒ v(α1 ) = 1 or v(α2) = 1;
- v(α1 → α2 ) = 1 ⇐⇒ v(α1 ) = 0 or v(α2) = 1;
- v(¬α) = 0 ⇒ v(α) = 1;
- v(¬¬α) = 1 ⇒ v(α) = 1;
- v(◦α) = 1 ⇒ v(α) = 0 or v (¬α) = 0;
- v(◦(α Ø β)) = 0 ⇒ v(◦α) = 0 or v(◦β) = 0, para Ø ∈ {∧, ∨, →};
Regras de implementação:
FA → B | (F→) | TA → B | (T→1) | TA → B | (T→2) |
TA | TA | FB | |||
FB | TB | FA | |||
TA ∧ B | (T∧) | FA ∧ B | (F∧1) | FA ∧ B | (F∧2) |
TA | TA | TB | |||
TB | FB | FA | |||
FA ∨ B | (F∨) | TA ∨ B | (T∨1) | TA ∨ B | (T∨2) |
FA | FA | FB | |||
FB | TB | TA | |||
/\ | (PB) | F ¬A | (F¬) | T ¬¬A | (T¬¬) |
TA FA | TA | TA | |||
(T ◦¬) | T ¬(A Ø B) | (T ¬Ø1) | T ¬(A Ø B) | (T ¬Ø2) | |
T ◦A | T A Ø B | T A Ø B | |||
T ¬A | T ◦A | T ◦B | |||
FA | F ◦B | F ◦A |
Regras diferentes
(F ◦Ø1) --> | T ¬(A Ø B) | (T ¬Ø1) | |
F ◦(A Ø B) | T A Ø B | ||
T ◦A | T ◦A | ||
F ◦B | F ◦B |
Onde F ◦(A Ø B) = F ¬((A Ø B) ∧ ¬(A Ø B))
Usando (F¬): T (A Ø B) ∧ ¬(A Ø B)
Usando (T∧): T A Ø B e T ¬(A Ø B)
O mesmo processo para as 2 regras: (F ◦Ø1) e (F ◦Ø2)
Referências:
- CARNIELLI, Walter; CONIGLIO, Marcelo E.; MARCOS, João. Logics of Formal Inconsistency. 2. ed. São Paulo: Springer-Verlag, 2007 p. 15-107.
- KRAUSE, Décio. A Lógica Paraconsistente. Disponível em: <http://www.cfh.ufsc.br/~dkrause/LogicaI/ParaconsistenteSA.htm>. Acesso em 09 set. 2009.
- CARNIELLI, Walter;CONIGLIO, MARCELO E.;MARCOS, João. Logics of formal inconsistency. Disponível em: <ftp://logica.cle.unicamp.br/pub/e-prints/vol.5,n.1,2005-revised.pdf>. Acesso em 09 set. 2009.
- NETO, ADOLFO G. S. S. ; KAESTNER, CELSO A. A. FINGER, Marcelo. A KE tableau system for C1. Disponível em: <http://www.dainf.ct.utfpr.edu.br/~adolfo/publications/2009/Slides_CLEAIPS_2009_NetoKaestnerFinger.pdf>. Acesso em 10 set. 2009.