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/ _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
