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
