Sistemas KG: uma introdução rápida

Esta nota é diferente das anteriores desta série. Até aqui eu expus posições de outros autores (Slater, Béziau, Arenhart) ou critiquei uma estratégia alheia (a de da Costa (1989)da Costa, N.C.A.. Logics that are both paraconsistent and paracomplete. Atti della Accademia Nazionale dei Lincei. Classe di Scienze Fisiche, Matematiche e Naturali. Rendiconti. v. 83. n. 1. p. 29–32. Accademia Nazionale dei Lincei. 1989.). A partir daqui, apresento algo meu: os Sistemas KG, desenvolvidos na minha tese de doutorado e publicados em Três vezes não (Gracher, 2022Gracher, Kherian. Três vezes não: um estudo sobre as negações clássica, paraconsistente e paracompleta. Londres. College Publications. 2022.). Vou pedir ao leitor um pouco mais de paciência do que nas notas anteriores — não porque o assunto seja mais difícil, mas porque quero fazer essa apresentação com o cuidado que ela merece, sem atalhos.

A ideia central

Recapitulando a nota anterior: o problema de $N_1$ não é hospedar as três negações — ele hospeda muito bem. O problema é que, em $N_1$, uma negação só é clássica, paraconsistente ou paracompleta por causa do comportamento (bem ou mal comportado) da fórmula à qual ela está aplicada. A negação em si — o símbolo $\neg$ — é uma coisa só, a "negação não-alética"; o que muda é a fórmula que ela nega. E foi exatamente essa estratégia — marcar a proposição, e deixar que o conectivo "herde" seu comportamento dela — que já critiquei numa nota anterior desta série.

A ideia central dos Sistemas KG é simples de enunciar, ainda que trabalhosa de desenvolver: em vez de um conectivo de negação cujo comportamento depende de marcações sobre a proposição, tomamos três conectivos de negação primitivos — $\neg_c$ (clássica), $\neg_q$ (paracompleta) e $\neg_p$ (paraconsistente) — que podem ser aplicados a qualquer fórmula, sem que essa fórmula precise estar previamente marcada como bem ou mal comportada de forma alguma. O bom comportamento, quando fizer sentido falar dele, será definido a partir das negações — não o contrário. Essa inversão de ordem é o que torna possível, como veremos, que as três negações interajam livremente dentro de uma mesma fórmula: nada, na sintaxe, impede de escrever $\neg_p\neg_c\alpha$ ou $\neg_c\neg_q\neg_p\alpha$, porque cada negação é, desde o início, seu próprio conectivo.

A linguagem

A linguagem $L$ dos Sistemas KG tem um alfabeto simples: variáveis proposicionais ($p, q, r, s, p_1, p_2, ...$); os três conectivos de negação primitivos ($\neg_c$, $\neg_q$, $\neg_p$); o condicional ($\rightarrow$); e os símbolos auxiliares de sempre (parênteses, vírgulas). As fórmulas são definidas como seria de se esperar: toda variável proposicional é uma fórmula; se $\alpha$ é fórmula, $\neg_c\alpha$, $\neg_q\alpha$ e $\neg_p\alpha$ também são; se $\alpha$ e $\beta$ são fórmulas, $(\alpha \rightarrow \beta)$ é fórmula; e nada mais é fórmula (Gracher, 2022Gracher, Kherian. Três vezes não: um estudo sobre as negações clássica, paraconsistente e paracompleta. Londres. College Publications. 2022.; p. 59-60).

Conjunção, disjunção e bicondicional não são primitivos — são definidos a partir do condicional e da negação clássica, do mesmo modo consagrado desde a lógica clássica:

Os postulados

Além do Modus Ponens, os Sistemas KG partem de nove esquemas de axiomas (Gracher, 2022Gracher, Kherian. Três vezes não: um estudo sobre as negações clássica, paraconsistente e paracompleta. Londres. College Publications. 2022.; p. 60-61). Os dois primeiros são os axiomas usuais da lógica positiva:

O terceiro fixa o comportamento da negação clássica como redução ao absurdo:

Os próximos dois axiomas merecem atenção especial, porque são exatamente as duas subalternações do Tetraedro Simples das Oposições que construímos nas primeiras notas desta série — só que agora não são apenas relações semânticas verificadas caso a caso: são axiomas.

Ou seja: a negação paracompleta subalterna a negação clássica, e a negação clássica subalterna a negação paraconsistente, por construção — desde o primeiro axioma que escrevemos. Não precisamos demonstrar essas relações a partir de condições de verdade indiretas, como fizemos com $N_1$; elas estão na própria base do sistema.

Os últimos três axiomas do núcleo comum tratam da dupla negação clássica e de metades das duplas negações paraconsistente e paracompleta:

(N4) diz que a dupla negação clássica se elimina, como seria de se esperar. Mas repare que (N5) e (N6) não fecham as duplas negações paraconsistente e paracompleta por completo — cada um garante apenas uma direção. É aqui que entra a família de sistemas.

