Kripke Semantics for Intuitionistic Lukasiewicz Logic

This paper proposes a generalization of the Kripke semantics of intuitionistic logic IL appropriate for intuitionistic Lukasiewicz logicILL -a logic in the intersection between IL and (classical) Lukasiewicz logic. This generalised Kripke semantics is based on the poset sum construction, used in Bova and Montagna (Theoret Comput Sci 410(12):1143-1158, 2009). to show the decidability (and PSPACE completeness) of the quasiequational theory of commutative, integral and bounded GBL algebras. The main idea is that w & x22a9;psi-which for ILis a relation between worlds w and formulas psi, and can be seen as a function taking values in the booleans (w & x22a9;psi)is an element of B-becomes a function taking values in the unit interval (w & x22a9;psi)is an element of[0,1]. An appropriate monotonicity restriction (which we call sloping functions) needs to be put on such functions in order to ensure soundness and completeness of the semantics.