Marcos, JoãoGreati, Vitor Rodrigues2019-12-092021-09-202019-12-092021-09-202019-11-22GREATI, Vitor Rodrigues. Hilbert calculi for the main fragments of Classical Logic. 2019. 139 f. TCC (Graduação) - Curso de Ciência da Computação, Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2019.https://repositorio.ufrn.br/handle/123456789/34164A 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.Attribution-NonCommercial-NoDerivs 3.0 Brazilhttp://creativecommons.org/licenses/by-nc-nd/3.0/br/Fragments of Classical LogicHilbert calculiPost’s latticeUniversal Algebrareticulado de Postcálculos de HilbertbachelorThesis