Caros:
David Fuenmayor e eu publicamos recentemente um artigo sobre
limitações dos Teoremas de Gödel no que se refere a certas lógicas
não-clássicas, ao mesmo tempo ilustrando o interesse em se utilizar
assistentes de prova na pesquisa em lógica:
-----------------------------------------------
Gödel’s Incompleteness Theorems from a
Paraconsistent Perspective
Walter Carnielli e David Fuenmayor
https://www.researchgate.net/publication/343838215_Godel%27s_Incompleteness_Theorems_from_a_Paraconsistent_Perspective
---------------------------------------------------------------------------
O artigo investiga as limitações dos argumentos de Gödel com a ajuda
da assistente de provas Isabelle. Mostramos que, ao adotar uma
negação mais leve e flexível (como a negação paraconsistente da lógica
RmbC), evitamos genuinamente a objeção de Gödel, que é erroneamente
considerada universal (embora o próprio Gödel nunca a tenha visto
assim).
Mostramos que uma condição para validar uma versão paraconsistente do
primeiro teorema da incompletude de Gödel é assumir que tanto G_F (a
sentença que declara sua própria indemonstrabilidade) quanto \square
G_F (a provabilidade de G_F) devem ser consistentes no sentido das
LFIs (Lógicas da Inconsistência Formal). De forma semelhante, a versão
paraconsistente do segundo teorema da incompletude de Gödel requer
mais premissas para serem válidas.
A conclusão é que os Teoremas de Gödel so valem para lógicas
paraconsistentes, em geral, ao custo de assumir novas premissas,
muito mais fortes. e que a noção de inconsistência das LFIs é
altamente relevante se queremos manter a validade os Teoremas de
Gödel.
Críticas e discordâncias são bem-vindas!
Walter