Hola, Valéria e João. Bem, eu ia me abster de responder, mas resolvi fazer um comentário rápido.
Em primeiro lugar, eu nunca disse que a Sara inventou sistemas rotulados. O que eu disse foi que o cap 11 do livro de Proof Analysis é um bom lugar para ler sobre sistemas modais rotulados baseados em cálculo de sequentes. E sistemas baseados em dedução natural não são adequados para obter diversos resultados em teoria da prova, em especial aqueles que necessitam o conceito de focalização (pois só há focalização em sistemas que contenham apenas regras de introdução). Em tempo: o livro é muito ruim, de uma maneira geral. Salva-se apenas o cap 11, na minha opinião. Em segundo lugar, eu entendo (e concordo com) a maioria dos argumentos postos pela Valéria mas o que ocorre é que, na verdade, as regras "semânticas" de G3K podem ser vistas como pontos fixos em lógica linear com definições. De fato, os corpos das definições são cláusulas de Horn (portanto positivas) e focar sobre elas resulta em um passo de dedução. Ou seja, elas não interferem no restante da prova (lógica). Mas acho que nada disso interessa diretamente ao Daniel, que colocou a pergunta, em primeiro lugar. Abraços, 2013/5/27 Valeria de Paiva <valeria.depa...@gmail.com> > hmm, obrigada JM pela referencia elogiosa ao meu trabalho com o Torben > sobre Deducao Natural pra logica hibrida construtiva! > > mas e': > > (É 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.) > > a gente ja discutiu isso algumas vezes. hoje estou meio sem tempo pra > longas conversas, mas nao posso deixar passar em branco o argumento > usual... > > e', botar as relacoes de acessibilidade dos modelos de Kripke na sintaxe > da logica modal 'e um truque bacana que funciona muito bem pra muitas > coisas, mas > 1. isso da' aa nocao de modelo de mundos um papel especial, de definidor > dos sistemas modais, que eu nao sei se 'e razoavel. logicas modais existiam > antes dos modelos de mundos e podem existir sem os mesmos, a principio. a > principio semantica de mundos 'e que nem qq outra semantica (algebrica, > categorica, de valoracoes, etc...) se a semantica de mundos precisa ser > parte da definicao da *sintaxe* das logicas modais, bom entao > ontologicamente elas sao privilegiadas. Por que? > 2. botar a semantica desejada na sintaxe que voce quer modelar (apesar de > logicas hibridas) continua me parecendo roubalheira/cheating... a gente nao > precisa disso pra logica classica, a gente nao precisa disso pra logica > intuicionista, a gente nao precisa pra certos sistemas modais... a nocao de > corretude/soundness fica meio comprometida, pois se a semantica 'e parte da > sintaxe, corretude e' por definicao, nao por demonstracao...essas > discussoes (ou algumas delas) tb estao na tese do Simpson, junto com as > respostas dele de pq as minhas objecoes nao sao relevantes. > 3. quem quer fazer teoria da prova/ou da demonstracao nao pode transformar > as provas que estao interessados em, em provas de primeira ordem. porque > isso destroi a estrutura de demonstracoes que sao tao bem comportadas (como > os slides que o JM sugeriu explicaram) em coisas dentro do universo de 1a > ordem que nao sao bem comportadas de forma nenhuma. > 4. quem como eu e tantos outros esta' interessado nas provas e nao no fato > de um certo teorema ser verdadeiro ou falso, precisa ter muito cuidado com > as traducoes entre sistemas logicos que vai aceitar., pois muitas das > traducoes que preservam valor verdade destroem a estrutura das provas... > > bom, acho que ja chega, ja repetimos alguns dos argumentos tradicionais. > outros interessados em teoria da prova e (pra nao dzer que nao falei das > flores) em focussing ou hypersequentes podem tb dar seus palpites. > > Abracos logicos cordiais > Valeria > > 2013/5/27 Daniel Durante <dura...@ufrnet.br> > > > Colegas, > > > > Muito obrigado MESMO pelas referências, já comecei estudar, e elas > > certamente me pouparão muito TEMPO :) E também confirmam minha suspeita > de > > que o assunto era mesmo bem desenvolvido. Aproveito, então, e deixo a > vocês > > uma pergunta séria, mas que vou formular em termos lúdicos: suponha que > por > > alguma limitação qualquer (não muito longe do real, no meu caso), por > > exemplo não tenho lápis e papel, nem boa memória (para fazer as coisas de > > cabeça), nem internet,... e em meu computador só tenho instalado o > software > > "Fitch", que me deixa (e auxilia a) fazer provas em dedução natural na > > lógica clássica de primeira ordem. Bem, com esta ferramenta eu já sei que > > posso construir teorias (conjuntos de premissas) para as diversas versões > > da lógica temporal, descobri que posso fazer o mesmo para os principais > > sistemas de lógica modal, imagino (para o meu desgosto) que posso fazer o > > mesmo inclusive para a lógica intuicionista, já que há uma teoria > clássica > > para S4. Bem, então eu começo a pensar que poderia fazer o mesmo para > > lógicas paraconsistentes, relevantes,… A pergunta, então, é: tem alguma > > lógica não-clássica que eu não vou conseguir resolver no meu software, > > simulando-a como uma teoria de primeira ordem clássica? > > Parece que qualquer sistema formal que seja correto e completo com > > respeito a alguma formulação semântica que possa ser expressa em uma > teoria > > de relações passível de ser axiomatizada em primeira ordem se tornaria > > equivalente a uma teoria clássica de primeira ordem!!??!! Deve haver algo > > errado com esta ideia, pois ela me faz pensar se existe mesmo alguma > lógica > > não-clássica no sentido de não poder ser tratada classicamente, de ser > > incompatível com a lógica clássica! O que vocês acham (ou sabem) sobre o > > assunto? > > > > Saudações, > > Daniel > > > > PS: Sobre o que disse o João Marcos: > > > > > (É 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.) > > > > Eu tenho um palpite, João. A razão pode ser histórica. No caso das > lógicas > > modais, por exemplo, a regimentação em primeira ordem só se tornou > possível > > depois que a semântica dos modelos de Kripke se estabeleceu. É preciso > > muita reflexão para converter os conceitos de "necessidade" e > > "possibilidade", que traduzem-se diretamente em operadores lógicos, em > uma > > relação binária entre estados possíveis do mundo (ou mundos possíveis) > que > > rotulam proposições! Outra esquisitice histórica da lógica modal é o nome > > dos sistemas! K, T, B, S4, S4.3, S5? > > _______________________________________________ > > Logica-l mailing list > > Logica-l@dimap.ufrn.br > > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > > > > > > -- > Valeria de Paiva > http://www.cs.bham.ac.uk/~vdp/ > http://valeriadepaiva.org/ > _______________________________________________ > Logica-l mailing list > Logica-l@dimap.ufrn.br > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > -- Elaine. ------------------------------------------------- Elaine Pimentel - DMat/UFMG Address: Departamento de Matematica Universidade Federal de Minas Gerais Av Antonio Carlos, 6627 - C.P. 702 Pampulha - CEP 30.161-970 Belo Horizonte - Minas Gerais - Brazil Phone: 55 31 3409-5970/3409-5994 Fax: 55 31 3409-5692 htps://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
