Olá, Tony: Creio que o tal "rapaz" conhece os teoremas de Gödel, e principalmente de "questões de implementação". Talvez valha a pena você dar uma conferida no blog dele: http://math.andrej.com/ ou em seu perfil de publicações: http://scholar.google.com/citations?user=u7JW7bIAAAAJ&hl=en
Mais: se você tiver alguma dúvida sobre matemática computacional você pode perguntar diretamente para ele no MathOverflow. http://mathoverflow.net/users/1176/andrej-bauer Ele costuma responder de forma extremamente eficiente. A palestra dele sobre ensino no TEDxLjubljana é também bastante bacana: http://www.youtube.com/watch?v=Ms3N-Sjzudw [ ]s, Joao Marcos 2012/12/30 Tony Marmo <[email protected]>: > Então João, Aristóteles já tinha proposições indefinidas, que não eram nem > universais, nem particulares. A questão da implementação vai depender de > qual lógica ou sistema se tem em mente. O rapaz que escreveu o tópico não > desenvolveu esse lado da argumentação, não indicou que tipo de princípios > lógicos acha mais compatíveis com os problemas matemáticos. Ele, portanto, > apenas está reagindo à doutrina de que necessariamente pensamento > clássico=matemático e que tudo se resolve na primeira ordem. Só que os > argumentos dele se confinam ao campo das observações matemáticas, do modo > que ele as pode entender. E mais: ele deveria ler algo sobre os teoremas de > Goedell, que poderiam ser-lhe de grande interesse. > > Em 30 de dezembro de 2012 08:31, Joao Marcos <[email protected]> escreveu: > >> Posso não ter entendido o que você quer dizer com "implementação". >> Vale notar que em Isabelle, por exemplo, há três tipos de variáveis: >> livres, ligadas/mudas, e esquemáticas. Apenas as variáveis >> esquemáticas podem ser instanciadas. A "quantificação implícita" >> sobre as variáveis livres ocorre apenas no final de uma demonstração, >> quando tais variáveis (de qualquer ordem) são convertidas em >> esquemáticas. De todo modo, tal conversão pode não ser interessante >> caso trabalhemos com lógicas não-monotônicas (com as quais Isabelle em >> princípio não trabalha). >> >> * * * >> >> O conteúdo do texto do Bauer linkado abaixo, de todo modo, tinha um >> objetivo mais conceitual, e terá seu apelo não apenas a teóricos de >> tipos mas também a categoristas, para além de lógicos de todas as >> demais estirpes. >> >> Confesso que a "razão 3" em particular me parece fraca, pois a objeção >> é eliminada se trabalhamos com a "definição correta" de *substituição* >> (substituir no contexto da quantificação citada resulta na mesma >> proposição de entrada). >> >> []s, JM >> >> >> On Sun, Dec 30, 2012 at 2:37 AM, Tony Marmo <[email protected]> wrote: >> > Estou de pleno acordo com a proposição título. A questão é saber como >> > implementá-la. >> > >> > 2012/12/29 Joao Marcos <[email protected]> >> >> >> >> um presente de natal de andrej bauer: >> >> >> >> >> >> >> >> http://math.andrej.com/2012/12/25/free-variables-are-not-implicitly-universally-quantified/ >> >> >> >> >> >> jm >> >> _______________________________________________ >> >> Logica-l mailing list >> >> [email protected] >> >> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l >> > >> > >> >> >> >> -- >> http://sequiturquodlibet.googlepages.com/ > > -- http://sequiturquodlibet.googlepages.com/ _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
