Olá, Daniel: Aponho apenas alguns comentários breves ao que você escreveu, para não correr o risco de me repetir muito.
>> 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! ;-) > > Nada demais aqui. Marcar as fórmulas com "prop" apenas indica que a regra é > de boa formação, é sintática no sentido estrito, e marcar as fórmulas com > "true", indica que se trata de regras de inferência-dedução. A própria > necessidade desta marcação e a semelhança (de recursos formais) entre os > dois tipos de regras indica sua proximidade. Em ambos os casos são regras de > manipulação simbólica. Curiosa a sua leitura. Entendo, ao contrário, que a necessidade de marcar as sentenças ora como "true" e ora como "prop" mostra exatamente o contrário, a saber, a necessidade de _distinguir as regras subjacentes_, em cada caso, como envolvidas em duas atividades completamente diferentes. As "regras de formação" de qualquer conectivo binário (conjunção, disjunção, implicação etc) são as mesmas. São as "regras de inferência", por outro lado, que permitem compreender a diferença de _significado_ entre estes conectivos. Aliás, o uso do termo "consequência sintática" tem inclusive esta conotação negativa: a de dar a impressão de que estaríamos envolvidos em uma tarefa "puramente sintática", "puramente formal" (do ponto de vista linguístico), "sem significado". Quem é que gosta de se envolver em tarefas sem significado? > Inicialmente falei de conjunto infinito de premissas, depois fui alertado > pelo Rodrigo Freire que este caso pode se reduzir ao de fórmulas com > comprimento infinito. Me parece que os dois casos exprimem o mesmo problema: > mesmo que S seja consequência lógica (ou semântica) de Gama, eu não diria > que S é consequência formal (ou sintática, ou dedutiva) de Gama se este fato > não puder ser efetivamente verificado ou estabelecido. Confesso que ainda não entendo bem a sua noção de "efetividade". Se por "efetivo" você quer dizer "recursivo", como é usual nos estudos de Computabilidade, vamos ter que concluir que a lógica clássica de primeira ordem não tem uma noção de consequência efetiva, e talvez você seja obrigado a conceder, dada a sua posição a respeito, que ela não se trata de um "sistema formal"... Alerto ainda para o fato de que há noções de demonstração perfeitamente adequadas inclusive para algumas lógicas não-monotônicas nas quais não há _teste positivo_ para derivabilidade (isto é, nas quais o conjunto de teoremas não é sequer recursivamente enumerável). Vide os trabalhos de Batens & cia sobre lógicas adaptativas. > Não estou propondo ressuscitar o Programa de Hilbert. Nem mesmo estou > propondo limitá-lo ao âmbito daquilo que temos o hábito de chamar de lógica > (embora eu seja simpático a esta ideia). Defendo apenas o ponto bastante > trivial de que ainda que possamos definir e utilizar com sucesso diversas > relações de consequência obtidas através dos mais variados recursos > matemáticos, aquilo que chamamos de sistema formal de lógica, capaz de > produzir provas ou demonstrações formais, deve basear-se em uma noção de > consequência efetiva, que comumente conhecemos como consequência sintática, > e que chamei aqui de consequência formal. Quero dizer com isso que qualquer > coisa que seja uma prova deve poder ser efetivamente obtida ou verificada, > nos moldes da teoria da recursão, do cálculo lambda, ou das máquinas de > Turing. No entanto, como você mesmo me alertou, há muitas lógicas/sistemas > para as quais as relações de consequência não são desta maneira limitadas. > Bem, então eu tiro três conclusões deste fato: (1) Não há provas formais > nestas lógicas/sistemas. Elas não são sistemas formais. É uma conclusão estranha... Não compreendo porque "formalidade" dependeria da existência de "provas formais" (entendidas como artefatos de estudo da Teoria das Demonstrações). Considere como exemplo o interessante e fundamental artigo de Hintikka, de 1957, sobre lógica deôntica quantificada. Não há um único "axioma" ou "regra de inferência" no artigo. Não haveria ali portanto um "sistemas formal"? > (2) Consequentemente, os teoremas da correção e completude não têm seu > significado usual, aqui, de assegurar que a demonstrabilidade é condição > necessária e suficiente para a validade. Seriam apenas, como você prefere, > resultados de adequação e caracterização. (3) A distinção entre consequência > sintática (ou formal) e consequência semântica (ou lógica) mantém-se > significativa, pois marca esta separação. E veja que esta separação não é > irrelevante, pois há toda uma tradição que trata a própria lógica como a > teoria das demonstrações. Pois parece que é justamente esta "tradição", a da Teoria das Demonstrações, a única na qual ainda se encontra a terminologia "consequência sintática" com alguma consistência... E o que me espanta é que é justamente nesta área que a terminologia é mais _contra-produtiva_, por permitir em particular a má identificação entre os estudos de sintaxe e os estudos de derivabilidade! Joao Marcos -- http://sequiturquodlibet.googlepages.com/ _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
