Dilators and the reverse mathematics zoo
Dilators and the reverse mathematics zoo
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 $\Pi^1_2$-formula is equivalent to the statement that some predilator is a dilator. We show how this completeness result breaks down without arithmetical comprehension: …