> Eu acho que vale a pena você dar uma olhada no livro Proof Analysis (Plato, > Negri), que tem um capítulo muito legal (11) sobre representação de lógicas > modais utilizando um sistema básico clássico (G3) e internalizando a > semântica através de regras modais, obtendo o sistema G3K.
Há um material em português muito bom sobre isso. :-) No capítulo 4 do livro http://www.dimap.ufrn.br/~jmarcos/courses/LC/Ementa.htm mostramos em detalhe pedestre como prover formalismos dedutivos (dedução natural) para boa parte dos sistemas modais mais comuns através do uso de rótulos (que representam mundos e são tratados como termos de uma linguagem de primeira ordem adequada) e de fórmulas relacionais (que representam, na mesma assinatura de primeira ordem já citada, a noção de acessibilidade). As propriedades que descrevem as restrições sobre as classes de enquadramentos são traduzidas de maneira óbvia em termos de regras dedutivas envolvendo as fórmulas relacionais da linguagem, eventualmente envolvendo funções de skolem (representadas por símbolos que também farão parte da sintaxe de primeira ordem escolhida). É bonito, simples e eficaz, acho que vale a pena conferir. Infelizmente não inventamos nada disso (e a Sara Negri também não, embora ela queira acreditar que sim)... A teoria da dedução rotulada/etiquetada para lógica modal foi estudada em detalhe por Luca Viganò e colaboradores. (É inteiramente misteriosa para mim a razão pela qual outros autores gastam tempo sobre sistemas dedutivos ad hoc para esta ou aquela lógica modal, dado que abordagens deste gênero são modulares e amplamente aplicáveis, além de fortemente adequadas do ponto de vista lógico.) Do ponto de vista modelo-teórico, as lógicas modais usuais são mapeadas via "standard translation" no fragmento diádico da lógica de primeira ordem --- mais especificamente no "guarded fragment", que possui propriedades de decidibilidade fantásticas. Há uns slides muito bacanas do Ramanujam sobre o assunto, fazendo um apanhado geral: http://fmindia.cmi.ac.in/update2008/slides/R._Ramanujam_jam.pdf O paper de Goranko & Otto no Handbook of Modal Logic também faz uma revisão interessante da teoria dos modelos modal. No caso construtivo, claro, a grande referência é a tese do Simpson. Para linguagens construtivas misturadas com lógica híbrida há o trabalho exemplar da Valeria com o Torben. Abraços, Joao Marcos > 2013/5/26 Daniel Durante <dura...@ufrnet.br> > >> Colegas, >> >> Tenho uma dúvida boba que certamente vocês podem me ajudar. Lendo algumas >> coisas básicas sobre lógica temporal, vi que uma maneira de tratar o >> assunto, que é inclusive expressivamente mais poderosa que a maneira padrão >> com operadores modais (temporais) é, no lugar disso, regimentar o discurso >> temporal em uma teoria de primeira ordem clássica. Ou seja, ao invés de >> operadores modais temporais, com regras de dedução e/ou axiomas próprios, >> teríamos simplesmente uma teoria de primeira ordem clássica que tem >> instantes de tempo (ou estados temporais "do mundo") como objetos (ou valor >> de suas variáveis) e a ordem temporal como a relação cujas propriedades os >> axiomas da teoria descrevem. >> Apesar desta abordagem ser mais ou menos comum para a lógica temporal, em >> uma rápida pesquisa eu não encontrei muita coisa sobre a regimentação das >> lógicas modais em geral em teorias clássicas de primeira ordem, que teriam >> estados possíveis do mundo como objetos e a acessibilidade como relação >> axiomatizada. Vi algo sobre S5 e a lógica de predicados monádicos, mas nada >> mais. >> Bem, minha pergunta é por referências mesmo, que certamente deve haver. >> Alguém poderia me indicar algumas referências sobre o assunto? >> >> Saudações, >> Daniel. -- http://sequiturquodlibet.googlepages.com/ _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
