Ruitenburg's Theorem mechanized and contextualized
<|reference_start|>Ruitenburg's Theorem mechanized and contextualized: 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 (intuitionistic logic is not locally finite, even in a single variable). However, 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.<|reference_end|>
@article{litak2024ruitenburg's,
    title={Ruitenburg's Theorem mechanized and contextualized},
    author={Tadeusz Litak},
    journal={arXiv preprint arXiv:2402.01840},
    year={2024},
    archivePrefix={arXiv},
    eprint={2402.01840},
    primaryClass={cs.LO}
}