A lógica C1

De Wiki DAINF
(Diferença entre revisões)
Linha 9: Linha 9:
 
</ul>
 
</ul>
  
          C1 Axiom schemas (ftp://logica.cle.unicamp.br/pub/e-prints/vol.5,n.1,2005-revised.pdf):  
+
C1 Axiomas:
http://www.cle.unicamp.br/e-prints/vol_5,n_1,2005.html
+
 
  
 
<ul>
 
<ul>
Linha 39: Linha 39:
 
           β  
 
           β  
  
Para obter a lógica proposicional clássica (CPL) de C1:, remove-se os ◦-aximas:  (bc1), (ca1), (ca2) e (ca3)
+
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:
,  adiciona-se a lei da explosão:
+
 
 
     (exp) α → (¬α → β)
 
     (exp) α → (¬α → β)
  
Linha 49: Linha 49:
 
Valoração para C1:
 
Valoração para C1:
  
v (α1 ∧ α2 ) = 1 ⇐⇒ v (α1 ) = 1 and v (α2 ) = 1;
+
<ul>
v (α1 ∨ α2 ) = 1 ⇐⇒ v (α1 ) = 1 or v (α2 ) = 1;
+
<li>v(α1 ∧ α2 ) = 1 ⇐⇒ v(α1 ) = 1 and v(α2) = 1;</li>
v (α1 → α2 ) = 1 ⇐⇒ v (α1 ) = 0 or v (α2 ) = 1;
+
<li>v(α1 ∨ α2 ) = 1 ⇐⇒ v(α1 ) = 1 or v(α2) = 1;</li>
v (¬α) = 0 ⇒ v (α) = 1;
+
<li>v(α1 → α2 ) = 1 ⇐⇒ v(α1 ) = 0 or v(α2) = 1;</li>
v (¬¬α) = 1 ⇒ v (α) = 1;
+
<li>v(¬α) = 0 ⇒ v(α) = 1;</li>
v (◦α) = 1 ⇒ v (α) = 0 or v (¬α) = 0.
+
<li>v(¬¬α) = 1 ⇒ v(α) = 1;</li>
v (◦(α Ø  β)) = 0 ⇒ v (◦α) = 0 or v (◦β) = 0, para Ø ∈ {∧, ∨, →};
+
<li>v(◦α) = 1 ⇒ v(α) = 0 or v (¬α) = 0;</li>
 
+
<li>v(◦(α Ø  β)) = 0 ⇒ v(◦α) = 0 or v(◦β) = 0, para Ø ∈ {∧, ∨, →};</li>
 +
</ul>
  
  
 
'''Referências:'''
 
'''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.
+
CARNIELLI, Walter; CONIGLIO, Marcelo E.; MARCOS, João. Logics of Formal Inconsistency. 2. ed. São Paulo:  Springer-Verlag, 2007 p. 15-107.  
 +
<br />
 
http://www.cfh.ufsc.br/~dkrause/LogicaI/ParaconsistenteSA.htm
 
http://www.cfh.ufsc.br/~dkrause/LogicaI/ParaconsistenteSA.htm
 +
<br />
 +
ftp://logica.cle.unicamp.br/pub/e-prints/vol.5,n.1,2005-revised.pdf
 +
<br />

Edição de 12h24min de 10 de setembro de 2009

C1 é históricamente importante porque foi a primeira lógica paraconsistente a ser apresentada por Newton C. A. da Costa 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)

C1 Axiomas:


  • (Ax1) α → (β → α)
  • (Ax2) (α → β) → ((α → (β → γ)) → (α → γ))
  • (Ax3) α → (β → (α ∧ β))
  • (Ax4) (α∧ β) → α
  • (Ax5) (α ∧ β) → β
  • (Ax6) α → (α ∨ β)
  • (Ax7) β → (α ∨ β)
  • (Ax8) (α → γ) → ((β → γ) → ((α ∨ β) → γ))
  • (Ax9) α ∨ (α → β)
  • (Ax10) α ∨ ¬α
  • (Ax11) ¬¬α → α

Axiom schemas:

  • (bc1) ◦α → (α → (¬α → β))
  • (ca1) (◦α ∧ ◦β) → ◦(α ∧ β)
  • (ca2) (◦α ∧ ◦β) → ◦(α ∨ β)
  • (ca3) (◦α ∧ ◦β) → ◦(α → β)

Inference rule (MP:)

         α, α → β
         _________
         β 

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) α → (¬α → β)


“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 Ø ∈ {∧, ∨, →};


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.
http://www.cfh.ufsc.br/~dkrause/LogicaI/ParaconsistenteSA.htm
ftp://logica.cle.unicamp.br/pub/e-prints/vol.5,n.1,2005-revised.pdf

Ferramentas pessoais