Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
alo, a tese do Simpson, que 'e um primor de bem-escrita, esta' ficando um pouquinho 'outdated'. esta' disponivel em http://homepages.inf.ed.ac.uk/als/Research/*thesis*.pdf meu paper com o Torben tb esta' disponivel (em tres versoes,conferencia, TR e revista): - *Towards Constructive Hybrid Logic (Extended Abstract) http://www.cs.bham.ac.uk/%7Evdp/publications/shortIHLfinal.ps* (with T. Brauner), Presented at Methods for Modalities 3, LORIA, Nancy, France, September 22-23, 2003. Also appears as a technical reporthttp://www.cs.bham.ac.uk/%7Evdp/publications/IntuitionisticHybrid.pdffrom the University of Roskilde, 2003. - Full paper from above, submitted with new title Intuitionistic Hybrid Logichttp://www.cs.bham.ac.uk/%7Evdp/publications/IntuitionisticHybrid.pdfto Journal of Applied Logic(JAL). Appeared as JAL 4(2006), 231-- 255, available online from the publishers on 11th August 2005. Valeria 2013/5/28 Daniel Durante dura...@ufrnet.br Colegas, Em primeiro lugar, há disponibilidade, online, para acessar a citada tese do Simpson e o artigo da Valeria e Torben? Sobre o que disse a Valéria, eu tenho alguns comentários: 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? EU concordo com você, mas muita gente não. Uma semântica correta e completa para um sistema formal equivale ao sistema formal. Se, além disso, esta semântica pode ser empacotada como teoria de um OUTRO sistema formal, então este outro sistema formal é, por transitividade, forte o suficiente para abarcar o primeiro. Se, ainda mais, este outro sistema formal for a lógica clássica, e se o seu fragmento utilizado para teorizar a semântica do primeiro sistema tiver propriedades já bem estudadas, temos bons motivos para preferir a teoria clássica. 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... A gente não precisa, mas a gente pode. E funciona! Suponha que eu seja um monista lógico, que só aceita a lógica clássica de primeira ordem, que acredita que o mundo é racional e a racionalidade do mundo é captada à perfeição pela lógica clássica. Fora da nossa especialidade acadêmica, esta me parece uma posição bastante aceita. Bem, mas mesmo neste caso, se eu utilizar este recurso de sintaxizar a semântica, eu não preciso me privar da maioria das lógicas não clássicas. Elas serão para mim teorias da única e verdadeira lógica. Um ponto filosófico interessante é que lógicas são tidas como PURA FORMA, enquanto que teorias são SOBRE ALGO. Mas que algo é esse do qual essas teorias tratam? As semânticas nos aproximam muito mais deste (misterioso) algo do que os sistemas formais. Sintaxizar a semântica ajuda a mostrar que a semântica da lógica não-clássica em questão é compatível e expressável na semântica da lógica clássica. Ou seja, ela não é tão não-clássica assim! 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… Nestes pontos eu concordo plenamente. Se o interesse são as provas, então o que importa é a sintaxe (em sentido amplo, viu João Marcos :) ). Sobre o que disse a Elaine: Mas acho que nada disso interessa diretamente ao Daniel, que colocou a pergunta, em primeiro lugar. Bem, saber que o livro Negri-Plato é muito ruim, e que só o capítulo 11 vale a pena, me interessa MUITO. São mais de 400 páginas :) Sobre o que disseram Marcelo e João Marcos: 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? Bom, pra não ser simulável em primeira ordem, que é turing
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
Oi Valéria, Muito obrigado pelos links! Minha pilha de leitura está aumentando! Daniel. PS: se alguém tentou e não conseguiu baixar a tese do Simpson, basta apagar os * da palavra thesis. O link abaixo funciona: http://homepages.inf.ed.ac.uk/als/Research/thesis.pdf +++ Em 28/05/2013, às 13:59, Valeria de Paiva valeria.depa...@gmail.com escreveu: alo, a tese do Simpson, que 'e um primor de bem-escrita, esta' ficando um pouquinho 'outdated'. esta' disponivel em http://homepages.inf.ed.ac.uk/als/Research/thesis.pdf meu paper com o Torben tb esta' disponivel (em tres versoes,conferencia, TR e revista): • Towards Constructive Hybrid Logic (Extended Abstract) (with T. Brauner), Presented at Methods for Modalities 3, LORIA, Nancy, France, September 22-23, 2003. Also appears as a technical report from the University of Roskilde, 2003. • Full paper from above, submitted with new title Intuitionistic Hybrid Logic to Journal of Applied Logic(JAL). Appeared as JAL 4(2006), 231-- 255, available online from the publishers on 11th August 2005. Valeria 2013/5/28 Daniel Durante dura...@ufrnet.br Colegas, Em primeiro lugar, há disponibilidade, online, para acessar a citada tese do Simpson e o artigo da Valeria e Torben? Sobre o que disse a Valéria, eu tenho alguns comentários: 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? EU concordo com você, mas muita gente não. Uma semântica correta e completa para um sistema formal equivale ao sistema formal. Se, além disso, esta semântica pode ser empacotada como teoria de um OUTRO sistema formal, então este outro sistema formal é, por transitividade, forte o suficiente para abarcar o primeiro. Se, ainda mais, este outro sistema formal for a lógica clássica, e se o seu fragmento utilizado para teorizar a semântica do primeiro sistema tiver propriedades já bem estudadas, temos bons motivos para preferir a teoria clássica. 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... A gente não precisa, mas a gente pode. E funciona! Suponha que eu seja um monista lógico, que só aceita a lógica clássica de primeira ordem, que acredita que o mundo é racional e a racionalidade do mundo é captada à perfeição pela lógica clássica. Fora da nossa especialidade acadêmica, esta me parece uma posição bastante aceita. Bem, mas mesmo neste caso, se eu utilizar este recurso de sintaxizar a semântica, eu não preciso me privar da maioria das lógicas não clássicas. Elas serão para mim teorias da única e verdadeira lógica. Um ponto filosófico interessante é que lógicas são tidas como PURA FORMA, enquanto que teorias são SOBRE ALGO. Mas que algo é esse do qual essas teorias tratam? As semânticas nos aproximam muito mais deste (misterioso) algo do que os sistemas formais. Sintaxizar a semântica ajuda a mostrar que a semântica da lógica não-clássica em questão é compatível e expressável na semântica da lógica clássica. Ou seja, ela não é tão não-clássica assim! 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… Nestes pontos eu concordo plenamente. Se o interesse são as provas, então o que importa é a sintaxe (em sentido amplo, viu João Marcos :) ). Sobre o que disse a Elaine: Mas acho que nada disso interessa diretamente ao Daniel, que colocou a pergunta, em primeiro lugar. Bem, saber que o livro Negri-Plato é muito ruim, e que só o capítulo 11 vale a pena, me interessa MUITO. São mais de 400 páginas :) Sobre o que disseram Marcelo
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
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
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
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
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
Oi Daniel. Em relação à sua pergunta: 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? Bom, pra não ser simulável em primeira ordem, que é turing completa, a lógica teria de mais indecidível que a lógica de primeira ordem. Agora, se a v quiser simulação em tempo polinomial, a coisa já fica mais interessante. Tem muita lógica que é duplamente exponencial, ou não elementar, e essas, certamente, v não consegue simular. Tente, por exemplo, simular um produto de duas lógicas intuicionistas e v se estrepa completamente. []s Marcelo 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 -- Marcelo Finger Department of Computer Science, Cornell University on leave from: Departament of Computer Science, IME University of Sao Paulo http://www.ime.usp.br/~mfinger ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
Oi Daniel, Não sei entendi sua pergunta. Mas em Lógicas temporais o uso de operadores que são definidos usando-se fecho transitivo ou ponto fixo é bem comum, por exemplo o Until. Voce não irá conseguir expressá-los no sistema Fitch. Um abraço, Mario Em 27 de maio de 2013 15:42, Marcelo Finger mfin...@ime.usp.br escreveu: Oi Daniel. Em relação à sua pergunta: 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? Bom, pra não ser simulável em primeira ordem, que é turing completa, a lógica teria de mais indecidível que a lógica de primeira ordem. Agora, se a v quiser simulação em tempo polinomial, a coisa já fica mais interessante. Tem muita lógica que é duplamente exponencial, ou não elementar, e essas, certamente, v não consegue simular. Tente, por exemplo, simular um produto de duas lógicas intuicionistas e v se estrepa completamente. []s Marcelo 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 -- Marcelo Finger Department of Computer Science, Cornell University on leave from: Departament of Computer Science, IME University of Sao Paulo http://www.ime.usp.br/~mfinger ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l -- Federal University of Rio de Janeiro www.cos.ufrj.br/~mario ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
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
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
2013/5/27 Elaine Pimentel escreveu: Em primeiro lugar, eu nunca disse que a Sara inventou sistemas rotulados. Ei, eu não disse que você disse. :-) Mas não pude perder a chance de espicaçar a Sara, que é uma pessoa de uma antipatia cristalina. O cúmulo para mim foi ela lá no UNILOG interromper o Sambin para dizer que ela tinha feito isso ou aquilo, e dentre as coisas que ela citou estava o trabalho do Luca --- que por acaso estava na plateia. A moça é mesmo de mais. 2013/5/27 Marcelo Finger escreveu: Em relação à sua pergunta: 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? Bom, pra não ser simulável em primeira ordem, que é turing completa, a lógica teria de mais indecidível que a lógica de primeira ordem. Se entre lógicas não-clássicas a gente conta as lógicas não-monotônicas então temos exemplos deste gênero: de fato, enquanto para a lógica clássica de primeira ordem temos um teste positivo para consequência mas não um teste negativo (o complemento da noção de derivabilidade não é recursivamente enumerável), para muitas lógicas não-monotônicas não há sequer um teste positivo. JM -- http://sequiturquodlibet.googlepages.com/ ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
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
