Existe: sobre o comprimento das provas. Na verdade Goedel apenas o enunciou em 36; foi provado nos anos 50. Usei-0 num artigo de 91, Undecidability and incompleteness in classical mechanics. É equivalente a um teorema de M. Blum em computação.
Sent from my iPhone On 07/03/2013, at 08:52, Elaine Pimentel <[email protected]> wrote: > Oi, João! > > Eu não conheço nenhum teorema de Gödel que trate do assunto (de fato, > não acredito que exista...). > > Sobre a sua pergunta, acho que é super interessante. Se considerarmos > a lógica clássica proposicional, então não há muito a dizer: > derivações normalizadas não utilizam lemas e são "minimais". Então eu > diria que a complexidade é a mesma. Se uma fórmula é um teorema > intuicionista, então o uso da dupla negação vai resultar em uma > derivação não normal, por exemplo. > > Já se passamos para a lógica de primeira ordem, temos a complicação do > existencial, pois é o único conectivo em cálculo de sequentes para o > qual a regra de introdução é não "invertível". Ou seja, você pode > decompor (pensando de baixo para cima) qualquer fórmula cujo conectivo > principal não seja um existencial que a "demonstrabilidade" fica > invariante. Então, para qualquer fórmula "demonstrável" -- para que > você não fique bravo comigo :) -- existe uma derivação mínimal dada > por "multifocusing" e portanto a complexidade pode ser medida apenas > pelo número de diferentes aplicações da regra existencial. > > Não sei como transformar isso para dedução natural, mas acredito que > basta definir uma classe de equivalência de derivações (normalizadas) > em dn para cada derivação "multifocused" em cálculo de sequentes. > > Eu acho esse assunto fascinante :) > > Abraço, > > Elaine. > > 2013/3/7 Joao Marcos <[email protected]>: >> Sobre derivações em dedução natural? >> >> JM >> >> 2013/3/6 Famadoria <[email protected]>: >>> Tem um teorema de Gödel sobre isso. >>> >>> Sent from my iPhone >>> >>> On 06/03/2013, at 19:38, Joao Marcos <[email protected]> wrote: >>> >>>> Gostaria de fazer uma consulta simples entre os colegas com mais >>>> intuição do que eu sobre este assunto. >>>> >>>> Um aluno me perguntou como poderia fazer para "comparar o nível de >>>> dificuldade de duas derivações", em dedução natural. A gente faz em >>>> sala de aula aquelas asserções ingênuas, do tipo "se você usou a regra >>>> do absurdo clássico, trata-se de uma derivação não trivial", "se você >>>> usou regras com descarte, a derivação é potencialmente mais complexa", >>>> "se você precisou usar lemas, a derivação não é tão básica assim", e >>>> até "se você construiu sua derivação de forma construtiva, ela pode >>>> até ter custado mais, mas é mais confiável"... >>>> >>>> Pois bem, minha primeira sugestão ao aluno foi que comparasse o nível >>>> de dificuldade de duas derivações executando dois passos: primeiro, >>>> converta estas derivações para uma forma *normalizada*; em seguida, >>>> conte o número de nós destas versões normalizadas, e o número de >>>> aplicações da regra do absurdo clássico. A Valeria me chamou a >>>> atenção em privado para a necessidade de considerar também outras >>>> variáveis, como o numero de regras usadas, e não somente o numero de >>>> regras do absurdo. >>>> >>>> E o que acham os colegas? Como vocês comparariam, em princípio, o >>>> *nível de dificuldade* de duas derivações, digamos, em dedução >>>> natural? >>>> >>>> Abraços, >>>> Joao Marcos >> >> -- >> http://sequiturquodlibet.googlepages.com/ >> _______________________________________________ >> Logica-l mailing list >> [email protected] >> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > > > > -- > Elaine. > ------------------------------------------------- > Elaine Pimentel - DMat/UFMG > > Address: Departamento de Matematica > Universidade Federal de Minas Gerais > Av Antonio Carlos, 6627 - C.P. 702 > Pampulha - CEP 30.161-970 > Belo Horizonte - Minas Gerais - Brazil > Phone: 55 31 3409-5970/3409-5994 > Fax: 55 31 3409-5692 > > htps://sites.google.com/site/elainepimentel/ > -------------------------------------------------------- > _______________________________________________ > Logica-l mailing list > [email protected] > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
