Dilators and the reverse mathematics zoo

Abstract

A predilator is a particularly uniform transformation of linear orders. We have a dilator when the transformation preserves well-foundedness. Over the theory ${\mathsf{ACA}}_0$ from reverse mathematics, any ${\hat{I}}_2^1$-formula is equivalent to the statement that some predilator is a dilator. We show how this completeness result breaks down without arithmetical comprehension: over ${\mathsf{RCA}}_0+\mathsf{PA}$, the statements from a large part of the reverse mathematics zoo are not equivalent to some predilator being a dilator.