{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T14:27:11Z","timestamp":1762352831676,"version":"3.41.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,9,27]],"date-time":"2019-09-27T00:00:00Z","timestamp":1569542400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"LIA LYSM AMU CNRS ECM INdAM"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2020,1,31]]},"abstract":"<jats:p>\n            It follows from known results in the literature that least and greatest fixed-points of monotone polynomials on Heyting algebras\u2014that is, the algebraic models of the Intuitionistic Propositional Calculus\u2014always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the\n            <jats:bold>IPC<\/jats:bold>\n            . Consequently, the \u03bc-calculus based on intuitionistic logic is trivial, every \u03bc-formula being equivalent to a fixed-point free formula. In the first part of this article, we give an axiomatization of least and greatest fixed-points of formulas, and an algorithm to compute a fixed-point free formula equivalent to a given \u03bc-formula. The axiomatization of the greatest fixed-point is simple. The axiomatization of the least fixed-point is more complex, in particular every monotone formula converges to its least fixed-point by Kleene\u2019s iteration in a finite number of steps, but there is no uniform upper bound on the number of iterations. The axiomatization yields a decision procedure for the \u03bc-calculus based on propositional intuitionistic logic. The second part of the article deals with closure ordinals of monotone polynomials on Heyting algebras and of intuitionistic monotone formulas; these are the least numbers of iterations needed for a polynomial\/formula to converge to its least fixed-point. Mirroring the elimination procedure, we show how to compute upper bounds for closure ordinals of arbitrary intuitionistic formulas. For some classes of formulas, we provide tighter upper bounds that, in some cases, we prove exact.\n          <\/jats:p>","DOI":"10.1145\/3359669","type":"journal-article","created":{"date-parts":[[2019,9,27]],"date-time":"2019-09-27T12:33:44Z","timestamp":1569587624000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Fixed-point Elimination in the Intuitionistic Propositional Calculus"],"prefix":"10.1145","volume":"21","author":[{"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[{"name":"Dipartimento di Matematica, Universit\u00e0 degli Studi di Milano, Milan, Italy"}]},{"given":"Maria Jo\u00e3o","family":"Gouveia","sequence":"additional","affiliation":[{"name":"Faculdade de Ci\u00eancias da Universidade de Lisboa, Lisbon, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4237-7856","authenticated-orcid":false,"given":"Luigi","family":"Santocanale","sequence":"additional","affiliation":[{"name":"LIS, CNRS UMR 7020, Aix-Marseille Universit\u00e9, Marseilles, France"}]}],"member":"320","published-online":{"date-parts":[[2019,9,27]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"LIPIcs. Leibniz Int. Proc. Inform.","volume":"23","author":"Afshari Bahareh","unstructured":"Bahareh Afshari and Graham E. Leigh . 2013. On closure ordinals for the modal &mu;-calculus. In Computer Science Logic 2013 . LIPIcs. Leibniz Int. Proc. Inform. , Vol. 23 . Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 30--44. Bahareh Afshari and Graham E. Leigh. 2013. On closure ordinals for the modal &mu;-calculus. In Computer Science Logic 2013. LIPIcs. Leibniz Int. Proc. Inform., Vol. 23. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 30--44."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1254748696"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-009-9170-9"},{"volume-title":"Rudiments of &mu;-calculus: Studies in Logic and the Foundations of Mathematics","author":"Arnold Andr\u00e9","key":"e_1_2_1_4_1","unstructured":"Andr\u00e9 Arnold and Damian Niwi\u0144ski . 2001. Rudiments of &mu;-calculus: Studies in Logic and the Foundations of Mathematics , Vol. 146 . Elsevier . Andr\u00e9 Arnold and Damian Niwi\u0144ski. 2001. Rudiments of &mu;-calculus: Studies in Logic and the Foundations of Mathematics, Vol. 146. Elsevier."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0168-y"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01203370"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/170320"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2012028"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00099-5"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 7th Workshop on Fixed Points in Computer Science (FICS\u201910)","author":"Czarnecki Marek","year":"2010","unstructured":"Marek Czarnecki . 2010 . How fast can the fixpoints in modal &mu;-calculus be reached? In Proceedings of the 7th Workshop on Fixed Points in Computer Science (FICS\u201910) , L. Santocanale (Ed.). Brno, Czech Republic, 89. Retrieved from Hal : https:\/\/hal.archives-ouvertes.fr\/hal-00512377. Marek Czarnecki. 2010. How fast can the fixpoints in modal &mu;-calculus be reached? In Proceedings of the 7th Workshop on Fixed Points in Computer Science (FICS\u201910), L. Santocanale (Ed.). Brno, Czech Republic, 89. Retrieved from Hal: https:\/\/hal.archives-ouvertes.fr\/hal-00512377."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586539"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.002"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.2.255"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787181_13"},{"volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning, Christian G","author":"Ferrari Mauro","key":"e_1_2_1_16_1","unstructured":"Mauro Ferrari , Camillo Fiorentini , and Guido Fiorino . 2010. fCube: An efficient prover for intuitionistic propositional logic . In Logic for Programming, Artificial Intelligence, and Reasoning, Christian G . Ferm\u00fcller and Andrei Voronkov (Eds.). Springer , Berlin , 294--301. Mauro Ferrari, Camillo Fiorentini, and Guido Fiorino. 2010. fCube: An efficient prover for intuitionistic propositional logic. In Logic for Programming, Artificial Intelligence, and Reasoning, Christian G. Ferm\u00fcller and Andrei Voronkov (Eds.). Springer, Berlin, 294--301."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06251-8_27"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_1_19_1","volume-title":"Maria Jo\u00e3o Gouveia, and Luigi Santocanale","author":"Ghilardi Silvio","year":"2016","unstructured":"Silvio Ghilardi , Maria Jo\u00e3o Gouveia, and Luigi Santocanale . 2016 . Fixed-point elimination in the intuitionistic propositional calculus. In Foundations of Software Science and Computation Structures. Lecture Notes in Comput. Sci., Vol. 9634 . Springer , Berlin, 126--141. Silvio Ghilardi, Maria Jo\u00e3o Gouveia, and Luigi Santocanale. 2016. Fixed-point elimination in the intuitionistic propositional calculus. In Foundations of Software Science and Computation Structures. Lecture Notes in Comput. Sci., Vol. 9634. Springer, Berlin, 126--141."},{"key":"e_1_2_1_20_1","volume-title":"Advances in Modal Logic","volume":"12","author":"Ghilardi Silvio","year":"2018","unstructured":"Silvio Ghilardi and Luigi Santocanale . 2018 . Ruitenburg\u2019s theorem via duality and bounded bisimulations . In Advances in Modal Logic , Vol. 12 . College Publications, 277--290. Silvio Ghilardi and Luigi Santocanale. 2018. Ruitenburg\u2019s theorem via duality and bounded bisimulations. In Advances in Modal Logic, Vol. 12. College Publications, 277--290."},{"key":"e_1_2_1_21_1","unstructured":"Silvio Ghilardi and Luigi Santocanale. 2019. Free Heyting Algebra Endomorphisms: Ruitenburg\u2019s Theorem and Beyond. Retrieved from Hal: https:\/\/hal.archives-ouvertes.fr\/hal-01969235.  Silvio Ghilardi and Luigi Santocanale. 2019. Free Heyting Algebra Endomorphisms: Ruitenburg\u2019s Theorem and Beyond. Retrieved from Hal: https:\/\/hal.archives-ouvertes.fr\/hal-01969235."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(97)00012-2"},{"key":"e_1_2_1_23_1","volume-title":"A Categorical Approach to Nonclassical Propositional Logics","author":"Ghilardi Silvio","unstructured":"Silvio Ghilardi and Marek Zawadowski . 2002. Sheaves, Games, and Model Completions : A Categorical Approach to Nonclassical Propositional Logics ( 1 st ed.). Springer . Silvio Ghilardi and Marek Zawadowski. 2002. Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics (1st ed.). Springer.","edition":"1"},{"key":"e_1_2_1_24_1","volume-title":"LIPIcs. Leibniz Int. Proc. Inform.","volume":"82","author":"Gouveia Maria Jo\u00e3o","year":"2017","unstructured":"Maria Jo\u00e3o Gouveia and Luigi Santocanale . 2017 . &aleph;1 and the modal &mu;-calculus. In Computer Science Logic 2017 . LIPIcs. Leibniz Int. Proc. Inform. , Vol. 82 . Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, Art. No. 38, 16. Maria Jo\u00e3o Gouveia and Luigi Santocanale. 2017.&aleph;1 and the modal &mu;-calculus. In Computer Science Logic 2017. LIPIcs. Leibniz Int. Proc. Inform., Vol. 82. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, Art. No. 38, 16."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/557365"},{"volume-title":"Number 3 in Cambridge Studies in Advanced Mathematics","author":"Johnstone Peter","key":"e_1_2_1_26_1","unstructured":"Peter Johnstone . 1982. Stone Spaces . Number 3 in Cambridge Studies in Advanced Mathematics . Cambridge University Press . Peter Johnstone. 1982. Stone Spaces. Number 3 in Cambridge Studies in Advanced Mathematics. Cambridge University Press."},{"volume-title":"Basic Concepts of Enriched Category Theory. Number 64 in Lecture Notes in Mathematics","author":"Kelly G. Max","key":"e_1_2_1_27_1","unstructured":"G. Max Kelly . 1982. Basic Concepts of Enriched Category Theory. Number 64 in Lecture Notes in Mathematics . Cambridge University Press . G. Max Kelly. 1982. Basic Concepts of Enriched Category Theory. Number 64 in Lecture Notes in Mathematics. Cambridge University Press."},{"key":"e_1_2_1_28_1","volume-title":"Strong functors and monoidal monads. Archiv der Mathematik XXIII","author":"Kock Anders","year":"1972","unstructured":"Anders Kock . 1972. Strong functors and monoidal monads. Archiv der Mathematik XXIII ( 1972 ), 113--120. Anders Kock. 1972. Strong functors and monoidal monads. Archiv der Mathematik XXIII (1972), 113--120."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"volume-title":"Handbook of Modal Logic","author":"Kracht Marcus","key":"e_1_2_1_30_1","unstructured":"Marcus Kracht . 2006. Modal consequence relations . In Handbook of Modal Logic , Volume 3 (Studies in Logic and Practical Reasoning), Patrick Blackburn, Johan F. A. K. van Benthem, and Frank Wolter (Eds.). Elsevier Science , New York, NY, Chap. 8, 491--547. Marcus Kracht. 2006. Modal consequence relations. In Handbook of Modal Logic, Volume 3 (Studies in Logic and Practical Reasoning), Patrick Blackburn, Johan F. A. K. van Benthem, and Frank Wolter (Eds.). Elsevier Science, New York, NY, Chap. 8, 491--547."},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 24th EACSL Annual Conference on Computer Science Logic (CSL\u201915)","volume":"41","author":"Lehtinen Karoliina","year":"2015","unstructured":"Karoliina Lehtinen and Sandra Quickert . 2015 . Deciding the first levels of the modal mu alternation hierarchy by formula construction . In Proceedings of the 24th EACSL Annual Conference on Computer Science Logic (CSL\u201915) (LIPIcs), Stephan Kreutzer (Ed.) , Vol. 41 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 457--471. Karoliina Lehtinen and Sandra Quickert. 2015. Deciding the first levels of the modal mu alternation hierarchy by formula construction. In Proceedings of the 24th EACSL Annual Conference on Computer Science Logic (CSL\u201915) (LIPIcs), Stephan Kreutzer (Ed.), Vol. 41. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 457--471."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02261708"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00739995"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.17.317-346"},{"volume-title":"Structural Proof Theory","author":"Negri Sara","key":"e_1_2_1_35_1","unstructured":"Sara Negri and Jan von Plato . 2001. Structural Proof Theory . Cambridge University Press , Cambridge . Sara Negri and Jan von Plato. 2001. Structural Proof Theory. Cambridge University Press, Cambridge."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275175"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274142"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2002010"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3359669","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3359669","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:06Z","timestamp":1750202586000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3359669"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,27]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,1,31]]}},"alternative-id":["10.1145\/3359669"],"URL":"https:\/\/doi.org\/10.1145\/3359669","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2019,9,27]]},"assertion":[{"value":"2018-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}