bachelorThesis
Hilbert calculi for the main fragments of Classical Logic
Cálculos de Hilbert para os principais fragmentos da Lógica Clássica
Registro en:
20180153470
GREATI, 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.
Autor
Greati, Vitor Rodrigues
Resumen
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. Classical logic, under a universal-algebraic consequence-theoretic perspective, can be defined as the logic induced by the complete clone over {0,1}. Up to isomorphism, any
other 2-valued logic may then be seen as a sublogic or fragment of Classical Logic. In
1941, Emil Post studied the lattice of all the 2-valued clones ordered under inclusion [10].
In [11], Wolfgang Rautenberg explored this lattice in order to show that all fragments of
Classical Logic are strongly finitely axiomatizable. Rautenberg used an unusual notation
and overloaded it several times, causing confusion; in addition, he presented incomplete
proofs and made lots of typographical errors, imprecisions and mistakes. In particular,
the main fragments of Classical Logic — expression here that refers to those fragments
related to the proofs presented by Rautenberg in the first part of his paper — deserve a
more rigorous and accessible presentation, because they promote important discussions
and results about the remaining fragments. Also, they give bases to the recursive procedures in the second part of the proof of the axiomatizability of all 2-valued fragments.
This work proposes a rephrasing of the proofs for the main fragments, with a more modern notation, with more attention to the details and the writing, and with the inclusion
of all axiomatizations of the clones under investigation. In addition, the involved proof
systems will be specified in the language of the Lean theorem prover, and the derivations
necessary for the completeness proofs will be verified with the aid of this tool. In this way,
the presentation of the proof of the result given by Rautenberg will be more accessible,
understandable and trustworthy to the community.