alo todos, Pois e', eu tambem acho que Doria se enganou nessa. eu tenho as obras completas do Goedel and por via das duvidas dei uma "googlada", mas nao achei nada..sem contar que os metodos de descricao de provas nao eram muito sofisticados. o calculo de sequentes 'e dos anos 30 e a deducao natural so' mostrou que funcionava mesmo nos anos 60, ne?
mas eu nao concordo com Elaine qdo ela diz: >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. tem muita coisa a se dizer sim e a complexidade nao deve ser a mesma. De um olhada no trabalho do Sam Buss em k-provabilidade usando os logic flow graphs dele, http://www.math.ucsd.edu/~sbuss/ResearchWeb/kprove/paper.pdf... acho que a medida de numero de usos de regra do absurdo 'e so' pra comecar... Mas concordo plenamente com Elaine que o assunto 'e fascinante!! abracos, Valeria 2013/3/7 Elaine Pimentel <[email protected]> > 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 > -- Valeria de Paiva http://www.cs.bham.ac.uk/~vdp/ http://valeriadepaiva.org/ _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
