Muito obrigado, João Marcos! Me é um grande alívio saber que aquilo de que desconfiava está certo: a prova condicional (que pressupõe o metateorema da dedução) não vale de modo irrestrito em tais sistemas modais. De fato, a literatura em questão não aponta a diferença entre os níveis global e local de consequência. Tens algum paper para indicar sobre esse assunto em especial?
2013/1/3 Joao Marcos <[email protected]> > Olá, Luis: > > 2013/1/3 Luis Rosa <[email protected]>: > > Porém, dado *N* e a regra de derivação que > > chamamos de 'prova condicional', *p *É *Lp *é um teorema de K > > Não, *p *É *Lp * NÃO é um teorema de K. A razão é simples: a sua > 'prova condicional', que pressuporia a validade do metateorema da > dedução, NÃO vale de forma irrestrita nestes sistemas modais. (Na sua > demonstração usual por indução sobre as derivações, o metateorema da > dedução sobrevive à regra de modus ponens, mas não à regra da > necessitação.) > > Observe que a regra *N*: > *⊢* *α* → *⊢* *L**α* > é uma espécie de regra _global_, que diz que *L**α* é um teorema > (fórmula demonstrada a partir de um conjunto vazio de premissas) > sempre que *α* for um teorema. Esta regra não vale na forma _local_ > que segue: > *α* *⊢* *L**α* > > Em contraste, a regra de modus ponens é em um certo sentido _mais > forte_, pois vale não apenas _globalmente_, na forma: > (*⊢* *α1* e *⊢* *α1**É**α2*) → *⊢* *α2* > mas também _localmente_, na forma: > A, *α1*, *α1**É**α2* *⊢* *α2* > onde A é um conjunto arbitrário de fórmulas. > > Um GRANDE e persistente problema da literatura modal 'standard' é > justamente o de não deixar bem clara a diferença entre os níveis local > e global de consequência, e não dar muita atenção à _incompletude > estrutural_ típica das lógicas modais. Pior, a fixação > 'filosófica'/'algébrica' em sistemas hilbertianos/axiomáticos costuma > dificultar justamente a compreensão da diferença entre axiomas e > regras, e da diferença entre teoremas e a noção mais geral de > consequência. > > * * * > > Um parêntese. Regras de inferência de uma lógica L1 de ordem n podem > frequentemente ser expressas como axiomas de uma lógica L2 de ordem m, > com m>n, quando esta última é usada como linguagem de especificação da > primeira. Um axioma lógico de L1 pode assim ser entendido como um > átomo (estruturado) de L2, e uma regra de inferência lógica de L1 pode > ser entendida como um axioma de L2. (A _implementação_ de uma > lógica-objeto, digamos, de primeira ordem, através de um framework > lógico de ordem superior (como *Isabelle*, por exemplo) faz uso > exatamente desta estratégia.) > > Joao Marcos > > -- > http://sequiturquodlibet.googlepages.com/ > -- *Luis Rosa * @fsopho // prof <https://sites.google.com/site/fsopho/> // lattes <http://lattes.cnpq.br/9235142514779816> FsOpHo Epistemology Blog <http://fsopho.wordpress.com/> Blog Distropia <http://distropia.wordpress.com/> Greek van Peixe - Gamer Rock <http://greekvanpeixe.com/> _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
