Ruitenburg's Theorem Mechanized and Contextualized
Tadeusz Litak
TL;DR
This work investigates the existence of periodic substitution sequences in logics beyond classical propositional logic, focusing on Wim Ruitenburg's result for intuitionistic propositional calculus ($\mathsf{IPC}$) and its unique status with respect to local finiteness. It presents a Coq mechanization of Ruitenburg's syntactic proof, together with a program-extraction pipeline that yields a certified implementation of Ruitenburg's algorithm, and analyzes two representations of bounds—ensembles and lists—to support both proof and computation. The results clarify that many non-classical logics fail the periodic sequence property, while IPC enjoys a linear-bound ultralps (ulps) behavior, enabling effective bound computation and fixpoint considerations. Overall, the work provides a rigorous, executable account of Ruitenburg's phenomenon in IPC and lays groundwork for exploring periodicity and fixpoints in broader logical families while offering a reusable Coq framework for related mechanizations.
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.