A lógica C1

De Wiki DAINF
(Diferença entre revisões)
m
 
(25 edições intermediárias de 2 usuários não apresentadas)
Linha 1: Linha 1:
−
C1 é históricamente importante porque foi a primeira lógica paraconsistente a ser apresentada por Newton C. A. da Costa em 1963.
+
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: </li>
+
mas uma abreviação: <br />
−
<li> ◦A = ¬(A ∧ ¬A) </li>
+
◦A = ¬(A ∧ ¬A) </li>
 
</ul>
 
</ul>
  
−
C1 Axiomas:
+
<br />
−
 
+
Axiomas de C1:
  
 
<ul>
 
<ul>
Linha 24: Linha 24:
 
<li>(Ax10) α ∨ ¬α </li>
 
<li>(Ax10) α ∨ ¬α </li>
 
<li>(Ax11) ¬¬α → α </li>
 
<li>(Ax11) ¬¬α → α </li>
−
</ul>
 
−
 
−
Axiom  schemas:
 
−
<ul>
 
 
<li>(bc1) ◦α → (α → (¬α → β)) </li>
 
<li>(bc1) ◦α → (α → (¬α → β)) </li>
 
<li>(ca1) (◦α ∧ ◦β) → ◦(α ∧ β)</li>
 
<li>(ca1) (◦α ∧ ◦β) → ◦(α ∧ β)</li>
Linha 34: Linha 30:
 
</ul>
 
</ul>
  
−
Inference rule (MP:)  
+
Regra de inferência (MP:)  
−
          α, α → β
+
<table width="100px">
−
          _________
+
<tr>
−
          β  
+
  <td>α, α → β</td>
 +
</tr>
 +
<tr>
 +
  <td><hr /></td>
 +
</tr>
 +
<tr>
 +
  <td>β</td>
 +
</tr>
 +
</table>
  
−
Para obter a lógica proposicional clássica (CPL) de C1:, remove-se os ◦-aximas:  (bc1), (ca1), (ca2) e (ca3),  adiciona-se a lei da explosão:
 
  
−
    (exp) α → (¬α → β)
+
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) α → (¬α → β)
  
 +
<table style="border:1px solid;border-collapse:collapsed;">
 +
<tr><td>
 
“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.  
 
“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.  
−
 
+
</td></tr>
 +
</table>
  
 
Valoração para C1:
 
Valoração para C1:
Linha 59: 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">&nbsp;</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">&nbsp;</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">&nbsp;</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">&nbsp;</td></tr>
 +
  <tr>
 +
  <td align="center">&nbsp;</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>
  
−
'''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.
 
 
<br />
 
<br />
−
http://www.cfh.ufsc.br/~dkrause/LogicaI/ParaconsistenteSA.htm
+
<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">&nbsp;</td>
 +
  <td align="left" rowspan="4" valign="middle">(F ◦Ø<sub>1</sub>)&nbsp;&nbsp;--> </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 />
−
ftp://logica.cle.unicamp.br/pub/e-prints/vol.5,n.1,2005-revised.pdf
+
<span style="font-family:Arial;font-size:10pt;">
 +
Onde <span style="color:#FF0066">F ◦(A Ø B)</span> = F ¬((A Ø B) ∧ ¬(A Ø B))
 +
<br />
 +
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:


Obtida de "http://dainf.ct.utfpr.edu.br/wiki/index.php?title=A_l%C3%B3gica_C1&oldid=2400"
Ferramentas pessoais