Ruitenburg's Theorem Mechanized and Contextualized
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912686992785408 |
|---|---|
| author | Litak, Tadeusz |
| author_facet | Litak, Tadeusz |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_01840 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Ruitenburg's Theorem Mechanized and Contextualized Litak, Tadeusz Logic in Computer Science 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. |
| title | Ruitenburg's Theorem Mechanized and Contextualized |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2402.01840 |