> O que estou propondo, muito provavelmente também de modo ingênuo :) , é que > a noção de verdade não precisa (embora possa) adequar-se a certas restrições > de efetividade que a noção de demonstrabilidade precisa.
Confesso que não sinto segurança para afirmar o quanto a noção de "efetividade" seria importante nestas tarefas... Mas eu arriscaria perguntar antes ao pessoal que trabalha especificamente com _complexidade computacional_ o que eles acham sobre isto! >> Penso que aqui há um equívoco, ligado a nossa discussão anterior. As >> *regras sintáticas de boa-formação* são em geral _completamente >> diferentes_ das *regras de inferência* que você associa a suas >> expressões bem-formadas. > > Elas não são tão diferentes assim. Ambas são regras de manipulação > simbólica. Pense na noção de fórmulas como tipos (o isomorfismo > Curry-Howard). O que de um lado do isomorfismo envolve regras de boa > formação e regras de inferência, do outro lado envolve somente regras de boa > formação, de termos e de tipos. Uma prova torna-se um lambda-termo > gramaticalmente (ou sintaticamente) bem formado. É um exemplo interessante, mas que eu acredito poder ser melhor explicado (a sintaxe de um sistema pode ser o formalismo dedutivo de outro, ou vice-versa --- vide "inferência de tipos")... Bom, mas para não repetir simplesmente um exemplo que já dei antes sobre a diferença entre regras sintáticas e regras de um sistema formal dedutivo, prefiro simplesmente apontar para as duas seguintes seções do _excelente_ verbete sobre "Natural Deduction" na Wikipedia: http://en.wikipedia.org/wiki/Natural_deduction#Judgments_and_propositions http://en.wikipedia.org/wiki/Natural_deduction#Introduction_and_elimination Note-se como os meta-predicados "true" e "prop" são de fato bem diferentes, em geral. Esta é, de todo modo, uma distinção básica para compreender como a "proof-theoretic semantics" faz o trabalho que deveria fazer. Mas eu não deveria estar me arriscando a dizer isso para você, que sabe obviamente muito mais do assunto do que eu! ;-) >> Conheço zilhões de sistemas lógicos que não foram originalmente >> propostos baseados em qualquer tipo de noção de "consequência formal" >> e que tiveram sua noção de consequência originalmente definida, ao >> invés, por meios "semânticos" ou "algébricos". Mais ainda, muitos >> destes sistemas são extremamente úteis e bem motivados, e jamais >> possuíram qualquer um sistema dedutivo formal minimamente decente >> associado (por exemplo, foram axiomatizados à la Hilbert, ou nem foram >> axiomatizados, ou nem são recursivamente axiomatizáveis). > > Bem, mas nenhum destes "zilhoes de sistemas lógicos" é um sistema formal. E > eu falei de sistemas formais. Estes sistemas são cálculos, estruturas > algébricas,... Se eu tivesse uma índole reformista eu poderia, talvez sem > razão, me empenhar em proibir o uso da palavra lógica quando aplicada a > estes sistemas sem sintaxe bem definida. Mas não farei isso. Aceito que eles > são lógicas, mas eles não são sistemas formais. Os sistemas podem ter "sintaxe" muito bem definida, mas terem suas definições de consequência subjacentes apresentadas de maneira absolutamente _precisa_ e "efetiva" usando estratégias que você muito provavelmente não identificaria como "formalismos dedutivos"... >> Bom, há aparentemente sistemas de "consequência formal" que incluem >> regras infinitárias... Há especialistas no assunto, nesta lista. > > Aqui eu confesso que o caráter meramente especulativo do que disse sobre a > ininteligibilidade de sentenças infinitas é ainda maior. Baseado apenas em > rasa intuição. Opiniões mais fundamentadas seriam ótimas. Espere: falávamos em regras com um conjunto infinito de premissas ou em sentenças de comprimento infinito? JM -- http://sequiturquodlibet.googlepages.com/ _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
