Olas! Eu nao vou ter tempo agora de escrever muito, mas acho que vale a pena dizer que me parece que a Sara Negri tem um "procedure" para gerar sistemas baseados em cálculo de sequentes para lógicas modais.
Abraco, Elaine. 2012/5/21 Valeria de Paiva <valeria.depa...@gmail.com>: > oi Joao Marcos, > com certeza, o estilo de deducao natural do Basin, Vigano e Matthews, que o > Luca explicou muito melhor no livro e' uma outra maneira de consertar os > formalismos dedutivos modais, da mesma forma que os sistemas do Simpson tb > o sao, pra logica modal intuicionista. > as logicas hibridas levam essa ideia ao seu desenvolvimento natural. > se voce vai etiquetar as formulas pra dizer onde elas sao validas, em vez > de colocar no sistema dedutivo simplesmente a relacao de acessibilidade do > modelo, pode colocar os mundos tambem e usa-los nas formulas como cidadaos > de primeira classe. > e isso te da', como bem disse o Mario, muito mais expressividade no > sistema. > a minha resposta pro Tony nao 'e discordando da do Mario, mas sim > explicando o que *eu* vejo de interessante... > > Como a gente ja conversou muitas vezes, eu tenho varios "problemas > emocionais" com todos os formalismos que fazem essa coisa de fazer a > semantica parte da sintaxe, pois eu acho que isso 'e meio > "cheating",filosoficamente. tb 'e dar uma primazia especial aas semanticas > de mundos possiveis que eu nao sei se elas teem), mas a gente quer usar > sistemas modais, a gente quer fazer contas/descobrir provas neles, e isso > certamente 'e uma solucao implementavel... > > vamos conversando e melhorando o nosso entendimento dos nossos sistemas, ne? > abs > Valeria > > On Mon, May 21, 2012 at 2:49 PM, Joao Marcos <botoc...@gmail.com> wrote: > >> Olá, Valeria: >> >> Acho que vale a pena recordar ainda que há uma outra maneira bastante >> simples de "consertar" os formalismos dedutivos modais, pelo acréscimo >> de etiquetas (representando termos de uma assinatura de primeira ordem >> adequada) sobre fórmulas modais e a adição de fórmulas relacionais à >> linguagem-objeto. Como resultado, regras de dedução natural >> extremamente simples para os principais sistemas modais podem ser >> definidas, tal como ilustradas no livro "Labelled Non-Classical >> Logics", de Luca Viganò --- ou no seguinte material nosso, em >> português: >> http://www.dimap.ufrn.br/~jmarcos/courses/LC/Cap4.pdf >> >> As lógicas híbridas, claro, vão muito além disso, sendo baseadas em >> linguagens legitimamente *mais expressivas* do ponto de vista das >> estruturas relacionais por elas caracterizadas, como Mário bem chamou >> a atenção em sua mensagem. >> >> Abraços, >> Joao Marcos >> >> >> On Sat, May 19, 2012 at 1:01 PM, Valeria de Paiva >> <valeria.depa...@gmail.com> wrote: >> > Tony, >> > as far as I'm concerned the real advantage of hybrid logics over >> multimodal >> > logics is on their proof theoretical aspects, hybrid logics are much >> better >> > behaved than modal logics as far as their proof theory goes. Patrick >> > Blackburn gave a course in nasslli2002 where he pressed this point and >> i've >> > spent an enjoyable half an hour trying to find the slides to send you, >> but >> > have not. the reader for the course is available >> > www.stanford.edu/group/nasslli/courses/*blackburn*/reader.pdf. >> > >> > in particular interpolation results are recovered: >> > (Repairing the Interpolation Theorem in Quantified Modal >> > Logic<http://www.loria.fr/%7Eblackbur/papers/repairing.pdf>, >> > by Carlos Areces, Patrick Blackburn and Maarten Marx. *Annals of Pure and >> > Applied Logic*, 124, 287-299, 2003. ) >> > >> > but for me the big payoff was on cut-elimination results for several >> > systems. >> > >> > Patrick's lectures were impressive enough to make me investigate >> > constructive versions of hybrid logics with Torben Brauner to begin with >> > and more recently with Herman Hauesler and Alexandre Rademaker. >> > >> > and yes, satisfaction operators do behave like modal operators. >> > >> > but no, it's not simply giving new names to old things, since using the >> > satisfaction operators and internalizing the models as part of your >> syntax >> > you genuinely get a different logic system, which has different >> inferential >> > properties and which you can implement and do more things with. >> > at least this is my take. >> > >> > []s, >> > Valeria >> >> -- >> http://sequiturquodlibet.googlepages.com/ >> > > > > -- > Valeria de Paiva > http://www.cs.bham.ac.uk/~vdp/ > http://valeriadepaiva.org/www/ > _______________________________________________ > Logica-l mailing list > Logica-l@dimap.ufrn.br > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l -- Elaine. -------------------------------------------------------- Elaine Pimentel Departamento de Matematicas Universidad del Valle Calle 13 No. 100 - 00 ; Edificio 320. Ciudadela Universitaria Melendez Cali, Colombia https://sites.google.com/site/elainepimentel/ -------------------------------------------------------- _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