Quatro sistemas, uma família

Nem todos os axiomas acima pertencem a todo Sistema KG. KGm (o sistema minimal) contém apenas (MP) e os axiomas (C1)-(N4) — sem (N5) nem (N6). Isso significa que, em KGm, nem a eliminação da dupla negação paraconsistente ($\neg_p\neg_p\alpha \rightarrow \alpha$) nem a introdução da dupla negação paracompleta ($\alpha \rightarrow \neg_q\neg_q\alpha$) são teoremas — as negações paraconsistente e paracompleta de KGm são, portanto, estritamente mais fracas que as de $C_1$ e $P_1$, respectivamente.

• KGp acrescenta (N5) a KGm: a dupla negação paraconsistente se elimina, e a negação paraconsistente passa a ter as propriedades da negação de $C_1$. A paracompleta continua fraca.
• KGq acrescenta (N6) a KGm: a dupla negação paracompleta se introduz, e a negação paracompleta passa a ter as propriedades da negação de $P_1$. A paraconsistente continua fraca.
• KGc acrescenta ambos, (N5) e (N6): as três negações têm, cada uma, todas as propriedades esperadas — respectivamente, de $C_1$, $P_1$ e da lógica clássica (Gracher, 2022Gracher, Kherian. Três vezes não: um estudo sobre as negações clássica, paraconsistente e paracompleta. Londres. College Publications. 2022.; p. 62-64).

Como KGm é o núcleo comum aos outros três, todo teorema de KGm é automaticamente teorema de KGp, KGq e KGc.

Bom comportamento, agora definido — não pressuposto

Aqui está a inversão que prometi lá no início. Em vez de marcar previamente uma proposição como bem comportada para então decidir o comportamento de sua negação — a estratégia de da Costa —, definimos o bom comportamento a partir das três negações primitivas, depois que elas já existem:

O operador-$p$ (bom comportamento paraconsistente) diz que a negação paraconsistente de $\alpha$ implica sua negação clássica; combinado com o axioma (N3), que já garante a implicação inversa, uma fórmula operada por $p$ tem suas negações clássica e paraconsistente equivalentes. O operador-$q$ funciona de modo simétrico com a negação paracompleta, combinado ao axioma (N2). O operador-$c$, por fim, equivale à conjunção dos outros dois (Gracher, 2022Gracher, Kherian. Três vezes não: um estudo sobre as negações clássica, paraconsistente e paracompleta. Londres. College Publications. 2022.; p. 61-62).

Note a diferença de espírito: para da Costa, o bom comportamento é uma propriedade primitiva da proposição, que determina como sua negação vai se comportar. Aqui, o bom comportamento é uma propriedade derivada, que só faz sentido depois que já temos três negações independentes para comparar entre si. A proposição não muda — o que muda, de novo, é só o conectivo.

Uma semântica com duas negações "abertas"

A semântica dos Sistemas KG é bivalorada, mas com uma particularidade importante. A negação clássica recebe a condição de sempre, uma bicondicional:

As negações paraconsistente e paracompleta, porém, recebem apenas metade dessa condição cada uma:

Isso não é um descuido — é exatamente o ponto. Se essas condições fossem bicondicionais como (b), as negações paraconsistente e paracompleta ficariam totalmente determinadas pelo valor de $\alpha$, e voltaríamos a ter negações que se comportam como a clássica por definição, e não por escolha. Deixando (c) e (d) como implicações de uma via só, o valor de $\upsilon_i(\neg_p\alpha)$ quando $\alpha$ é verdadeira — ou de $\upsilon_i(\neg_q\alpha)$ quando $\alpha$ é falsa — fica livre, a não ser que outras condições (como as dos sistemas KGp e KGq) venham fechá-lo (Gracher, 2022Gracher, Kherian. Três vezes não: um estudo sobre as negações clássica, paraconsistente e paracompleta. Londres. College Publications. 2022.; p. 71-73).

Essa liberdade tem uma consequência visual interessante: em vez de tabelas de verdade comuns, onde cada linha determina um único resultado, as tabelas dos Sistemas KG às vezes bifurcam. Considere a tabela mais simples, que relaciona $\alpha$ apenas às suas três negações, sem operadores de bom comportamento:

Quando $\alpha$ é verdadeira, sabemos que $\neg_c\alpha$ é falsa e $\neg_q\alpha$ é falsa — mas $\neg_p\alpha$ pode ser verdadeira ou falsa, porque nada na condição (c) obriga um valor quando $\alpha$ já é verdadeira. Do mesmo modo, quando $\alpha$ é falsa, $\neg_p\alpha$ é verdadeira, mas $\neg_q\alpha$ fica livre (Gracher, 2022Gracher, Kherian. Três vezes não: um estudo sobre as negações clássica, paraconsistente e paracompleta. Londres. College Publications. 2022.; p. 88-89). Chamamos isso de "quase-matriz": uma tabela bivalorada, mas não funcional no sentido usual — o valor de uma fórmula complexa nem sempre é determinado apenas pelos valores de suas subfórmulas.

