A lógica C1

Edição de 12h46min 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) (◦α ∧ ◦β) → ◦(α → β)

Regra de inferência (MP:)

Para obter a lógica proposicional clássica (CPL) de C1, removem-se os ◦-aximas: (bc1), (ca1), (ca2) e (ca3) e adiciona-se a lei da explosão:

   (exp) α → (¬α → β)

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:

1. CARNIELLI, Walter; CONIGLIO, Marcelo E.; MARCOS, João. Logics of Formal Inconsistency. 2. ed. São Paulo: Springer-Verlag, 2007 p. 15-107.

1. KRAUSE, Décio. A Lógica Paraconsistente. Disponível em: <http://www.cfh.ufsc.br/~dkrause/LogicaI/ParaconsistenteSA.htm>. Acesso em 09 set. 2009.

1. 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.

1. http://www.cle.unicamp.br/e-prints/vol_5,n_1,2005.html