{'fraction_non_alphanumeric': 0.052547770700636945, 'fraction_numerical': 0.01194267515923567, 'mean_word_length': 4.929245283018868, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
The periodic sequence property

In 1984, Wim Ruitenburg [19] published a surprising result1 about the intuitionistic propositional calculus (IPC). It does not seem well-known: one of the few researchers making extensive use of it was the late Sergey Mardaev [9–13]; apart from it, some recent references quoting Ruitenburg’s paper include Ghilardi et al. [6] or Humberstone’s monograph [7]. Moreover, most of these references use it in the context of definability (eliminability) of fixpoints, where it is just one of possible lines of attack (the other being via uniform interpolation [16]; see [6] for a discussion). The property established by Ruitenburg deserves more attention though: to begin with, it turns out to be a natural generalization of local finiteness. Consider a propositional formula A. Fix a propositional variable p, which can be thought of as representing the context hole or the argument of A taken as a polynomial (other propositional variables being additional constants). Given any other formula B, write A(B) for the result of substituting B for p. Also, write A ≡L B for `L A↔ B. Now define the obvious iterated substitution operation A(p) := p,A(p) := A(A(p)). Such a sequence turns almost immediately into a cycle modulo ≡CPC: