DEDUÇÃO NATURAL ROTULADA PARA LÓGICAS
MODAIS E MULTIMODAIS
Dedução Natural é um sistema de
prova desenvolvido independentemente por Gentzen e Jaśkowski.
Caracteriza-se por conter diversas regras de inferência, em geral
duas para cada operador (uma para introduzi-lo e outra para
eliminá-lo) em contraste com a presença de pouquíssimos ou nenhum
axioma; além do mais, caracteriza-se por conter regras de inferência
hipotéticas. Assim, o sistema de Dedução Natural passou a ser
reconhecido como o que mais se aproxima da forma como se raciocina em
matemática.
Contudo, a despeito deste sistema de
prova ser aplicado com sucesso a diversos sistemas de lógica (ex:
clássica, intuicionista, minimal, algumas lógicas relevantes,
alguns poucos sistemas modais etc), tem-se encontrado diversas
dificuldades para aplicá-lo em diversos outros sistemas.
Recentemente estas dificuldades vem sendo contornadas por autores
como Simpson e Gabbay, com a adoção de sistemas de provas
rotulados. Rótulos (ou etiquetas) são marcações atribuídas às
formulas em um sistema de provas, geralmente expressando propriedades
semânticas dessas.
Neste seminário, mostrarei como a
dedução natural rotulada funciona para diversos sistemas de lógica
modal e multimodal, discutirei o que ainda há para ser estudado na
área e como esse sistema pode ser utilizado para formalizar
raciocínios e argumentos envolvendo termos modais.
Nenhum comentário:
Postar um comentário