Kripke Semantics for Intuitionistic Łukasiewicz Logic

This paper proposes a generalization of the Kripke semantics of intuitionistic logic IL appropriate for intuitionistic Łukasiewicz logic IŁL —a logic in the intersection between IL and (classical) Łukasiewicz 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 ⊩ψ —which for IL is a relation between worlds w and formulas ψ , and can be seen as a function taking values in the booleans (w ⊩ψ ) ∈𝔹 —becomes a function taking values in the unit interval (w ⊩ψ ) ∈ [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.