A Kripke Semantics for the Logic of Gelfand Quantales

Authors: Allwein G.¹; MacCaull W.²

Source: Studia Logica, Volume 68, Number 2, July 2001 , pp. 173-228(56)

Publisher: Springer

Buy & download fulltext article:

Price: $47.00 plus tax (Refund Policy)

Abstract:

Gelfand quantales are complete unital quantales with an involution, *, satisfying the property that for any element a, if a odot b a for all b, then a odot a* odot 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.

Keywords: lattice representations; quantales; frames; Kripke semantics; semantic tableau

Language: English

Document Type: Regular paper

Affiliations: 1: Visual Inference Laboratory Indiana University Bloomington, IN 47405 USA gtall@cs.indiana.edu 2: Dept. Mathematics, Statistics and Computer Science St. Francis Xavier University PO Box 5000 Antigonish, NS B2G 2W5 Canada wmaccaul@stfx.ca

Publication date: 2001-07-01