É essa mesma liberdade que torna possível o resultado que perseguíamos desde a nota anterior: como $\neg_p\alpha$ não está amarrada ao valor de $\alpha$ (a não ser pela metade de condição que vimos), nada impede que uma fórmula complexa combine as três negações livremente, cada uma contribuindo com sua própria condição de verdade, sem que o comportamento de uma force o das outras.

Quase-matrizes exigem tableaux

Como as tabelas de verdade dos Sistemas KG podem bifurcar, elas não são um método de decisão tão direto quanto as tabelas da lógica clássica. Por isso, o método de prova mais prático para os Sistemas KG é o de tableaux analíticos com fórmulas sinalizadas, na tradição de Smullyan (1971)Smullyan, Raymond R. First-order logic. v. 43. Springer. 1971.. A ideia: sinalizamos uma fórmula com $1$ (assumida verdadeira) ou $0$ (assumida falsa); partimos da negação daquilo que queremos provar; aplicamos regras que decompõem fórmulas complexas em mais simples; e, se todo ramo da árvore resultante chegar a uma contradição — a mesma fórmula sinalizada como verdadeira e como falsa —, a fórmula original é uma tautologia do sistema (Gracher, 2022Gracher, Kherian. Três vezes não: um estudo sobre as negações clássica, paraconsistente e paracompleta. Londres. College Publications. 2022.; p. 97).

As regras para KGm são estas:

Note que faltam duas regras: não há regra para $\neg_p\alpha^1$ nem para $\neg_q\alpha^0$. Isso é o espelho exato da assimetria que vimos na semântica — como essas duas condições não são bicondicionais em KGm, não há nada que essas fórmulas sinalizadas nos obriguem a concluir sobre $\alpha$. Quando o sistema inclui os axiomas (N5) ou (N6), duas regras adicionais entram em cena:

Para conjunção e disjunção (definidas a partir do condicional e da negação clássica) valem regras derivadas, que funcionam exatamente como se esperaria da lógica clássica: $\alpha \wedge \beta$ verdadeira produz $\alpha^1$ e $\beta^1$ direto; $\alpha \wedge \beta$ falsa ramifica em $\alpha^0$ ou $\beta^0$; e simetricamente para a disjunção (Gracher, 2022Gracher, Kherian. Três vezes não: um estudo sobre as negações clássica, paraconsistente e paracompleta. Londres. College Publications. 2022.; p. 99-101).

Um exemplo resolvido

Para ver o método em ação, vamos provar que o próprio axioma (N3), $\neg_c\alpha \rightarrow \neg_p\alpha$, é uma tautologia de KGm — como deveria ser, já que é um axioma. Começamos assumindo sua negação:

Os passos 4 e 5 atribuem valores opostos à mesma fórmula $\alpha$ no mesmo ramo — uma contradição semântica. O ramo fecha ($\otimes$), e como é o único ramo do tableau, o tableau inteiro fecha. Isso confirma que $\neg_c\alpha \rightarrow \neg_p\alpha$ é uma tautologia de KGm.

O que fica garantido

Os Sistemas KG preservam os metateoremas que qualquer sistema decente baseado em Modus Ponens e nos axiomas (C1)-(C2) deveria ter: autodedutibilidade, monotonicidade, a regra do corte, o teorema da dedução, o teorema da implicatividade, prova por casos e o teorema da finitude (Gracher, 2022Gracher, Kherian. Três vezes não: um estudo sobre as negações clássica, paraconsistente e paracompleta. Londres. College Publications. 2022.; p. 65-69). Não vou reproduzir essas demonstrações aqui — são resultados bastante padronizados, que qualquer curso de lógica proposicional deduz para sistemas hilbertianos com implicação — mas é importante que o leitor saiba que estão lá, demonstradas com cuidado no livro. Mais relevante para os nossos propósitos: a semântica de valorações que apresentei é correta e completa em relação aos quatro sistemas axiomáticos, e o método de tableaux é correto e completo em relação a essa mesma semântica — de modo que os três níveis (axiomas, valorações, tableaux) sempre concordam sobre o que é ou não teorema.

Onde isso nos deixa

Voltando à pergunta que abriu esta série de notas: agora temos um sistema em que $\neg_c$, $\neg_q$ e $\neg_p$ são conectivos primitivos, livres para se combinar em uma mesma fórmula sem que o comportamento de um force o comportamento dos outros — exceto pelas relações que decidimos impor deliberadamente, como as subalternações (N2) e (N3), que valem como axiomas em qualquer contexto, não apenas quando a fórmula está previamente marcada como bem comportada. É exatamente o que faltava em $N_1$.

O que ainda não expliquei é o que ganhamos de fato com essa liberdade — que resultados novos ela produz, que teoremas surpreendentes aparecem quando as três negações finalmente podem interagir. É esse o assunto da próxima nota.