Bom esclarecimento do seu entendimento, Hermógenes, mas ainda há pontos que não estão estritamente corretos. Por exemplo,
> Como nós poderíamos, contudo, com base no resultado abstrato de TMR, > *demonstrar* o resultado de Gödel para uma formalização particular A da > aritmética? Seria necessário resolver a dicotomia, a qual, neste > caso, como nós já *sabemos*, mas gostaríamos de *demonstrar* > independentemente de Gödel, pende para um dos lados. Isto é, seria > necessário demonstrar que a função D de diagonalização é definível em > A. Essa demonstração, juntamente com a dicotomia já demonstrada em > TMR, nos daria então o resultado desejado, que é a indecidibilidade de > A. Na verdade, a diagonalização não é definível (o termo contemporâneo é representável) em absoluto (independente da nomeação das fórmulas), como já disse. Isso depende da nomeação das fórmulas. É trivial arrumar uma nomeação das fórmulas para a qual a diagonalização é definível, e uma para a qual a diagonalização não é. Apresentei isso. Eis aqui outra nomeação para a qual a diagonalização é definível: Nomeie as fórmulas que não são diagonalização com os termos para os números ímpares. Nomeie as diagonalizações dessas F's com os termos soma 'F' + 'F'. Nomeie as demais com os termos pares não utilizados. A seguinte fórmula representa a diagonalização: (x é par e y = x) ou (x é ímpar e y = x + x). > Consultando as definições relevantes em TMR, em particular a > definição de "definível", constatamos que a nossa missão seria > demonstrar um resultado existencial. E eis aqui, finalmente, a minha > alegação: > > - Uma *demonstração* de que a função D de diagonalização é definível > em A não pode dispensar de aritmetização. > O resultado existencial está demonstrado acima em duas linhas usando apenas a divisão entre pares e ímpares e a soma. TMR + esse resultado nos dá que a teoremicidade não é representável com essa nomeação. O que faltaria para concluir que a aritmética é indecidível? Faltaria demonstrar que todas as propriedades recursivas são representáveis com essa nomeação. Aí sim, poderíamos discutir se esse tipo de coisa, que aparece pela primeira vez no artigo do Godel, pode ser demonstrada sem aritmetização. É uma discussão interessante, podemos aprender algo levando isso para frente. Em especial, essa alegação *não* pretende ser interpretada das > seguintes formas: > > - Para se compreender o enunciado abstrato de TMR e sua dicotomia > subjacente é necessário apelar à aritmetização. > > - A noção de "aritmetização", ou "representabilidade da matemática" é > uma panaceia que remonta, pelo menos, aos tempos de Pitágoras. > > No próprio livro TMR, as demonstrações de indecidibilidade de teorias > particulares, especialmente no teorema 9, §II, assumem explicitamente > (nota de rodapé 7, §II) a recursividade da função D, e aqui se aplicam > as minhas observações anteriores sobre as propostas alternativas nos > moldes de Kleene. > > Em resumo, o enunciado abstrato de TMR nos fornece a dicotomia: > > ¬ D (diagonalização) ∨ ¬ T (teoremicidade) > > o que, para quem está familiarizado com a lógica proposicional > clássica, é equivalente a > > D → ¬T > Certo, inclusive é desse último modo que formulei em meu livro. Mas é preciso entender que há uma nomeação subjacente à dicotomia, e esta dicotomia se refere à falha de representabilidade com essa nomeação, para um lado ou para o outro. Se o resultado pretendido é, para além da dicotomia abstrata de TMR, a > indecidibilidade, isto é ¬T, de uma teoria particular A para a aritmética, > então, temos ainda que demonstrar D. Ora, pelas definições em > TMR, D é um enunciado existencial. Por isso eu falava de uma hipótese > existencial embutida. > ¬T não é o mesmo que indecidibilidade, é indefinibilidade com a nomeação subjacente. Isso precisa estar claro, ou o enunciado não será entendido. Para aplicar o teorema a primeira coisa é apresentar uma nomeação das fórmulas. Depois podemos mostrar D. Fiz isso acima, trivialmente. Disso não temos ainda a indecidibilidade, como mencionei, e talvez aqui esteja a sua alegação: Alegação do Hermógenes reformulada: A tarefa de (i) apresentar uma nomeação das fórmulas, (ii) representar a diagonalização com essa nomeação e (iii) mostrar que todas a propriedades recursivas são representáveis com essa nomeação para uma teoria T (aritmética? teoria de conjuntos?) não pode ser totalmente executada sem aritmetização. Ainda seria preciso esclarecer o que é aritmetização, porque a alegação acima pode ser verdadeira por definição (de aritmetização)! Mostrei que as etapas (i) e (ii) podem ser executadas sem aritmetização. > Está concedido que existem codificações distintas e, porventura, > melhores do que aquelas utilizadas por Gödel e que, por sua vez, podem > apelar para as mais variadas propriedades numéricas. Isso significa > que qualquer codificação funciona para se aritmetizar a teoria, desde > a noção de fórmula até a noção de derivação formal, e que basta > mencionar números para que se tenha aritmetização? Não me parece > razoável. > > Agora, nós poderíamos, eventualmente, fornecer critérios gerais (por > exemplo, por meio de definições) que uma codificação precisa obedecer > para desempenhar o papel pretendido na aritmetização. Isso não > significa, porém, prescindir da aritmetização. Seria apenas o mesmo > que dizer, em termos coloquiais: "Não enche o saco! Gödel já mostrou > que dá pra fazer! Ninguém tem tempo ou interesse nessas continhas. > Com exceção, talvez, dos hackers. Vá amolar um construtivista!" > Sim, a nomeação das fórmulas (codificação) precisaria ser tal que a diagonalização e todas as propriedades recursivas são representáveis com ela, como eu disse na minha primeira mensagem lá atrás. Com isso, TMR fornece as consequências desejadas (indecidibilidade, incompletude). Para ver se isso é possível sem aritmetização, é preciso explicar melhor o que é aritmetização. -- 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/CAExWzUJcvMewz%2B3MTjT2MopP8Me4XEnAn2OdMKVkJeVLxnegZQ%40mail.gmail.com.
