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 >> <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXvpJgzVJ7JEXjXvbtYnzqOrkSD30KHbzgwBH%2BOOs_6sOw%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- > 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 > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CACRvmVQhtWnD6EW%2BbnyYqArdKpMVpsrnTgispR0%2BjyvO%2BHpGFA%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/CAGJaJ%2B-ekWSPbQ8UHZZhcTq4frt5%3DFTUkfhKtNnZt2-UopjN5A%40mail.gmail.com.
