Vitor Greati

From a universal-algebraic consequence-theoretic perspective, classical logic can be defined as the logic induced by the complete clone over \(\{0,1\}\). Up to isomorphism, any other \mbox{2-valued logic} may then be seen as a sublogic / fragment of classical logic. In spite of the theoretical straightforwardness of such a presentation, one may argue that 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, (sets of finitary operations closed under projection and composition) 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. Thus, for each finite collection of 2-valued operations given as input, the only challenge concerning the implementation of Rautenberg’s algorithm in a computational system would be to find the exact clone that it describes within Post’s lattice. By an application of Kleene’s Fixed-Point Theorem, any finite set of boolean functions may be closed under projection and finitary multiple composition in finite time, in a bottom-up fashion; as the thereby produced boolean clone must live in the corresponding lattice, by a clever top-down analysis of the latter one may then find its precise location. We have implemented both the latter tasks using the Haskell programming language and distributed the resulting system as a RESTful web service endpoint and as a web application to be freely used by the community. With that, the first step towards the automated extraction of a Hilbert calculus for any fragment of classical logic was made fully operational; the remainder of the work is to be based on Rautenberg’s axiomatization procedure.