Vitor Greati

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 a fragment of Classical Logic. In 1941, Emil Post studied the lattice of all the 2-valued clones ordered under inclusion. 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.