Арифметика второго порядка и автономная вычислимость

Автономный процесс может быть описан либо в рамках арифметики второго порядка, либо близкой к ней теории Цермело–Френкеля (без аксиомы степени), что удобно. Ключевую роль играет следующий результат: доказывается, что если какой-нибудь автономный оракул дает модель для арифметики второго порядка, то он автоматически дает модель для теории Цермело–Френкеля (без аксиомы степени), которая естественно интерпретируется на наследственно-счетных множествах, легко представимых посредством счетных деревьев с обрывом цепей. Вообще, любой автономный процесс может быть описан в системе Цермело–Френкеля (без аксиомы степени), причем это описание абсолютное относительно любой оракульной модели. Следовательно, не может быть автономного процесса, дающего модель для полной теории арифметики второго порядка.