Olá, Daniel: Acho que você levanta abaixo uma questão interessante e suficientemente diferente do problema original que eu vinha discutindo, e se justificaria por isso a abertura de uma nova linha de mensagens para discuti-la.
Confesso que não estou bem seguro (já estive mais seguro no passado, mas todas as minhas propostas ingênuas neste sentido se esfumaçaram ao longo dos anos) de onde passaria a (muitas vezes tênue) linha que separa "demonstrabilidade" de "verdade", como você colocou, e creio que seria interessante ouvir o que os colegas têm a dizer a respeito disso. > a distinção entre demonstrabilidade (pelo lado formal) > e verdade (pelo lado semântico) que os > famosos teoremas da correção e completude/incompletude nos mostram. Entendo que teoremas de adequação/caracterização (correção+completude) são necessários toda vez que precisamos verificar como duas noções de consequência estariam relacionadas. Assim, podemos falar em caracterização de uma noção de consequência originalmente associada a um sistema de dedução natural usando em um segundo estágio uma noção de consequência associada a um outro sistema formal dedutivo (a partir de sequentes, por exemplo), ou usando neste novo estágio uma noção de consequência associada a uma dada semântica. Podemos também falar na caracterização de uma noção de consequência semântica usando agora uma nova noção de consequência semântica, definida de forma completamente diferente. E assim por diante. Desta forma, para saber "o que os teoremas de correção+completude nos mostram" eu preciso antes de mais nada saber quais são as noções de consequência que estão envolvidas. Se eu soubesse bem onde acaba o estudo da "demonstrabilidade" e começa o estudo da "verdade", como você disse, eu provavelmente entenderia o que você quer dizer ao invocar os "famosos teoremas". Mas em geral eu não sei. > Mas minha questão é sobre qual a relevância desta distinção! Penso na lógica > como uma disciplina proposicional, que lida com proposições, e que as > proposições, independentemente do tipo de entidade que sejam, são passíveis > de expressão linguística (ou simbólica) através de sentenças governadas por > regras sintático-gramaticais (ou de manipulação simbólica). Todos os > sistemas formais de que tenho notícia são propostos com base nesta > representação linguístico-simbólica e é ela que operacionaliza todas as > regras de boa formação e de inferência, sendo portanto fundamento da noção > de consequência formal. 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. > Se é assim, então a noção de consequência formal > está limitada às consequências que conseguimos efetivamente produzir ou > verificar, pois dependem de nossa capacidade de manipulação simbólica. A > consequência formal seria a consequência lógica restrita às nossas > limitações humanas de verificabilidade. Tais restrições (relativas à > verificabilidade efetiva) não precisam ser levadas em consideração na noção > de consequência semântica, e este é, a meu ver, o fundamento e a importância > da distinção entre consequência formal (outrora chamada de sintática :) ) e > consequência semântica. Bom, talvez então nós "tenhamos notícia" de coisas bem diferentes. :-) 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). > Foi pensando nesta limitação que sugeri o exemplo da > quantidade infinita de premissas, que inviabilizaria a consequência formal, > mas não interferiria na consequência semântica. Bom, há aparentemente sistemas de "consequência formal" que incluem regras infinitárias... Há especialistas no assunto, nesta lista. Abraços, Joao Marcos -- http://sequiturquodlibet.googlepages.com/ _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
