Técnicas Nominais e aplicações em Lógica de primeira ordem

Abstract

Esta dissertação apresenta um estudo sobre as Técnicas Nominais, introduzidas por Murdoch J. Gabbay e Andrew M. Pitts, que consistem em uma gama de técnicas, baseadas no conceito de conjuntos nominais, que descrevem novas maneiras de apresentar a sintaxe de sistemas formais envolvendo operações de ligação variável. Uma de suas principais aplicações envolve a determinação de um modelo nominal abstrato para a Lógica clássica de primeira ordem com igualdade L1, alicerçado em uma generalização nominal dos conceitos da teoria de reticulados usual. Com este propósito em mente, iremos explorar os conceitos necessários referentes as técnicas nominais para, em seguida, utilizá-los para realizar uma extensão das noções básicas da teoria de reticulados, onde definiremos conjuntos nominais parcialmente ordenados, bem como estabeleceremos as noções de ínfimos e supremos, para então obtermos a noção de reticulados nominais. Estabeleceremos também noções de distributividade e complementação para reticulados nominais e relacionaremos isso com o conceito de σ-álgebra, o qual irá nos permitir não só incorporar a operação de substituição no nosso modelo, como também generalizar a noção de substituição. Todas essas definições irão culminar na definição de uma estrutura algébrica nominal chamada de álgebra L1 e será esta estrutura que usaremos para interpretar a lógica de primeira ordem L1 e provar a sua correção, noção esta que liga a sintaxe e a semântica da lógica L1. Mais precisamente, a correção afirma que se Φ ⊢ Ψ for um sequente derivável em L1, então a sua interpretação JΦ ⊢ ΨK sobre uma álgebra L1 é verdadeira.