A Kripke semantics for the logic of Gelfand quantales (Q5954708): Difference between revisions
From MaRDI portal
Created a new Item |
Added link to MaRDI item. |
||
links / mardi / name | links / mardi / name | ||
Revision as of 02:09, 30 January 2024
scientific article; zbMATH DE number 1701687
Language | Label | Description | Also known as |
---|---|---|---|
English | A Kripke semantics for the logic of Gelfand quantales |
scientific article; zbMATH DE number 1701687 |
Statements
A Kripke semantics for the logic of Gelfand quantales (English)
0 references
5 February 2002
0 references
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.
0 references
lattice representations
0 references
frames
0 references
Gelfand quantales
0 references
Gelfand logic
0 references
Kripke semantics
0 references
complete lattices
0 references
semantic tableau
0 references