Ruitenburg's Theorem Mechanized and Contextualized
arXiv:2402.01840 · doi:10.4204/EPTCS.435.4
Abstract
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.
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)