Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-28 Por tôpico Rodrigo Freire
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.

Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-28 Por tôpico Joao Marcos
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

Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-26 Por tôpico Rodrigo Freire
[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

Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-25 Por tôpico Valeria de Paiva
Legal esse paper to Putnam, Petrucio! obrigada por mandar. Boas Festas pra todos! Valeria On Wed, Dec 25, 2019 at 5:47 AM 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

Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-25 Por tôpico Carlos Gonzalez
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?

Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-25 Por tôpico Jorge Petrucio Viana
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 <

Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-22 Por tôpico Valeria de Paiva
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

Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-22 Por tôpico Joao Marcos
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 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 >

Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-22 Por tôpico Valeria de Paiva
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?

Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-19 Por tôpico Famadoria
Vê o teorema de Kleene, de novo. Sent from my iPhone On 19 Dec 2019, at 08:36, Joao Marcos 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

Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-19 Por tôpico Joao Marcos
> 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

Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-18 Por tôpico Famadoria
Me parece que o teorema da incompletude de Kleene prescinde de uma codificação. Sent from my iPhone > On 18 Dec 2019, at 13:03, Joao Marcos wrote: > > Os comentários sobre o *racionalismo otimista* ("platonismo ingênuo"?) > de Gödel, no artigo, são filosoficamente interessantes. > > Das três

[Logica-l] Re: Kurt Gödel and the mechanization of mathematics

2019-12-18 Por tôpico Joao Marcos
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