[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ê 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/BFF24528-233C-4A5C-81C2-EA7B2217B219%40gmail.com.
