Hermógenes e lista, Eu , (pura teimosia?) continuo insistindo que a raiz do problema está na definição recursiva que usam as linguagens formais, que passam a ser, como Kleene disse, aritméticas.
Foi Thoralf Skolem, um defensor da teoria de números, que "aritmetizou" a lógica e a matemática quando deu a definição recursiva de fórmula, etc. Um artigo interessante e profundo teria como nome: "Thoralf Skolem and the mechanization of mathematics" Para ser bem claro: Para mim não tem sentido algum, nem interesse qualquer, falar da influência de Gödel na mecanização da matemática quando "fórmula", "dedução", etc., tem uma definição recursiva. Quero dizer coisas como: a concatenação e uma adição e a substituição é uma multiplicação. Por isso é que funciona a aritmetização de Gödel. A propósito: Alguém conhece uma bibliografia sobre o uso geral desse conceito de "mecanização"? "Que comportamento mecânico que tem esse homem", etc. Carlos On Sat, Dec 28, 2019 at 8:10 PM Hermógenes Oliveira <olive...@daad-alumni.de> wrote: > Olá, pessoal. > > João Marcos escreveu: > > 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). > > Permitam-me assumir o ultrajante papel de advogado do diabo. :-) > > Rodrigo Freire escreveu (ênfase minha): > > > 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. > > Ora, é fácil se livrar da aritmetização se simplesmente a assumirmos > como hipótese! > > O resultado de Kleene também foi aludido nesta discussão como > evidência em favor da tese de João Marcos. Esse resultado, de fato, > implica uma *versão* do resultado de Gödel que trata de teorias > recursivamente axiomatizáveis nas quais *as funções recursivas > primitivas são representáveis*[1]. Ora, para se chegar ao enunciado > original de Gödel, é necessário ainda estabelecer que as funções > recursivas primitivas são representáveis nas teorias fundacionais tipo > Principia Mathematica. É precisamente isso que é alcançado por meio > da aritmetização. Ainda que seja repertório básico para os lógicos de > carreira contemporâneos, isso não é evidente. Inclusive, pode-se > dizer que Gödel inaugurou com seu artigo os estudos do que hoje > chamamos de funções recursivas primitivas. > > Se estamos pensando em demonstrações do enunciado original de Gödel, > com todo seu impacto e consequências, então não creio que seja > possível evitar a tal aritmetização (bem como diagonalização). > Supostas demonstrações livres dela estão fadadas a pressupô-la de > alguma maneira, seja explicitamente, ou embutida em definições. > > Certamente, como já foi observado nesta discussão, há uma certa > vagueza em "demonstrações do resultado de incompletabilidade de > Gödel". Não está perfeitamente claro quando um resultado deve contar > como uma demonstração do enunciado gödeliano. Ademais, quando estamos > discutindo o que é ou não necessário para se demonstrar um resultado, > há que se considerar ainda uma certa ambiguidade na noção de > demonstração. Afinal, há boas e más demonstrações. Qual o valor de > se evitar esta ou aquela técnica se o preço é terminarmos com uma má > demonstração? > > Assim como qualquer resultado, as demonstrações do teorema da > indecidibilidade do Gödel podem ser inseridas num espectro com relação > a sua perspicácia e poder elucidatório. Num dos extremos está algo > como a demostração do próprio Gödel (talvez com algumas melhorias > inessenciais na codificação) e no outro extremo está aquela em que > simplesmente se assume o enunciado do teorema como hipótese. > > Afinal, o resultado é conhecido como teorema de Gödel e não teorema de > Finsler[2]. E, a julgar pela escassa correspondência entre os dois[3], > os detalhes técnicos, inclusive aritmetização, são uma importante > razão para essa nomenclatura. Portanto, não diria que seja matéria > apenas para hackers[3]. > > > Notas: > > [1] Em conversa privada, João Marcos indicou a excelente nota de Peter > Smith sobre o assunto: > > https://www.logicmatters.net/resources/pdfs/KleeneProof.pdf > > [2] Paul Finsler. Formale Beweise und die Entsheidbarkeit. Mathematische > Zeitschrift, Band 25, 1926, S. 676-682. > > [3] Kurt Gödel. Collected Works, Volume IV, p. 405-415. > > [3] A codificação particular escolhida por Gödel é, de fato, > inessencial, como observou o próprio Gödel, e pode ser substituída, > eventualmente por versões melhores, sem qualquer prejuízo. Porém, a > aritmetização em si me parece desempenhar um papel central. > > -- > Hermógenes Oliveira > > "The competent programmer is fully aware of the strictly limited size > of his own skull; therefore he approaches the programming task in full > humility, and among other things he avoids clever tricks like the > plague." Edsger W. Dijkstra > > -- > 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/AM6P192MB0488F538837579BDB703E438E9250%40AM6P192MB0488.EURP192.PROD.OUTLOOK.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/CAGJaJ%2B-3Q-8ikc0HSN1tw9b%2Bj93X3%3D71oChizN%2BFSeLhTuZcJQ%40mail.gmail.com.
