Ver código-fonte

C1 é históricamente importante porque foi a primeira lógica paraconsistente a ser apresentada por Newton C. A. da Costa em 1963.

<ul>
<li>	O operador de consistência (◦) foi introduzido. </li>
<li>	O significado de ◦A é “A é consistente”.</li>
<li>	O conectivo consistência "◦" não é um conectivo primitivo, 
mas uma abreviação: </li>
<li>	◦A = ¬(A ∧ ¬A) </li>
</ul>

C1 Axiomas:


<ul>
<li>(Ax1) α → (β → α) </li>
<li>(Ax2) (α → β) → ((α → (β → γ)) → (α → γ)) </li>
<li>(Ax3) α → (β → (α ∧ β))</li>
<li>(Ax4) (α∧ β) → α</li>
<li>(Ax5) (α ∧ β) → β</li>
<li>(Ax6) α → (α ∨ β) </li>
<li>(Ax7) β → (α ∨ β) 
<li>(Ax8) (α → γ) → ((β → γ) → ((α ∨ β) → γ)) </li>
<li>(Ax9) α ∨ (α → β) </li>
<li>(Ax10) α ∨ ¬α </li>
<li>(Ax11) ¬¬α → α </li>
</ul>

Axiom  schemas:
<ul>
<li>(bc1) ◦α → (α → (¬α → β)) </li>
<li>(ca1) (◦α ∧ ◦β) → ◦(α ∧ β)</li>
<li>(ca2) (◦α ∧ ◦β) → ◦(α ∨ β)</li>
<li>(ca3) (◦α ∧ ◦β) → ◦(α → β)</li>
</ul>

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:

<ul>
<li>v(α1 ∧ α2 ) = 1 ⇐⇒ v(α1 ) = 1 and v(α2) = 1;</li>
<li>v(α1 ∨ α2 ) = 1 ⇐⇒ v(α1 ) = 1 or v(α2) = 1;</li>
<li>v(α1 → α2 ) = 1 ⇐⇒ v(α1 ) = 0 or v(α2) = 1;</li>
<li>v(¬α) = 0 ⇒ v(α) = 1;</li>
<li>v(¬¬α) = 1 ⇒ v(α) = 1;</li>
<li>v(◦α) = 1 ⇒ v(α) = 0 or v (¬α) = 0;</li>
<li>v(◦(α Ø  β)) = 0 ⇒ v(◦α) = 0 or v(◦β) = 0, para Ø ∈ {∧, ∨, →};</li>
</ul>


'''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 />
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 />