О некоторых медленно сходящихся системах преобразований термов

Формулируются системы преобразований термов, число шагов работы которых на произвольном входе конечно, но не ограничивается никакой вычислимой функцией, доказуемо тотальной в арифметике Пеано $\mathsf{PA}$. Тем самым, утверждение о сходимости таких систем не доказуемо в $\mathsf{PA}$. Эти системы получаются из независимого комбинаторного утверждения, известного как принцип червя; их также можно рассматривать как вариант хорошо известной игры Геракла и гидры, введенной Дж. Парисом и Л. Кирби.
Библиография: 16 названий.