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