A hipótese que T tem nomes para suas fórmulas significa apenas que as fórmulas de T e os termos fechados de T estão em correspondência 1-1: a cada fórmula F corresponde um termo fechado ‘F’. Nem precisa mencionar aritmética. Qualquer teoria em que o numero de fórmulas é igual ao número de termos fechados satisfaz isso por definição.
Que T não representa simultaneamente sua diagonalização de fórmulas (a operação que associa F(‘F’) à fórmula F) e sua teoremicidade é a conclusão (em TMR), e também dispensa qualquer menção à aritmética. Não é preciso qualquer menção, por exemplo, às funções recursivas nesse teorema. Onde está a aritmetização como hipótese? > Em 28 de dez de 2019, à(s) 17:10, Hermógenes Oliveira > <olive...@daad-alumni.de> escreveu: > > 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/817494C6-4421-4BCD-85CC-9E31622A6138%40gmail.com.
