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
