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.
