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 \Vdash \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 \Vdash \psi ) \in {{\mathbb {B}}}\)—becomes a function taking values in the unit interval \((w \Vdash \psi ) \in [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.


  1. 1.

    Bova, S., and F. Montagna, Proof search in Hájek’s Basic Logic. ACM Trans. Comput. Log. 9:21:1–21:26, 2008.

  2. 2.

    Bova, S., and F. Montagna, The consequence relation in the logic of commutative GBL-algebras is PSPACE-complete. Theoretical Computer Science 410(12):1143–1158, 2009.

    Article  Google Scholar 

  3. 3.

    Ciabattoni, A., On Urquhart’s C logic. In 30th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2000, Portland, Oregon, USA, May 23-25, 2000, Proceedings IEEE Computer Society, 2000, pp. 113–120.

  4. 4.

    Ciabattoni, A., and C. G. Fermüller, Hypersequents as a uniform framework for Urquhart’s C, MTL and related logics. In 31st IEEE International Symposium on Multiple-Valued Logic, ISMVL 2001, Warsaw, Poland, May 22-24, 2001, Proceedings IEEE Computer Society, 2001, pp. 227–232.

  5. 5.

    Cignoli, R., F. Esteva, L. Godo, and A. Torrens. Basic fuzzy logic is the logic of continuous t-norms and their residua. Soft Computing 4(2):106–112, 2000.

    Article  Google Scholar 

  6. 6.

    Hájek, P., Basic fuzzy logic and BL-algebras. Soft Computing 2(3):124–128, 1998.

    Article  Google Scholar 

  7. 7.

    Jipsen, P., and F. Montagna, On the structure of generalized BL-algebras. Algebra Universalis 55(2):227–238, 2006.

    Article  Google Scholar 

  8. 8.

    Kripke, S. A., Semantical analysis of intuitionistic logic I. In J.N. Crossley and M.A.E. Dummett, (eds.), Formal Systems and Recursive Functions, volume 40 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1965, pp. 92–130.

  9. 9.

    Kułacka, A., Tableau calculus for basic fuzzy logic BL. In A. Laurent, O. Strauss, A. Bouchon-Meunier, and R. R. Yager, (eds.), Information Processing and Management of Uncertainty in Knowledge-Based Systems. Springer International Publishing, Cham, 2014, pp. 325–334.

  10. 10.

    Kułacka, A., Propositional Fuzzy Logics: Tableaux and Strong Completeness. PhD thesis, Imperial College London, London, UK, 2017.

  11. 11.

    Kułacka, A., D. Pattinson, and L. Schröder, Syntactic labelled tableaux for Łukasiewicz fuzzy ALC. In IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, pp. 962–968.

  12. 12.

    Méndez, J. M., and F. Salto, Urquhart’s C with intuitionistic negation: Dummett’s LC without the contraction axiom. Notre Dame J. Formal Logic 36(3):407–413, 07 1995.

  13. 13.

    Negri, S., Proof analysis in modal logic. Journal of Philosophical Logic 34(5-6):507–544, 2005.

    Article  Google Scholar 

  14. 14.

    Negri, S., and J. von Plato, Proof Analysis: A Contribution to Hilbert’s Last Problem. Cambridge University Press, 2011.

  15. 15.

    Olivetti, N., Tableaux for Łukasiewicz infinite-valued logic. Studia Logica 73(1):81–111, 2003.

    Article  Google Scholar 

Download references


We would like to thank Rob Arthan for several interesting and useful discussions about Łukasiewicz logic and Kripke semantics, the anonymous referee various helpful comments and suggestions, and for pointing out that in an earlier version of this paper we were not careful enough in distinguishing our logic IŁL from the logic \({\mathbf{GBL}}_{\text {ewf}}\), and Reuben Rowe for a careful proofreading and several comments. Edmund Robinson acknowledges the support of UK EPRSC Research Grant EP/R006865/1: Interface Reasoning for Interacting Systems (IRIS).

Author information



Corresponding author

Correspondence to P. Oliva.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Presented by Daniele Mundici

Rights and permissions

Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Lewis-Smith, A., Oliva, P. & Robinson, E. Kripke Semantics for Intuitionistic Łukasiewicz Logic. Stud Logica 109, 313–339 (2021).

Download citation


  • Łukasiewicz logic
  • Intuitionistic Łukasiewicz logic
  • Kripke semantics
  • GBL algebras