Não usou dedução natural e nem precisa; poderíamos codificar em linguagem binária a dedução. E se aplica o teorema de Goedel sobre o comprimento das provas.
Sent from my iPhone On 07/03/2013, at 08:01, Joao Marcos <[email protected]> wrote: > 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
