Re: [Logica-l] Kurt Gödel and the mechanization of mathematics
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 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
Re: [Logica-l] Kurt Gödel and the mechanization of mathematics
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 > 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
Re: [Logica-l] Kurt Gödel and the mechanization of mathematics
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.
Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics
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. (TMR) 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. Essa versão é fácil de demonstrar, como tentei explicar na mensagem anterior. Não é preciso passar por funções recursivas para isso. Nada de aritmética. Essa seria uma versão abstrata, livre de aritmética e de aritmetização, do que chamamos hoje de teorema de Tarski da indefinibilidade da verdade, apesar de Tarski atribuir a Godel em seu livro. No meu livro coloquei essencialmente a mesma coisa, como expliquei no prefácio. Fiz algo similar para o segundo teorema também. Abraço > Em 28 de dez de 2019, à(s) 12:52, Joao Marcos escreveu: > > 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 certo, a necessária "representação > formal da Matemática" pode ser feita de variadas formas alternativas. > (Os detalhes da demonstração original gödeliana são de interesse > apenas para hackers!) Neste sentido, como ainda não tive tempo de > trabalhar com o seu livro, Rodrigo, posso dizer que aprecio > particularmente o interessante livro de Amílcar e Cristina Sernadas, > "Foundations of Logic and Theory of Computation", onde a noção de > computabilidade é definida sobre strings de alfabetos arbitrários; > contudo, a noção formal de _representabilidade_, ali, também recorre > diretamente a teorias da Aritmética --- como de costume. > > Abraços, > Joao Marcos > > >> On Thu, Dec 26, 2019 at 10:23 AM Rodrigo Freire wrote: >> >> [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 >> representar a matemática formalmente. É assim que está no meu livro, Tópicos >> em lógica de primeira ordem, que pode ser baixado livremente. >> >> Suponha que há uma teoria formal de primeira ordem T que “representa” a >> matemática. Como a metamatematica de T é parte da matemática, T é capaz de >> “representar” essa parte também. Isso deve implicar o que entendo por >> codificação: >> >> 1) há uma correspondência unívoca entre fórmulas de T e termos fechados de T >> (Para poder falar de suas fórmulas e “representar” sua metamatemática, T >> deve ter nomes não ambíguos para as fórmulas. Por exemplo, T deve ser capaz >> de dizer de uma fórmula que ela é bem formada. Para isso é preciso nomear a >> fórmula sem ambiguidade. Usamos ‘F’ como nome de F). >> >> 2) tudo o que é decidido na metamatemática, é decidido por um método de >> cálculo matemático, portanto deve ser decidido em T: Tudo que é calculável >> deve ser calculável em T, pois T representa toda a matemática. (T deve >> representar predicados e funções recursivas, pois qualquer método matemático >> de cálculo é representável em T). >> >> 1) + 2) é a codificação. Vamos ver o quanto disso é necessário para a >> demonstração que se T é consistente, a sua teoremicidade não é calculável em >> T. >> >> **Da codificação segue que a operação de diagonalização nas fórmulas (a >> operação que associa a fórmula F(‘F’) a qualquer fórmula F) é calculável em >> T. ** >> >> Se a propriedade metamatemática de ser teorema de T fosse calculável, então >> seria calculável em T. Isso significa que T seria capaz de deduzir B(‘F’), >> quando F é teorema, e ~B(‘F’), quando F não é teorema, para alguma fórmula >> B(x) de T que dizemos representar a teoremicidade. >> >> Mas como a diagonalização é calculável em T, é possível construir uma >> sentença G tal que G é equivalente à ~B(‘G’) em T. Portanto, se T não deduz >> G, então, pela hipótese que a propriedade de ser teorema é calculável, a não >> dedução de G é calculável em T, ou seja, T deduz ~B(‘G’). Mas ~B(‘G’) é >> equivalente a G em T, e concluímos que T deduz G. Novamente pela hipótese, a >> teoremicidade de G é calculável em T, portanto T deduz B(‘G’), que é >> equivalente a ~G. Portanto, T é inconsistente. >> >> Para essa demonstração basta supor 1) acima e apenas que a operação de >> diagonalização é calculável em T. Essa parte da codificação 1) + 2) que é >> requerida.
Re: [Logica-l] Re: Kurt Gödel and the mechanization of mathematics
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 certo, a necessária "representação formal da Matemática" pode ser feita de variadas formas alternativas. (Os detalhes da demonstração original gödeliana são de interesse apenas para hackers!) Neste sentido, como ainda não tive tempo de trabalhar com o seu livro, Rodrigo, posso dizer que aprecio particularmente o interessante livro de Amílcar e Cristina Sernadas, "Foundations of Logic and Theory of Computation", onde a noção de computabilidade é definida sobre strings de alfabetos arbitrários; contudo, a noção formal de _representabilidade_, ali, também recorre diretamente a teorias da Aritmética --- como de costume. Abraços, Joao Marcos On Thu, Dec 26, 2019 at 10:23 AM Rodrigo Freire wrote: > > [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 > representar a matemática formalmente. É assim que está no meu livro, Tópicos > em lógica de primeira ordem, que pode ser baixado livremente. > > Suponha que há uma teoria formal de primeira ordem T que “representa” a > matemática. Como a metamatematica de T é parte da matemática, T é capaz de > “representar” essa parte também. Isso deve implicar o que entendo por > codificação: > > 1) há uma correspondência unívoca entre fórmulas de T e termos fechados de T > (Para poder falar de suas fórmulas e “representar” sua metamatemática, T deve > ter nomes não ambíguos para as fórmulas. Por exemplo, T deve ser capaz de > dizer de uma fórmula que ela é bem formada. Para isso é preciso nomear a > fórmula sem ambiguidade. Usamos ‘F’ como nome de F). > > 2) tudo o que é decidido na metamatemática, é decidido por um método de > cálculo matemático, portanto deve ser decidido em T: Tudo que é calculável > deve ser calculável em T, pois T representa toda a matemática. (T deve > representar predicados e funções recursivas, pois qualquer método matemático > de cálculo é representável em T). > > 1) + 2) é a codificação. Vamos ver o quanto disso é necessário para a > demonstração que se T é consistente, a sua teoremicidade não é calculável em > T. > > **Da codificação segue que a operação de diagonalização nas fórmulas (a > operação que associa a fórmula F(‘F’) a qualquer fórmula F) é calculável em > T. ** > > Se a propriedade metamatemática de ser teorema de T fosse calculável, então > seria calculável em T. Isso significa que T seria capaz de deduzir B(‘F’), > quando F é teorema, e ~B(‘F’), quando F não é teorema, para alguma fórmula > B(x) de T que dizemos representar a teoremicidade. > > Mas como a diagonalização é calculável em T, é possível construir uma > sentença G tal que G é equivalente à ~B(‘G’) em T. Portanto, se T não deduz > G, então, pela hipótese que a propriedade de ser teorema é calculável, a não > dedução de G é calculável em T, ou seja, T deduz ~B(‘G’). Mas ~B(‘G’) é > equivalente a G em T, e concluímos que T deduz G. Novamente pela hipótese, a > teoremicidade de G é calculável em T, portanto T deduz B(‘G’), que é > equivalente a ~G. Portanto, T é inconsistente. > > Para essa demonstração basta supor 1) acima e apenas que a operação de > diagonalização é calculável em T. Essa parte da codificação 1) + 2) que é > requerida. Daí concluímos que se a teoremicidade for calculável em T, então T > é inconsistente. É isso que fiz em meu livro, uma versão abstrata que não > menciona funções recursivas. Todos os detalhes podem ser encontrados lá. > > Como já foi dito, há outras demonstrações, mas acho que essa é a que está > mais diretamente ligada à ideia fundacional: se é possível uma representação > formal da matemática em um sistema formal T, então a teoremicidade de T não é > calculável (na metamatemática de T ou na própria T), a menos que T seja > inconsistente. > > > > > Em 25 de dez de 2019, à(s) 14:15, Carlos Gonzalez > escreveu: > > > 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? > > Também pode usar técnicas de teoria de modelos para construir modelos > standard e outras, como ultraprodutos, para modelos não standard. Técnicas > matemáticas não finitárias. > > Um recurso divertido é acrescentar a AP uma constante nova "c" e um conjunto > infinito de axiomas: > (s é a função sucessor) > não ( c = 0) > não ( c = s0) > não ( c =
