Eu falei que ia fazer um programa de computador que prova teoremas. É muito difícil fazer isso. É possível mas dá muito trabalho. Não sei quanto tempo vou levar. Pra quem gostaria de ver um desses, entre no site http://www.metamath.org
Especialmente difícil é fazer substituição de uma variável numa fórmula. Enfim, quando tiver pronto, eu devo pôr o algoritmo aqui, deve ficar bem grande.
Se eu tivesse um pouco mais organizado com os estudos estaria postando mais.
Por enquanmto é só fase de testes mesmo.
Então se poucos estão lendo, sem muitos problemas... Mas só por enquanto...
sexta-feira, 21 de novembro de 2008
sexta-feira, 7 de novembro de 2008
Provando Teoremas com um Computador
Parece difícil de acreditar mas dá pra fazer isso! Vou fazer isso em linguagem Pascal.
Primeiro passo: codificar as fórmulas matemáticas no computador.
Pensei em duas maneiras de codificar: uma recursiva e outra direta.
Na codificação direta fazemos assim: a fórmula é um array[1..N] of integer, onde N é um número bem grande (depende da memória do seu computador).
Então codificamos os símbolos lógicos ¬[1], ^[2], v[3], →[4], A[5], E[6], =[7], ([8], )[9], xn[10n],l cn[10n+1], fn[10n+2], Pn[10n+3]. xn, cn, fn e Pn são as variáveis, constantes, funcionais e predicados da teoria.
E cada símbolo é substituído pelo número ao lado.
Na forma recursiva, que eu prefiro, faz assim: toda fórmula não atômica é um array[1..11] of integer, onde o primeiro número é um conectivo (representado por um número de 1 a 6, como acima), o terceiro e o quarto são os números dos argumentos (que podem ser fórmulas ou variáveis). Uma fórmula atômica é um array[1..11] of integer onde o primeiro é o número do predicado, e os seguintes os números dos termos. E um termo é um array[1..11] of integer onde o primeiro é o número do funcional, e os seguintes os números dos termos ou variáveis. Pode-se padronizar que variáveis sejam números pares e termos compostos números ímpares, de semelhante modo fórmluas atômicas com números pares.
Depois extende-se isso para conjuntos de fórmulas e termos: um array[1..N,1..11] of integer, onde N é um número muito grande. Esse arranjo é a lista das fórmulas.
Por exemplo, como escrever Ax(x e R→(x²>=0)). Numeramos as fórmulas 2: x²>=0; 4: x e R; 1: x e R→(x²>=0); 3: Ax(x e R→(x²>=0)). Então o array fica assim:
[→,2,4,...]
[>=,x²,0,...]
[A,x,1,...]
[e,x,R,...]
Mais tarde eu ponho como fica o programa...
Primeiro passo: codificar as fórmulas matemáticas no computador.
Pensei em duas maneiras de codificar: uma recursiva e outra direta.
Na codificação direta fazemos assim: a fórmula é um array[1..N] of integer, onde N é um número bem grande (depende da memória do seu computador).
Então codificamos os símbolos lógicos ¬[1], ^[2], v[3], →[4], A[5], E[6], =[7], ([8], )[9], xn[10n],l cn[10n+1], fn[10n+2], Pn[10n+3]. xn, cn, fn e Pn são as variáveis, constantes, funcionais e predicados da teoria.
E cada símbolo é substituído pelo número ao lado.
Na forma recursiva, que eu prefiro, faz assim: toda fórmula não atômica é um array[1..11] of integer, onde o primeiro número é um conectivo (representado por um número de 1 a 6, como acima), o terceiro e o quarto são os números dos argumentos (que podem ser fórmulas ou variáveis). Uma fórmula atômica é um array[1..11] of integer onde o primeiro é o número do predicado, e os seguintes os números dos termos. E um termo é um array[1..11] of integer onde o primeiro é o número do funcional, e os seguintes os números dos termos ou variáveis. Pode-se padronizar que variáveis sejam números pares e termos compostos números ímpares, de semelhante modo fórmluas atômicas com números pares.
Depois extende-se isso para conjuntos de fórmulas e termos: um array[1..N,1..11] of integer, onde N é um número muito grande. Esse arranjo é a lista das fórmulas.
Por exemplo, como escrever Ax(x e R→(x²>=0)). Numeramos as fórmulas 2: x²>=0; 4: x e R; 1: x e R→(x²>=0); 3: Ax(x e R→(x²>=0)). Então o array fica assim:
[→,2,4,...]
[>=,x²,0,...]
[A,x,1,...]
[e,x,R,...]
Mais tarde eu ponho como fica o programa...
terça-feira, 4 de novembro de 2008
Teorema de Gödel
Algumas pessoas já ouviram falar desse teorema. É um dos teoremas mais impactantes da Matemática do século passado. Diz que em toda teoria matemática que contenha a aritmética existem afirmações que não podem ser provadas...
A maioria das pessoas que ouviram falar desse teorema talvez não entenda seu verdadeiro enunciado, e talvez tenha muitas dificuldades pra entender sua demonstração (que raramente é posta na íntegra em textos da internet). Tanto é que alguns não Matemáticos refutam esse teorema (apesar de que "refutar teoremas" não faz muito sentido em Matemática, o que se faz é verificar se uma demonstração está correta ou não). Fala-se muita besteira na internet a respeito desse teorema por causa da falta de avisos contidos nos textos sobre o assunto. Por exemplo: Gödel não provou que a Matemática é inconsistente, mas apenas que teorias fortes são incompletas, no sentido que existem perguntas que a teoria não poderá responder. E isso apenas para teorias formais, ou seja, teorias definidasem um sentido preciso de lógica simbólica.
O que ele provou foi:
Toda teoria lógica formal em que se consegue definir as constantes, símbolos funcionais e relacionais da aritmética de Peano de primeira ordem, não é completa e (omega)consistente ao mesmo tempo. Não é completa no sentido de que existe uma fórmula sem variáveis livres (wff) que não pode ser provada verdadeira nem falsa pela teoria. E não é (omega)consistente no sentido que ou não é consistente ou existe uma fórmula (Existe x em IN tal que P(x)), tal que P(x) não vale pra nenhum x em IN no modelo correspondente a teoria. Mais tarde provaram que tal teoria não pode ser consistente e completa ao mesmo tempo.
Se a pessoa não entendeu o enunciado acima é melhor nem tentar comentar por aí sobre o teorema, fazer reflexões filosóficas esdrúxulas sobre o mesmo, e pior ainda: tentar refutá-lo (as tentativas de fazer isso levam a artigos risíveis do ponto de vista matemático, até mesmo uma falta de respeito com quem faz ciência de modo sério).
Bom, qual é a interpretação intuitiva do teorema?? Bom, uma delas é: não existe um algoritmo que produza todas as verdades aritméticas, ou mais informalmente, não existe um programa de computador que seja capaz de decidir exatamente quais fórmulas sobre os números naturais são válidas, por maior que ele seja. Em compensação, pode-se produzir um computador que produza somente verdades aritméticas, mas não todas elas.
A maioria das pessoas que ouviram falar desse teorema talvez não entenda seu verdadeiro enunciado, e talvez tenha muitas dificuldades pra entender sua demonstração (que raramente é posta na íntegra em textos da internet). Tanto é que alguns não Matemáticos refutam esse teorema (apesar de que "refutar teoremas" não faz muito sentido em Matemática, o que se faz é verificar se uma demonstração está correta ou não). Fala-se muita besteira na internet a respeito desse teorema por causa da falta de avisos contidos nos textos sobre o assunto. Por exemplo: Gödel não provou que a Matemática é inconsistente, mas apenas que teorias fortes são incompletas, no sentido que existem perguntas que a teoria não poderá responder. E isso apenas para teorias formais, ou seja, teorias definidasem um sentido preciso de lógica simbólica.
O que ele provou foi:
Toda teoria lógica formal em que se consegue definir as constantes, símbolos funcionais e relacionais da aritmética de Peano de primeira ordem, não é completa e (omega)consistente ao mesmo tempo. Não é completa no sentido de que existe uma fórmula sem variáveis livres (wff) que não pode ser provada verdadeira nem falsa pela teoria. E não é (omega)consistente no sentido que ou não é consistente ou existe uma fórmula (Existe x em IN tal que P(x)), tal que P(x) não vale pra nenhum x em IN no modelo correspondente a teoria. Mais tarde provaram que tal teoria não pode ser consistente e completa ao mesmo tempo.
Se a pessoa não entendeu o enunciado acima é melhor nem tentar comentar por aí sobre o teorema, fazer reflexões filosóficas esdrúxulas sobre o mesmo, e pior ainda: tentar refutá-lo (as tentativas de fazer isso levam a artigos risíveis do ponto de vista matemático, até mesmo uma falta de respeito com quem faz ciência de modo sério).
Bom, qual é a interpretação intuitiva do teorema?? Bom, uma delas é: não existe um algoritmo que produza todas as verdades aritméticas, ou mais informalmente, não existe um programa de computador que seja capaz de decidir exatamente quais fórmulas sobre os números naturais são válidas, por maior que ele seja. Em compensação, pode-se produzir um computador que produza somente verdades aritméticas, mas não todas elas.
segunda-feira, 3 de novembro de 2008
Sem comentários...
Eu espero que esse blog não seja semanal.
Mas até agora poucos visitantes aqui, nenhum comentário do pessoal sobre o meu pré-blog. Ainda não sei exatamente que rumo tomarei, só o tempo dirá. Espero que ele não siga ignorado, preciso de uma forma pra divulgar.
Mas até agora poucos visitantes aqui, nenhum comentário do pessoal sobre o meu pré-blog. Ainda não sei exatamente que rumo tomarei, só o tempo dirá. Espero que ele não siga ignorado, preciso de uma forma pra divulgar.
Assinar:
Postagens (Atom)