É preciso ler para comentar. Eu o li. O artigo está muito bem escrito, é claro e informativo. Aliás, tem muito conteúdo.
Porém, se me permite uma observação, o tema dele não é exatamente saber qual é o escopo dos teoremas de Gödel. As suas questões fulcrais, que ficam claras ao longo do texto, são: 1. É possível demonstrar os teoremas de Gödel numa lógica paraconsistente? 2. Se tal é possível, como se fazem as demonstrações? A premissa de que o escopo dos teoremas em comento não abrange todos os sistemas formais é apenas a justificativa para formular a primeira pergunta. A questão de saber quantas são as aritméticas que existem e quais são elas não é estranha ao assunto, obviamente, mas ela já faz parte do que as ideias gerais subjacentes do artigo podem suscitar. Ou seja, requerem outro artigo para ser respondida. Isto dito, eu sugiro quando as pessoas quiserem examinar essa outra questão, de um ponto de vista filosófico, organizarem seus argumentos assim: Seja A★ um sistema formal diferente em seus axiomas da aritmética de Peano: 1. Quais são então as características que A★ deve ter para ser considerado uma aritmética legítima? 2. A★ tem utilidade matemática? Qual? 3. Os resultados obtidos a partir de A★ divergem dos resultados conhecidos da aritmética elementar? 4. É possível construir A★ por meios de uma teoria de conjuntos ou de uma geometria conhecida? Fico por aqui com essas observações gerais. Em ter, 25 de ago de 2020 16:54, Walter Carnielli < walter.carnie...@gmail.com> escreveu: > Olá Marcelo, e demais interessad@s: > > Ótima pergunta, que nos dá ensejo de esclarecer o papel da > aritmética.em nosso artigo Como notamos no Remark 5.2, existem outros > estudos sobre aritmética paraconsistente. Mas não é essa nossa intenção. > > Nossa análise assume o lema de ponto fixo (paraconsistente) > ´ (G_F <-> \neg\box G_F) 'para o bem do argumento' a fim de encontrar > novas premissas (implícitas) necessárias e/ou suficientes para que se possa > reconstruir formalmente o argumento de Gödel usando uma negação > paraconsistente. Isso aparece claor inclusive na Footnote 5, onde nos > referimso a 'the last-mile' of Gödel's proof". > > > A análise pode ser feita em duas vias: > > 1) Poderia ser o caso (não acreditamos nisso) que alguém > demonstrasse que é impossível definir a função Gödelização em uma > aritmética paraconsistente baseada em RmBC. Se fosse assim, já > seria então impossível exprimir as versões conhecidas dos Teoremas > de Godel em tal lógica.. mas poderia haver outro tipo de prova. > > 2) Contudo, isso não parece ser o caso: ao contrário, RmbC ( o > sistema lógico que usamos, mas podem ser usados outros) tem uma > versão em primeira ordem, onde se podem definir os Axiomas de Peano: > > > W. A. Carnielli, M. E. Coniglio, and D. Fuenmayor. “Logics of > Formal Inconsistency enriched with replacement: an algebraic > nd modal account”. Submitted for publication, preprint available from > https://www.cle.unicamp.br/eprints/index.php/CLE_e-Prints. > > > 3) Como Axiomas de Peano não dependem da negação,e ainda mais RmbC de > primeira ordem consegue definir dentro dela a lógica clássica de > primeira ordem (FOL) fica patente que sim, se pode reproduzir a > função Gödelização em RmbC de primeira ordem . > > > 4) Partimos então dai, e o resto da análise está no artigo. > > > Cremos que isso responde completamente à sua (ótima) questão. > > > Abraços, > > > Walter + David > > > > > > > >> Os Teoremas de Gödel são menos inevitáveis do que parecem... >> <http://groups.google.com/a/dimap.ufrn.br/group/logica-l/t/f4f39c3e8fae4ff5?utm_source=digest&utm_medium=email> >> >> >> Marcelo Finger <mfin...@ime.usp.br>: Aug 24 10:51PM -0300 >> >> Oi Walter. >> >> A aritmética RmbC é computável? Se for, qual a sua expressividade, ou >> seja, qual fragmento da aritmética clássica ela consegue simular? >> >> []s >> >> >> Em seg., 24 de ago. de 2020 às 21:50, Walter Alexandre Carnielli < >> >> -- >> Marcelo Finger >> Departament of Computer Science, IME >> University of Sao Paulo >> http://www.ime.usp.br/~mfinger >> ORCID: https://orcid.org/0000-0002-1391-1175 >> ResearcherID: A-4670-2009 >> <http://lattes.cnpq.br/1055555496835379> >> > -- > Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos > Grupos do Google. > Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie > um e-mail para logica-l+unsubscr...@dimap.ufrn.br. > Para ver essa discussão na Web, acesse > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CA%2Bob58Mhu47w7FE1nfHYL-Ky47%2BuZ2pGhNgzL7ZYSrWRWE9KsQ%40mail.gmail.com > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CA%2Bob58Mhu47w7FE1nfHYL-Ky47%2BuZ2pGhNgzL7ZYSrWRWE9KsQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAEsiyHSRc7g%2Bd0G2Lat%3DuNkmbdosOHVUQwsbgv8vGoAVRtQovw%40mail.gmail.com.
