Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 1 of 1
Full-Text Articles in Logic and Foundations
Residuated Frames With Applications To Decidability, Nikolaos Galatos, Peter Jipsen
Residuated Frames With Applications To Decidability, Nikolaos Galatos, Peter Jipsen
Mathematics, Physics, and Computer Science Faculty Articles and Research
Residuated frames provide relational semantics for substructural logics and are a natural generalization of Kripke frames in intuitionistic and modal logic, and of phase spaces in linear logic. We explore the connection between Gentzen systems and residuated frames and illustrate how frames provide a uniform treatment for semantic proofs of cut-elimination, the finite model property and the finite embeddability property, which imply the decidability of the equational/universal theories of the associated residuated lattice-ordered groupoids. In particular these techniques allow us to prove that the variety of involutive FL-algebras and several related varieties have the finite model property.