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
