Hilbert calculi for the main fragments of Classical Logic

Abstract

A Lógica Clássica, sob a ótica da Álgebra Universal, pode ser vista como aquela induzida pelo clone completo sobre o conjunto {0,1}. Os demais clones sobre o mesmo conjunto induzem, portanto, sublógicas ou fragmentos da Lógica Clássica. Em 1941, Emil Post apresentou a organização de todos clones sobre {0,1} em um reticulado ordenado por inclusão [10]. Em [11], Wolfgang Rautenberg explorou esse reticulado para demonstrar que todos esses fragmentos são fortemente e finitamente axiomatizáveis. Rautenberg utilizou uma notação pouco usual e a sobrecarregou diversas vezes, gerando confusão, além de ter apresentado demonstrações incompletas e cometido vários erros tipográficos, imprecisões e desacertos. Em especial, os principais fragmentos da Lógica Clássica — expressão aqui utilizada para se referir àqueles dos quais tratam as demonstrações dos casos principais apresentadas por Rautenberg na primeira parte de seu artigo — merecem uma apresentação mais rigorosa e acessível, pois produzem importantes discussões e resultados sobre os demais clones, além de embasarem os procedimentos recursivos da segunda parte da demonstração do teorema da axiomatizabilidade de todos os clones bivalorados. Neste trabalho, propõe-se uma reapresentação das demonstrações para esses fragmentos, desta vez com uma notação mais moderna, com maior preocupação com os detalhes, com mais atenção à corretude da escrita e com a inclusão de todas as axiomatizações dos clones investigados. Além disso, os sistemas formais envolvidos serão especificados na linguagem do assistente de demonstração Lean, e as demonstrações de completude serão verificadas com a ajuda dessa ferramenta. Dessa forma, a demonstração do resultado apresentado por Rautenberg estará apresentada de forma mais acessível, compreensível e confiável para a comunidade.