A Gödel-style translation from positive calculus into strict implication logic
Jana Haenen
Abstract:
In this thesis, we develop a Gödel-style translation of a positive calculus, that is, a calculus that is equivalent to the positive fragment of classical propositional logic that is sound and complete with respect to bounded distributive lattices, into a suitable expansion of classical logic. In order to accomplish this, we build on a known correspondence between bounded distributive lattices and Boolean algebras with so-called lattice subordinations. We introduce a strict implication calculus that is sound and complete with respect to the class of Boolean algebras with a lattice subordination, which, as a consequence of the duality between the category of Boolean algebras with a lattice subordination and the category of quasi-ordered Priestley spaces, will also serve to reason about quasi-ordered Priestley spaces. For the positive calculus, we chose to work with a hypersequent framework, because it allows for nontrivial extensions of the calculus that correspond to proper subclasses of the class of bounded distributive lattices. We present a translation Tr(−) from the positive calculus to the strict implication calculus and show that it is full and faithful. We consider extensions of both calculi and show that every extension of the positive calculus is embedded via Tr(−) into some extension of strict implication calculus and vice versa, that for every extension of the strict implication calculus there exists a positive calculus that is embeddable in it via Tr(−).