Hilbert calculi for the main fragments of Classical Logic
Cálculos de Hilbert para os principais fragmentos da Lógica Clássica
| dc.contributor | Marcos, João | |
| dc.contributor | Rivieccio, Umberto | |
| dc.contributor | Pimentel, Elaine | |
| dc.creator | Greati, Vitor Rodrigues | |
| dc.date | 2019-12-09T17:30:26Z | |
| dc.date | 2021-09-20T11:46:08Z | |
| dc.date | 2019-12-09T17:30:26Z | |
| dc.date | 2021-09-20T11:46:08Z | |
| dc.date | 2019-11-22 | |
| dc.identifier | 20180153470 | |
| dc.identifier | 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. | |
| dc.identifier | https://repositorio.ufrn.br/handle/123456789/34164 | |
| dc.description | 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. | |
| dc.description | 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. | |
| dc.format | application/pdf | |
| dc.language | en | |
| dc.publisher | Universidade Federal do Rio Grande do Norte | |
| dc.publisher | Brasil | |
| dc.publisher | UFRN | |
| dc.publisher | Ciência da Computação | |
| dc.rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil | |
| dc.rights | http://creativecommons.org/licenses/by-nc-nd/3.0/br/ | |
| dc.rights | LOCKSS system has permission to collect, preserve, and serve this Archival Unit | |
| dc.subject | Fragments of Classical Logic | |
| dc.subject | Hilbert calculi | |
| dc.subject | Post’s lattice | |
| dc.subject | Universal Algebra | |
| dc.subject | reticulado de Post | |
| dc.subject | cálculos de Hilbert | |
| dc.title | Hilbert calculi for the main fragments of Classical Logic | |
| dc.title | Cálculos de Hilbert para os principais fragmentos da Lógica Clássica | |
| dc.type | bachelorThesis |