Fixed-Point Elimination in the Intuitionistic Propositional Calculus
From MaRDI portal
Publication:2811336
Abstract: It is a consequence of existing 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. We give in this paper 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. We extract, out of the algorithm, upper bounds for such n, depending on the size of the formula. For some formulas, we show that these upper bounds are polynomial and optimal.
Recommendations
- Fixed-point elimination in the intuitionistic propositional calculus
- Intuitionistic fixed point logic
- Quantifier elimination for a class of intuitionistic theories
- A cut-elimination proof in intuitionistic predicate logic
- Quantifier Elimination and Provers Integration
- scientific article; zbMATH DE number 3976993
- Bounds for cut elimination in intuitionistic propositional logic
- scientific article; zbMATH DE number 48659
- Typed Lambda Calculi and Applications
- Fixed-point logics and computation
Cites work
- scientific article; zbMATH DE number 2172008 (Why is no real title available?)
- Computable fixpoints in well-structured symbolic model checking
- Convergence of positive schemes in S4 and Int
- Deciding the first levels of the modal \(\mu\) alternation hierarchy by formula construction
- Fixed-point theory in the varieties \(\mathcal{D}_{n}\)
- Least fixed points in Grzegorczyk's logic and in the intuitionistic propositional logic
- Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
- Model completions and r-Heyting categories
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- On modal \(\mu \)-calculus and Gödel-Löb logic
- On the Bourbaki-Witt principle in toposes
- On the \(\mu \)-calculus over transitive and finite transitive frames
- On the period of sequences (An(p)) in intuitionistic propositional calculus
- Processes, Terms and Cycles: Steps on the Road to Infinity
- Results on the propositional \(\mu\)-calculus
- Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
- Some Notes on Proofs with Alpha Graphs
- Strong categorical datatypes II: A term logic for categorical programming
- Strong functors and interleaving fixpoints in game semantics
- Strong functors and monoidal monads
- The modal \(\mu \)-calculus hierarchy over restricted classes of transition systems
Cited in
(9)- Free Heyting algebra endomorphisms: Ruitenburg’s Theorem and beyond
- Least and greatest fixed points in intuitionistic natural deduction
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- On the period of sequences (An(p)) in intuitionistic propositional calculus
- Intuitionistic fixed point theories over Heyting arithmetic
- Ruitenburg's theorem via duality and bounded bisimulations
- A Function Elimination Method for Checking Satisfiability of Arithmetical Logics
- Fixed-point elimination in the intuitionistic propositional calculus
- Intuitionistic fixed point logic
This page was built for publication: Fixed-Point Elimination in the Intuitionistic Propositional Calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2811336)
