Uma família de lógicas não-clássicas
Os Sistemas KG são quatro lógicas proposicionais construídas sobre uma mesma linguagem para estudar conjuntamente a negação clássica, a paraconsistente e a paracompleta. KGm, KGp, KGq e KGc compartilham uma base formal e se distinguem pela maneira como tratam as duplas negações, permitindo investigar tanto cada negação quanto suas combinações.
A linguagem proposicional de KG permite combinar, de modo independente, três maneiras de negar.
Se α e β são fórmulas, então ¬cα, ¬pα, ¬qα e (α → β) também são fórmulas.
α, α → β / βC1α → (β → α)
C2(α → β) → ((α → (β → γ)) → (α → γ))
N1(α → β) → ((α → ¬cβ) → ¬cα)
N2¬qα → ¬cα
N3¬cα → ¬pα
N4¬c¬cα → α
N5¬p¬pα → α
N6α → ¬q¬qα
KGm usa MP, C1–C2 e N1–N4. KGp acrescenta N5; KGq, N6; KGc, N5 e N6.
α ∧ β := ¬c(α → ¬cβ)α ∨ β := ¬cα → βα ↔ β := (α → β) ∧ (β → α)A base comum. Não assume nem ¬p¬pα → α nem α → ¬q¬qα.
Acrescenta N5: a dupla negação paraconsistente pode ser eliminada.
Acrescenta N6: a dupla negação paracompleta pode ser introduzida.
Reúne N5 e N6 e, portanto, as duas extensões da base minimal.
Na semântica bivalorada, 1 é o valor designado e 0 o não-designado. Para todo sistema KG:
v(¬cα) = 1 ⇔ v(α) = 0v(¬pα) = 0 ⇒ v(α) = 1v(¬qα) = 1 ⇒ v(α) = 0v(α → β) = 1 ⇔ v(α) = 0 ou v(β) = 1v(α ∧ β) = 1 ⇔ v(α) = v(β) = 1v(α ∨ β) = 1 ⇔ v(α) = 1 ou v(β) = 1v(α ↔ β) = 1 ⇔ v(α) = v(β)KGp e KGcv(¬p¬pα) = 1 ⇒ v(α) = 1
KGq e KGcv(α) = 1 ⇒ v(¬q¬qα) = 1
A seguir, você pode construir Árvores Semânticas (Tableaux Analíticos) para testar fórmulas nos quatro Sistemas KG. Depois do laboratório, o Tetraedro das Oposições sintetiza geometricamente as relações algébricas entre as três negações e suas principais interações.
Método de prova
Um tableau é uma árvore semântica que decompõe uma fórmula em condições cada vez mais simples. Para testar se α é teorema de um Sistema KG, começamos supondo que ela é falsa — escrevemos α 0 — e aplicamos as regras adequadas aos conectivos e às negações.
Se cada ramo conduz a uma fórmula com os dois valores, como β 1 e β 0, encontramos uma contradição semântica e fechamos o ramo com ⊗. Quando todos os ramos fecham, não existe valoração que torne α falsa; portanto, α é demonstrada no sistema escolhido. Um ramo completo que permanece aberto indica uma possível contra-valoração.
Nos Sistemas KG, as regras preservam a semântica comum e acrescentam duas expansões específicas: uma para KGp/KGc e outra para KGq/KGc. Passe o cursor pelos cartões para consultar cada regra.
¬cα 1 ⟹ α 0¬cα 0 ⟹ α 1A negação clássica sempre inverte o valor da fórmula.
¬pα 0 ⟹ α 1Se a negação paraconsistente é falsa, a fórmula é verdadeira. Não há expansão geral para ¬pα com valor 1.
¬qα 1 ⟹ α 0Se a negação paracompleta é verdadeira, a fórmula é falsa. Não há expansão geral para ¬qα com valor 0.
(α → β) 0 ⟹ α 1, β 0(α → β) 1α 0 │ β 1A condicional falsa gera duas consequências no mesmo ramo; a verdadeira divide o tableau.
(α ∧ β) 1 ⟹ α 1, β 1(α ∧ β) 0α 0 │ β 0Uma conjunção verdadeira preserva ambos os conjuntivos; uma conjunção falsa ramifica.
(α ∨ β) 0 ⟹ α 0, β 0(α ∨ β) 1α 1 │ β 1Uma disjunção falsa preserva ambos os disjuntos falsos; uma disjunção verdadeira ramifica.
(α ↔ β) 1 ⟹ (α 1, β 1) │ (α 0, β 0)(α ↔ β) 0 ⟹ (α 1, β 0) │ (α 0, β 1)O bicondicional verdadeiro conserva valores iguais; o falso separa valores distintos em ramos alternativos.
¬p¬pα 1 ⟹ α 1É a regra de tableau correspondente ao axioma N5, exclusivo das extensões KGp e KGc.
¬q¬qα 0 ⟹ α 0É a regra de tableau correspondente ao axioma N6, exclusivo das extensões KGq e KGc.
α 1α 0──────── ⊗Quando uma fórmula e sua conjugada aparecem no mesmo ramo, nenhuma valoração satisfaz aquele ramo. O tableau fecha quando todos os ramos fecham.
Laboratório formal
Digite uma fórmula, escolha o sistema e acompanhe cada regra expandir a árvore semântica.
Também são aceitos ->, &, | e letras latinas.
Construção visual
Aplicando regras · passo 1 de 5
Exemplos orientados
Selecione uma fórmula para carregá-la no laboratório e acompanhar a construção do tableau. Os contrastes abertos mostram resultados que não são teoremas de KGm.
Regras implementadas
As consequências seguem no mesmo ramo. KGp acrescenta NP para ¬p¬pα com sinal 1; KGq acrescenta NQ para ¬q¬qα com sinal 0.
Condicional verdadeira, conjunção falsa, disjunção verdadeira e os dois valores do bicondicional dividem a árvore em alternativas.
Um ramo é destacado e fechado quando contém a mesma fórmula com os dois valores de verdade.
Da tradição aristotélica aos Sistemas KG
O ponto de partida é o quadrado aristotélicoQuadrado aristotélicoA · E · I · OATodo S é PENenhum S é PIAlgum S é POAlgum S não é P, uma representação das proposições universais e particulares. Nele, as oposições distinguem contradição, contrariedade, subcontrariedade e subalternação — relações que descrevem quais valores de verdade duas proposições podem ou não compartilhar.
Quando α é comparada às negações clássica, paraconsistente e paracompleta, o quadrado ganha uma dimensão. Surge o tetraedro simplesTetraedro simplesα e suas três negações¬c · clássica¬p · paraconsistente¬q · paracompleta: α e ¬cα são contraditórias; α e ¬qα, contrárias; α e ¬pα, subcontrárias; e as três negações também se articulam por subalternações.
Os Sistemas KG permitem então reiterar negações diferentes numa mesma fórmula. Ao acrescentar todas as combinações de duplas negações, o tetraedro completo amplia a figura inicial para revelar uma rede de contradições, contrariedades, subcontrariedades e subalternações — todas analisáveis pelo método de tableaux.
Arraste para girar · use Zoom + e Zoom − · selecione uma fórmula ou relação