Fixed-Point Elimination in the Intuitionistic Propositional Calculus

DOI10.1007/978-3-662-49630-5_8zbMATH Open1475.03069arXiv1601.00402OpenAlexW2976714240MaRDI QIDQ2811336FDOQ2811336

Authors: Silvio Ghilardi, Luigi Santocanale, Maria João Gouveia 

Publication date: 10 June 2016

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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 $mu$-calculus based on intuitionistic logic is trivial, every $mu$-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 $mu$-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.

Full work available at URL: https://arxiv.org/abs/1601.00402

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
• Typed Lambda Calculi and Applications
• Fixed-point logics and computation

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Heyting algebras (lattice-theoretic aspects) (06D20)

Cites Work

• Title not available (Why is that?)
• Results on the propositional \(\mu\)-calculus
• Computable fixpoints in well-structured symbolic model checking
• Strong functors and monoidal monads
• Fixed-Point Theory in the Varieties $\mathcal{D}_{n}$
• On an interpretation of second order quantification in first order intuitionistic propositional logic
• Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
• The modal \(\mu \)-calculus hierarchy over restricted classes of transition systems
• On the \(\mu \)-calculus over transitive and finite transitive frames
• On modal \(\mu \)-calculus and Gödel-Löb logic
• Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
• Strong categorical datatypes II: A term logic for categorical programming
• Model completions and r-Heyting categories
• Some Notes on Proofs with Alpha Graphs
• Processes, Terms and Cycles: Steps on the Road to Infinity
• Least fixed points in Grzegorczyk's logic and in the intuitionistic propositional logic
• On the period of sequences (Aⁿ(p)) in intuitionistic propositional calculus
• Convergence of positive schemes in S4 and Int
• Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction
• On the Bourbaki-Witt principle in toposes
• Strong functors and interleaving fixpoints in game semantics

Cited In (6)

• 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 (Aⁿ(p)) in intuitionistic propositional calculus
• Intuitionistic fixed point theories over Heyting arithmetic
• A Function Elimination Method for Checking Satisfiability of Arithmetical Logics

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)