Ruitenburg定理的机械化与语境化 (Ruitenburg's Theorem Mechanized and Contextualized)

from arxiv, In Proceedings FICS 2024, arXiv:2511.00626. The results were obtained while the author was employed at FAU Erlangen-Nuremberg. In the final stages of preparing the print version, the author has been employed at University of Naples Federico II, supported by the PNRR MUR projects FAIR (No. PE0000013-FAIR)

In 1984, Wim Ruitenburg published a surprising result about periodic sequences in intuitionistic propositional calculus (IPC). The property established by Ruitenburg naturally generalizes local finiteness; recall that intuitionistic logic is not locally finite, even in a single variable. One of the two main goals of this note is to illustrate that most "natural" non-classical logics failing local finiteness also do not enjoy the periodic sequence property. IPC is quite unique in separating these properties. The other goal of this note is to present a Coq formalization of Ruitenburg's heavily syntactic proof. Apart from ensuring its correctness, the formalization allows extraction of a program providing a certified implementation of Ruitenburg's algorithm.

翻译：1984年，Wim Ruitenburg发表了关于直觉主义命题演算（IPC）中周期序列的惊人结果。Ruitenburg所建立的这一性质自然地推广了局部有限性；需知直觉主义逻辑即使在单变量情形下也不具有局部有限性。本文的两个主要目标之一是阐明：大多数不具备局部有限性的“自然”非经典逻辑同样不满足周期序列性质。IPC在区分这些性质方面具有独特性。本文的另一目标是展示Ruitenburg高度语法化证明的Coq形式化。该形式化不仅确保了证明的正确性，还能提取出可提供Ruitenburg算法认证实现的可执行程序。