Fixed-point Elimination in the Intuitionistic Propositional Calculus
Fixed-point Elimination in the Intuitionistic Propositional Calculus
复制标题
直觉命题演算中的不动点消元法
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
L. Santocanale
中科院分区：
文献类型：
--
作者：
S. Ghilardi;M. J. Gouveia;L. Santocanale
它遵循从已知的结果在文献中，最小和最大的不动点的单调多项式的Heyting代数，即代数模型的直觉命题演算总是存在的，即使这些代数是不完整的格。原因是这些极值不动点可由IPC的公式定义。因此，基于直觉逻辑的μ演算是平凡的，每个μ公式等价于一个不动点自由公式。在本文的第一部分中，我们给出了公式的最小和最大不动点的公理化，以及计算与给定μ-公式等价的无不动点公式的算法。最大不动点的公理化是简单的。最小不动点的公理化比较复杂，特别是每个单调公式都通过Kleene迭代在有限步内收敛到它的最小不动点，但迭代次数没有统一的上界。公理化给出了基于命题直觉逻辑的μ演算的判定过程。文章的第二部分涉及封闭序数的单调多项式的Heyting代数和直觉单调公式;这些是最少的迭代次数所需的多项式/公式收敛到其最小不动点。模仿消除过程，我们展示了如何计算上界的任意直觉公式的闭包序数。对于某些类别的公式，我们提供更严格的上限，在某些情况下，我们证明准确。
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 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.