Ok Valeria, bom trabalho. Vou encerrar com três brevíssimas observações:
-Não duvido que para alguma noção razoável de complexidade a função sucessor é menos complexa que a exponenciação. Pode ser uma noção de recursos para a normalização forte de lambda termos ou outra coisa. Isso não é motivo para acreditar na inconsistência de PRA, pelo contrário. -O que não me parece fazer sentido é a inferência: "complexo implica não existe". Parece insistência minha, mas Nelson não afirma só que a tetração é mais complexa que o sucessor. Ele afirma que não existe "m tetra n", para argumentos n e m exibidos. -O que eu duvido portanto é que uma noção razoável de existência de números seja baseada em uma noção de complexidade, como Nelson acredita. Em última análise, por tudo que já escrevi, não me parece inteligível a inferência "complexo implica não existe". Abraço Rodrigo 2011/9/30 Valeria de Paiva <valeria.depa...@gmail.com> > Rodrigo, > Deixa eu tentar explicar o que eu acho que o Nelson *pode* estar querendo > dizer. > > >Você pode mudar o sentido de número e decretar que números acima de algum > > valor não existem. A função sucessor não é mais total, etc. Mas isso é > > destruir a noção de número. > > sim, mas nao 'e isso que queremos. e acho que nao 'e isso que o Nelson > esta' fazendo. a funcao sucessor 'e total, como a gente normalmente > considera, pode ser descrita pelo lambda termo (\lambda x. x+1) e 1 'e > um numero legal e somar com 1 tambem funciona bem. > > a gente tambem pode definir adicao e multiplicacao usando lambda > termos e podemos talvez pensar no tempo/espaco que leva pra normalizar > o termo correspondente. isto 'e no esforco/trabalho que da' pra > reduzir \lambda x. ( suc(suc(suc(Zero)))) + \lambda x. > ((suc(suc(Zero)))) pra 5. > > > Dai talvez faca algum sentido dizer que superexponenciacao 'e > diferente da funcao sucessor e que uma sempre termina, mas a outra > nao. nao sei se 'e isso que ele esta dizendo e em vez de ficar falando > bobagens eu devia era ler o famoso documento de 100 paginas, mas > pensando em reducoes de lambda termos eu pelo menos consigo ver que > pode existir uma nocao de prova bem parecida com a minha, que leva em > consideracao alguma nocao de complexidade para produzir um resultado > aritmetico. > > dai que pode existir uma nocao nada artificial que coloque restricoes > nas nocoes classicas e leve o Nelson a dizer que superexponenciacao > nao termina sempre(ou melhor que nao podemos garantir que a > superexponenciacao sempre termine). eu nao sei se 'e isso que ele > esta' dizendo, e achei que alguem saberia me dizer, sem muito esforco. > > obrigada pela conversa, > Valeria > > 2011/9/30 Rodrigo Freire <freires...@gmail.com>: > > Oi Valéria > > > > Até onde posso compreender, o Nelson acredita que PRA é inconsistente por > > acreditar que algumas funções primitivas recursivas não são totais. Não > > consigo entender o que isso significa. > > > > Mais especificamente: Nelson acredita que superexponenciação não é total. > > > > Considere a seguinte sequencia de funções primitivas recursivas: > constante > > igua a 0, sucessor, soma, produto, exponenciação com base 2, > > superexponenciação com base 2. Nelson acredita que uma dessas não é total > e > > não é 0 nem sucessor. Considere a primeira. Chamemos ela de f. Considere > o > > primeiro argumento n em que f não "dá resultado". O que acontece com o > > algoritmo que calcula f(n) em termos das funções primitivas recursivas > > anteriores (que são totais) e de f para argumentos menores que n (que > > existem)? > > > > Você pode mudar o sentido de número e decretar que números acima de algum > > valor não existem. A função sucessor não é mais total, etc. Mas isso é > > destruir a noção de número. > > > > > > Também é possível mudar o que significa "consistência". Por exemplo > dizendo > > que não há provas de complexidade menor ou igual a n de 0=1, para alguma > > noção de complexidade e algum n. Aí o problema da consistência pode > passar a > > fazer sentido para PRA. No sentido usual do termo, o problema da > > consistência não se coloca para PRA. > > De novo, o que está acontecendo é uma destruição da noção de prova, e da > > noção dependente de consistência. As regras de inferência não são mais > > totais? Por que não? > > > > > > De acordo com a sua pergunta: essas não são as noções de número e de > prova > > que fazem mais sentido, que colocam restrições artificiais nas noções > > clássicas sem nenhuma razão para fazer isso. > > > > Essa citação do Harvey Friedman expressa a situação: > > > > "I raised just this objection with the (extreme) ultrafinitist > Esenin-Volpin > > during a lecture of his. He asked me to be more specific. I then > proceeded > > to start with 2^1 and asked him whether this is “real” or something to > that > > effect. He virtually immediately said yes. Then I asked about 2^2, and he > > again said yes, but with a perceptible delay. Then 2^3, and yes, but with > > more delay. This continued for a couple of more times, till it was > obvious > > how he was handling this objection. Sure, he was prepared to always > answer > > yes, but he was going to take 2^100 times as long to answer yes to 2^100 > > then he would to answering 2^1. There is no way that I could get very far > > with this." > > > > > > > > Abraço > > Rodrigo > > > > > > 2011/9/30 Valeria de Paiva <valeria.depa...@gmail.com> > >> > >> oi Rodrigo, > >> > >> Obrigada pela mensagem abaixo, eu tb estou na mesma situacao de: > >> >não entendo nada disso e esses palpites apenas expressam uma > >> > sensação, não tem bases muito sólidas. > >> "gut feelings", sem argumentos solidos, aqui tambem... > >> > >> eu tentei uma vez ensinar complexidade pra computacao sem usar logica > >> classica, usando programas funcionais e raciocinio constructivo, mas > >> nao consegui fazer nem a primeira aula direito. Alguem devia > >> faze-lo... > >> > >> Mas a minha visao 'e diferente quanto a: > >> >O Shoenfield adaptou a interpretação dialética para aplicá-la direto a > PA > >> > sem passar por HA. Então não sei se essa preocupação com a tradução de > >> > Godel > >> > é realmente significativa. > >> voce leu a minha preocupacao com HA da maneira inversa do que a que eu > >> pretendia. eu gosto de passar por HA, o que eu gostaria na verdade e' > >> de fazer logica classica mais parecida com logica intuicionista, de > >> providenciar Curry-Howard pra logica classica de uma maneira > >> canonica...dai o que eu quero 'e extrair das preocupacoes do Nelson, > >> as que eu compartilho... > >> > >> eu tambem acredito que PRA 'e consistente, por isso gostaria de > >> entender melhor porque o Nelson acha que nao 'e, pois nao concordo > >> contigo quando voce diz que ``dizer que PRA é inconsistente é sem > >> sentido". Pode ser que nao faca sentido da forma como as definicoes > >> estao organizadas, mas a regra do jogo 'e descobrir quais sao as > >> definicoes que fazem mais sentido pra gente, nao? qual 'e a definicao > >> de numero natural, de principio de inducao que faz mais sentido e > >> prova mais teoremas, sem introduzir conceitos duvidosos que nem o > >> "terceiro excluido"--essas sao as perguntas que queremos responder, > >> nao? > >> > >> obrigada pelas explicacoes, > >> Valeria > >> > >> > > > > > > -- > Valeria de Paiva > http://www.cs.bham.ac.uk/~vdp/ > http://valeriadepaiva.org/www/ > _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
