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 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.


Bem, neste caso o que temos é tão fraco que muita gente nem chamaria isso de 
lógica. Os lógicos-filósofos são muito mais conservadores neste ponto do que os 
lógicos-computeiros! Eu, como sou uma má mistura dos dois tipos, não sei.

Saudações,
Daniel
_______________________________________________
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Responder a