Extração automática de cálculos de Hilbert associados aos fragmentos da lógica clássica

Abstract

The classical logic 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 / fragment of classical logic. There is still very little common knowledge about the minimal combination of such fragments, which in principle may be obtained by simply merging the corresponding Hilbert calculi. In 1941, Emil Post studied the lattice of all the 2-valued clones, ordered under inclusion. This lattice ---countably infinite yet constituted of finitely generated members--- has constituted ever since an invaluable source of information and insights about the relationships among the sublogics of classical logic. Wolfgang Rautenberg explored Post's classification in proving that every 2-valued logic is strongly finitely axiomatizable; it is worth noting that this proof carries along an effective procedure for producing a Hilbert calculus to any fragment of classical logic. This work proposes to implement a Web system that is able to receive as input a set of 2-valued operations and return to the user the Hilbert Calculus associated. The implementation of the procedure to produce the Hilbert Calculus associated with the reported input will be done using the Haskell programming language and distributed as a RESTful API. In addition, a Website will be made, to be used freely by the community, which will receive the user inputs, consume the API, and inform the result of the cited procedure, based on the inputs that the user provided.