Prezado João Marcos, Eu não entendo o que vc quer dizer com:
> 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. Em particular, se o sistema formal está corretamente construído, porque vai dificultar qualquer compreensão? O que é essa "fixação" da que vc está falando. Eu tenho visto, sim, muitos usos "descuidados" do metateorema da dedução por matemáticos, desses que a gente pensa que não fez besteira porque teve sorte. E também vi alguns usos errados, como falei num outro e-mail. Mas, para mim, confundir um alicate com uma chave de fenda não é culpa do sistema formal nem do fabricante de ferramentas. Agradecerei o esclarecimento. Carlos 2013/1/3 Joao Marcos <botoc...@gmail.com>: > Olá, Luis: > > 2013/1/3 Luis Rosa <fso...@gmail.com>: >> 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 > Logica-l@dimap.ufrn.br > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
