It follows from known results in the literature that least and greatest fixed-points of monotone polynomials on Heyting algebras-that is, the algebraic models of the Intuitionistic Propositional Calculus-always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC. Consequently, the μ-calculus based on intuitionistic logic is trivial, every μ-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 μ-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's 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 μ-calculus based on propositional intuitionistic logic. The second part of the article dealswith closure ordinals of monotone polynomials onHeyting 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.

Fixed-point Elimination in the Intuitionistic Propositional Calculus / S. Ghilardi, M.J. Gouveia, L. Santocanale. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 21:1(2019 Oct), pp. 4.1-4.37.

Fixed-point Elimination in the Intuitionistic Propositional Calculus

S. Ghilardi
Primo
;
2019-10

Abstract

It follows from known results in the literature that least and greatest fixed-points of monotone polynomials on Heyting algebras-that is, the algebraic models of the Intuitionistic Propositional Calculus-always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC. Consequently, the μ-calculus based on intuitionistic logic is trivial, every μ-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 μ-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's 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 μ-calculus based on propositional intuitionistic logic. The second part of the article dealswith closure ordinals of monotone polynomials onHeyting 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.
elimination; fixed-points; intuitionistic propositional calculus;
Settore MAT/01 - Logica Matematica
set-2019
Article (author)
File in questo prodotto:
File Dimensione Formato  
TOCL-19.pdf

accesso aperto

Tipologia: Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione 857.11 kB
Formato Adobe PDF
857.11 kB Adobe PDF Visualizza/Apri
a4-ghilardi.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 535.67 kB
Formato Adobe PDF
535.67 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/680151
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact