A Kripke semantics for the logic of Gelfand quantales

Studia Logica 68 (2):173-228 (2001)


Gelfand quantales are complete unital quantales with an involution, *, satisfying the property that for any element a, if a b a for all b, then a a* a = a. 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 for 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 tableaux guarantees the existence of an Kripke model in which the formula is not valid; hence it is not a theorem of Gelfand Logic

Download options


    Upload a copy of this work     Papers currently archived: 72,722

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

29 (#399,119)

6 months
1 (#388,319)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Logics Without the Contraction Rule.Hiroakira Ono & Yuichi Komori - 1985 - Journal of Symbolic Logic 50 (1):169-201.
The Theory of Representations for Boolean Algebras.M. H. Stone - 1936 - Journal of Symbolic Logic 1 (3):118-119.
Kripke Models for Linear Logic.Allwein Gerard & Dunn J. Michael - 1993 - Journal of Symbolic Logic 58 (2):514-545.
Relational Proof System for Relevant Logics.Ewa Orlowska - 1992 - Journal of Symbolic Logic 57 (4):1425-1440.

Add more references