 A major stumbling block for proving Takeuti’s fundamental conjecture is that in \((\forall_2\bL)\) and \((\exists_2\rR)\) inferences the minor formula \(F(\{v\mid A(v)\})\) can have a much higher complexity than the principal (inferred) formula \(QX\,F(X)\). If, instead, one allowed these inferences only in cases where the ‘abstraction’ term \(\{v\mid A(v)\}\) had (in some sense) a lower complexity than \(QX\,F(X)\), cut elimination could be restored. To implement this idea, one introduces a hierarchy of sets (formally represented by abstraction terms) whose complexity is stratified by ordinal levels \(\alpha\), and a pertaining hierarchy of quantifiers \(\forall X^{\beta}\) and \(\exists X^{\beta}\) conceived to range over sets of levels \(&lt;\beta\). This is the basic idea underlying the ramified analytic hierarchy. The problem of which ordinals could be used for the transfinite iteration led to the concept of autonomous progressions of theories. The general idea of progressions of theories is very natural and we shall consider it first before discussing the autonomous versions.