Agora entendo melhor. Aritmetização não é necessária, basta a noção formal e mais abstrata de representabilidade. Para citar uma referência muito antiga que já deixa isso bem claro, muito anterior ao meu livro e ao dos Sernadas, cito o clássico Tarski, Mostowski, Robinson, Undecidable Theories. (TMR)
TMR apresenta a seguinte versão do teorema de Godel (citando de memória, pode haver alguma variação inessencial) -Se T tem nomes para suas fórmulas (item 1 da codificação na minha mensagem anterior) e é consistente, então T não representa simultaneamente a operação de diagonalização nas suas fórmulas e a dedutibilidade em T. Essa versão é fácil de demonstrar, como tentei explicar na mensagem anterior. Não é preciso passar por funções recursivas para isso. Nada de aritmética. Essa seria uma versão abstrata, livre de aritmética e de aritmetização, do que chamamos hoje de teorema de Tarski da indefinibilidade da verdade, apesar de Tarski atribuir a Godel em seu livro. No meu livro coloquei essencialmente a mesma coisa, como expliquei no prefácio. Fiz algo similar para o segundo teorema também. Abraço > Em 28 de dez de 2019, à(s) 12:52, Joao Marcos <botoc...@gmail.com> escreveu: > > Petrucio, Carlos, Valeria: agradeço as mensagens! > > Rodrigo, a sua resposta ajuda a corroborar a minha afirmação que a > demonstração do teorema de incompletabilidade gödeliano NÃO depende da > "aritmetização da sintaxe" (como defendeu a autora do artigo citado no > começo da presente discussão). Por certo, a necessária "representação > formal da Matemática" pode ser feita de variadas formas alternativas. > (Os detalhes da demonstração original gödeliana são de interesse > apenas para hackers!) Neste sentido, como ainda não tive tempo de > trabalhar com o seu livro, Rodrigo, posso dizer que aprecio > particularmente o interessante livro de Amílcar e Cristina Sernadas, > "Foundations of Logic and Theory of Computation", onde a noção de > computabilidade é definida sobre strings de alfabetos arbitrários; > contudo, a noção formal de _representabilidade_, ali, também recorre > diretamente a teorias da Aritmética --- como de costume. > > Abraços, > Joao Marcos > > >> On Thu, Dec 26, 2019 at 10:23 AM Rodrigo Freire <freires...@gmail.com> wrote: >> >> [Também não sei se entendi muito bem qual é a direção da questão, e o que eu >> vou escrever aqui pode não ter a ver com o problema intencionado.] >> >> >> Vou tentar explicar o que entendo pela codificação presente no teorema e >> como essa codificação está diretamente ligada à ideia fundacional de >> representar a matemática formalmente. É assim que está no meu livro, Tópicos >> em lógica de primeira ordem, que pode ser baixado livremente. >> >> Suponha que há uma teoria formal de primeira ordem T que “representa” a >> matemática. Como a metamatematica de T é parte da matemática, T é capaz de >> “representar” essa parte também. Isso deve implicar o que entendo por >> codificação: >> >> 1) há uma correspondência unívoca entre fórmulas de T e termos fechados de T >> (Para poder falar de suas fórmulas e “representar” sua metamatemática, T >> deve ter nomes não ambíguos para as fórmulas. Por exemplo, T deve ser capaz >> de dizer de uma fórmula que ela é bem formada. Para isso é preciso nomear a >> fórmula sem ambiguidade. Usamos ‘F’ como nome de F). >> >> 2) tudo o que é decidido na metamatemática, é decidido por um método de >> cálculo matemático, portanto deve ser decidido em T: Tudo que é calculável >> deve ser calculável em T, pois T representa toda a matemática. (T deve >> representar predicados e funções recursivas, pois qualquer método matemático >> de cálculo é representável em T). >> >> 1) + 2) é a codificação. Vamos ver o quanto disso é necessário para a >> demonstração que se T é consistente, a sua teoremicidade não é calculável em >> T. >> >> **Da codificação segue que a operação de diagonalização nas fórmulas (a >> operação que associa a fórmula F(‘F’) a qualquer fórmula F) é calculável em >> T. ** >> >> Se a propriedade metamatemática de ser teorema de T fosse calculável, então >> seria calculável em T. Isso significa que T seria capaz de deduzir B(‘F’), >> quando F é teorema, e ~B(‘F’), quando F não é teorema, para alguma fórmula >> B(x) de T que dizemos representar a teoremicidade. >> >> Mas como a diagonalização é calculável em T, é possível construir uma >> sentença G tal que G é equivalente à ~B(‘G’) em T. Portanto, se T não deduz >> G, então, pela hipótese que a propriedade de ser teorema é calculável, a não >> dedução de G é calculável em T, ou seja, T deduz ~B(‘G’). Mas ~B(‘G’) é >> equivalente a G em T, e concluímos que T deduz G. Novamente pela hipótese, a >> teoremicidade de G é calculável em T, portanto T deduz B(‘G’), que é >> equivalente a ~G. Portanto, T é inconsistente. >> >> Para essa demonstração basta supor 1) acima e apenas que a operação de >> diagonalização é calculável em T. Essa parte da codificação 1) + 2) que é >> requerida. Daí concluímos que se a teoremicidade for calculável em T, então >> T é inconsistente. É isso que fiz em meu livro, uma versão abstrata que não >> menciona funções recursivas. Todos os detalhes podem ser encontrados lá. >> >> Como já foi dito, há outras demonstrações, mas acho que essa é a que está >> mais diretamente ligada à ideia fundacional: se é possível uma representação >> formal da matemática em um sistema formal T, então a teoremicidade de T não >> é calculável (na metamatemática de T ou na própria T), a menos que T seja >> inconsistente. >> >> >> >> >> Em 25 de dez de 2019, à(s) 14:15, Carlos Gonzalez <gonza...@gmail.com> >> escreveu: >> >> >> Eu não estou entendendo muito bem qual é o eixo desta discussão. >> >> Suponha que trabalhamos em AP. >> >> Se demonstrar que o conjunto das fórmulas que não são teoremas não é >> recursivamente enumerável, então o conjunto dos teoremas não é recursivo, E >> isso pode ser provado de maneira finitária. Certo? >> >> Também pode usar técnicas de teoria de modelos para construir modelos >> standard e outras, como ultraprodutos, para modelos não standard. Técnicas >> matemáticas não finitárias. >> >> Um recurso divertido é acrescentar a AP uma constante nova "c" e um conjunto >> infinito de axiomas: >> (s é a função sucessor) >> não ( c = 0) >> não ( c = s0) >> não ( c = ss0) >> não ( c = sss0) >> . >> . >> não ( c = s...s0) >> . >> . >> Por compacidade essa teoria tem modelo. Claro, não standard. >> >> Tudo isso é muito conhecido. >> >> Carlos >> >> >> >> >> >> >> >> >> >> >>> On Wed, Dec 25, 2019 at 1:47 PM Jorge Petrucio Viana >>> <petrucio_vi...@id.uff.br> wrote: >>> >>> Olá para todos, >>> não li esse artigo em detalhes, mas numa passada de olhos, não vi nem >>> aritmetização, nem o predicado Bew, nem autoreferência na prova da >>> incompletude. >>> >>> https://projecteuclid.org/euclid.ndjfl/1027953483 >>> >>> abraços >>> P >>> >>> Em dom., 22 de dez. de 2019 às 22:36, Valeria de Paiva >>> <valeria.depa...@gmail.com> escreveu: >>>> >>>> bom, eu achei que tinha uma escrita pois a Milly Maietti me disse que >>>> tinha, mas procurando no math overflow vi isso: >>>> https://mathoverflow.net/questions/132797/is-there-a-categorical-proof-of-g%C3%B6dels-incompleteness-theorem >>>> depois procuro nos meus preprints, mas estou viajando >>>> Boas Festas a todos, >>>> abs >>>> Valeria >>>> >>>> On Sun, Dec 22, 2019 at 5:31 PM Joao Marcos <botoc...@gmail.com> wrote: >>>>> >>>>> Nunca vi, Valeria... >>>>> >>>>> Você teria uma referência para a demonstração do Joyal? >>>>> >>>>> Abraços, JM >>>>> >>>>> >>>>> On Sun, Dec 22, 2019, 22:28 Valeria de Paiva <valeria.depa...@gmail.com> >>>>> wrote: >>>>>> >>>>>> JM, >>>>>> Eu achei q vc queria ter uma medida de quao dependente de codificao uma >>>>>> prova e’. Eu acho q o Joyal tem uma prova de incompletude usando >>>>>> categories, q nao depende muito de codificacao. >>>>>> mas eu nunca vi ninguem tentando medir quao dependente de codificacao >>>>>> uma prova 'e. voce ja' viu algum assim? >>>>>> abracos, >>>>>> Valeria >>>>>> >>>>>> On Thu, Dec 19, 2019 at 4:52 AM Famadoria <famado...@gmail.com> wrote: >>>>>>> >>>>>>> Vê o teorema de Kleene, de novo. >>>>>>> >>>>>>> Sent from my iPhone >>>>>>> >>>>>>> On 19 Dec 2019, at 08:36, Joao Marcos <botoc...@gmail.com> wrote: >>>>>>> >>>>>>>>> Me parece que o teorema da incompletude de Kleene prescinde de uma >>>>>>>>> codificação. >>>>>>>> >>>>>>>> Bem lembrado, Doria. O teorema de incompletabilidade de Gödel >>>>>>>> realmente segue como corolário do resultado de Forma Normal de Kleene, >>>>>>>> que não apenas prescinde de auto-referência mas que pode ser >>>>>>>> demonstrado sem codificação. Com a minha pergunta, contudo, eu >>>>>>>> pretendia inquirir a respeito da _necessidade_ de usar *aritmetização* >>>>>>>> (ou recursos aritméticos, em geral) em demonstrações de >>>>>>>> incompletabilidade (em particular, à la Gödel). Intuitivamente, a >>>>>>>> resposta me parece ser negativa, isto é, não me parece que tais >>>>>>>> _demonstrações_ "dependam da aritmetização da sintaxe", como afirma a >>>>>>>> autora do artigo. Mas é fato também que, por um motivo ou por outro, >>>>>>>> não tenho visto demonstrações do teorema gödeliano que evitem a >>>>>>>> burocracia da aritmetização... >>>>>>>> >>>>>>>> Abraços, >>>>>>>> Joao Marcos >>>>>>>> >>>>>>>> >>>>>>>>>> On 18 Dec 2019, at 13:03, Joao Marcos <botoc...@gmail.com> wrote: >>>>>>>>>> >>>>>>>>>> Os comentários sobre o *racionalismo otimista* ("platonismo >>>>>>>>>> ingênuo"?) >>>>>>>>>> de Gödel, no artigo, são filosoficamente interessantes. >>>>>>>>>> >>>>>>>>>> Das três observações que faço abaixo, as duas primeiras são críticas >>>>>>>>>> e >>>>>>>>>> a terceira é um questionamento para os colegas. >>>>>>>>>> >>>>>>>>>> ### >>>>>>>>>> >>>>>>>>>> (0) >>>>>>>>>> >>>>>>>>>> Entre outras coisas, como observação parentética, parece-me um pouco >>>>>>>>>> _out of the ordinary_ que se escreva algo assim: >>>>>>>>>> >>>>>>>>>> "The axioms of PA include the commutative law of addition, for >>>>>>>>>> example, which states that it doesn’t matter in which order two >>>>>>>>>> numbers are added to each other, the result is the same. They also >>>>>>>>>> include the single rule of proof called Modus Ponens: “if A implies >>>>>>>>>> B, >>>>>>>>>> and A, then B”. >>>>>>>>>> >>>>>>>>>> Suponho, contudo, que tais frases se tratem de uma espécie de >>>>>>>>>> simplificação, _for the sake of the exposition_... >>>>>>>>>> >>>>>>>>>> ### >>>>>>>>>> >>>>>>>>>> (1) >>>>>>>>>> >>>>>>>>>> Formular o teorema de incompletabilidade de Gödel da seguinte maneira >>>>>>>>>> também me parece razoavelmente _misleading_: >>>>>>>>>> >>>>>>>>>> "Given any axiom system which is both consistent and sufficiently >>>>>>>>>> strong computationally, in the sense of being able to encode finite >>>>>>>>>> sequences (see below), there is a statement in the language of the >>>>>>>>>> system that is true, but cannot be proved from the axioms." >>>>>>>>>> >>>>>>>>>> Em particular, o sistema axiomático (não-recursivamente enumerável) >>>>>>>>>> que contêm como axiomas todas as sentenças verdadeiras da Aritmética >>>>>>>>>> é >>>>>>>>>> obviamente completo... >>>>>>>>>> >>>>>>>>>> ### >>>>>>>>>> >>>>>>>>>> (2) >>>>>>>>>> >>>>>>>>>> A pergunta que deixo aqui para os colegas é: qual é, na opinião de >>>>>>>>>> vocês, o grau de verdade da asserção >>>>>>>>>> >>>>>>>>>> "The proofs for both theorems depend on the concept of an encoding, >>>>>>>>>> or >>>>>>>>>> in technical terms the arithmetization of syntax"? >>>>>>>>>> >>>>>>>>>> Em outras palavras, qual o real grau de "dependência" do "conceito de >>>>>>>>>> codificação" para as demonstrações de incompletude? >>>>>>>>>> >>>>>>>>>> ### >>>>>>>>>> >>>>>>>>>> Joao Marcos >>>>>>>>>> >>>>>>>>>>> On Wed, Dec 18, 2019 at 10:31 AM Joao Marcos <botoc...@gmail.com> >>>>>>>>>>> wrote: >>>>>>>>>>> >>>>>>>>>>> Kurt Gödel and the mechanization of mathematics >>>>>>>>>>> - Juliette Kennedy discusses Kurt Gödel’s Incompleteness Theorems: >>>>>>>>>>> the >>>>>>>>>>> ingenious proofs and enduring impact >>>>>>>>>>> https://www.the-tls.co.uk/articles/kurt-godel-incompleteness-theorems/ >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> JM >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> -- >>>>>>>>>> http://sequiturquodlibet.googlepages.com/ >>>>>>>>>> >>>>>>>>>> -- >>>>>>>>>> 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/CAO6j_Lg6zFhN50kmLG_Q1QsZgXpKYA7yreFSnwQZnDZN1M-_ww%40mail.gmail.com. >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> -- >>>>>>>> http://sequiturquodlibet.googlepages.com/ >>>>>>> >>>>>>> -- >>>>>>> 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/63B5BA64-530F-4B5F-8D55-2EB8C1CEC58D%40gmail.com. >>>> >>>> >>>> >>>> -- >>>> Valeria de Paiva >>>> http://vcvpaiva.github.io/ >>>> http://www.cs.bham.ac.uk/~vdp/ >>>> >>>> -- >>>> 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/CAESt%3DXvpJgzVJ7JEXjXvbtYnzqOrkSD30KHbzgwBH%2BOOs_6sOw%40mail.gmail.com. >>> >>> -- >>> 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/CACRvmVQhtWnD6EW%2BbnyYqArdKpMVpsrnTgispR0%2BjyvO%2BHpGFA%40mail.gmail.com. >> >> -- >> 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/CAGJaJ%2B-ekWSPbQ8UHZZhcTq4frt5%3DFTUkfhKtNnZt2-UopjN5A%40mail.gmail.com. >> >> -- >> 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/BFF24528-233C-4A5C-81C2-EA7B2217B219%40gmail.com. > > > > -- > http://sequiturquodlibet.googlepages.com/ -- 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/AD82487C-C08D-4284-A6B1-5563B48DD1A3%40gmail.com.
