A lógica C1
| Linha 9: | Linha 9: | ||
</ul> | </ul> | ||
| − | + | C1 Axiomas: | |
| − | + | ||
<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 11h24min 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
