English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

It is a consequence of existing literature that least and greatestfixed-points of monotone polynomials on Heyting algebras-that is, the alge-braic models of the Intuitionistic Propositional Calculus-always exist, evenwhen these algebras are not complete as lattices. The reason is that theseextremal fixed-points are definable by formulas of the IPC. Consequently, the$\mu$-calculus based on intuitionistic logic is trivial, every $\mu$-formulabeing equiv- alent to a fixed-point free formula. We give in this paper anaxiomatization of least and greatest fixed-points of formulas, and an algorithmto compute a fixed-point free formula equivalent to a given $\mu$-formula. Theaxiomatization of the greatest fixed-point is simple. The axiomatization of theleast fixed- point is more complex, in particular every monotone formulaconverges to its least fixed-point by Kleene's iteration in a finite number ofsteps, but there is no uniform upper bound on the number of iterations. Weextract, out of the algorithm, upper bounds for such n, depending on the sizeof the formula. For some formulas, we show that these upper bounds arepolynomial and optimal.

Fixed-point elimination in the Intuitionistic Propositional Calculus (extended version)