A Kripke semantics for the logic of Gelfand quantales (Q5954708)

The concept of a quantale was introduced by Mulvey in connection with his work in the foundations of constructive mechanics. Gelfand quantales are complete unital quantales with an involution, *, satisfying the property that for any element \(a\), if \(a\odot b\leq a\) for all \(b\), then \(a\odot a^*\odot a= a\). In this paper a Hilbert-style axiom system is given for a propositional logic, called Gelfand logic, which is sound and complete with respect to Gelfand quantales. A Kripke semantics is presented with respect to which the soundness and completeness of Gelfand logic is shown. The completeness theorem relies on a Stone-style representation theorem for complete lattices. A Rasiowa/Sikorski-style semantic tableau system is also presented, with the property that if all branches of a tableau are closed then the formula in question is a theorem of Gelfand logic. An open branch in a completed tableau guarantees the existence of a Kripke model in which the formula is not valid; hence it is not a theorem of Gelfand logic.