Extração automática de cálculos de Hilbert associados aos fragmentos da lógica clássica
Uma lógica \(\mathcal{L}\) é bivalorada quando é caracterizável por uma matriz lógica \(\langle \{0,1\}, \{1\}, \cdot_2 \rangle\), onde \(\cdot_2\) denota interpretações dos conectivos da assinatura de \(\mathcal{L}\). A lógica clássica é qualquer lógica bivalorada cujo clone da álgebra de dois elementos associada possui todas as operações sobre o conjunto subjacente. Dessa forma, qualquer outra lógica bivalorada é uma sublógica – ou fragmento – da lógica clássica. Emil Post, matemático e lógico americano do século XX, apresentou, em 1941, uma descrição completa de todos os clones sobre o conjunto \(\{0,1\}\), na forma de um reticulado formado pelo conjunto dos referidos clones ordenado pela relação de inclusão. O reticulado de Post constitui uma fonte valiosa de informação sobre os fragmentos da lógica clássica, permitindo, por exemplo, extrair conclusões acerca dos efeitos da adição de determinados conectivos booleanos a certos fragmentos. Baseado na estrutura desse reticulado, Wolfgang Rautenberg, matemático alemão também do século XX, em artigo publicado em 1981, apresentou um procedimento para a extração de axiomatizações – ou cálculos de Hilbert – para matrizes bivaloradas, e, portanto, para fragmentos da lógica clássica induzidos por tais matrizes. Tal contribuição é especialmente útil para aplicações interessadas nas lógicas oriundas das combinações de fragmentos da lógica clássica, visto que os cálculos de Hilbert constituem um ambiente simples e propício para a criação de tais combinações e para os estudos dos sistemas complexos derivados a partir delas. Apesar disso, ainda não há uma implementação computacional desse procedimento. O trabalho sendo desenvolvido busca preencher essa lacuna, por intermédio da produção de um sistema computacional que receba como entrada a especificação semântica de um fragmento da lógica clássica, escrito por meio de uma interface amigável, e produza uma axiomatização correspondente segundo o método descrito por Rautenberg. Esta apresentação abordará detalhes e exemplos sobre os fragmentos da lógica clássica no contexto do reticulado de Post, além de explanar o que foi até então estudado quanto ao procedimento exposto por Rautenberg, elucidando a importância deste – e, consequentemente, a do presente trabalho – para a seara da combinação entre lógicas.