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