про эшелоны это я так выразился, для поэтичности: каждому "эшелону" соответствует формальная теория в которой известно простое недоказуемое Пи_2 утверждение.
Большие числа получаются из известных недоказуемых Пи_2 утверждений, достаточно вставить вместо переменной из-под универсального квантора первое число, для которого известно, что явление уже действует (в теории рамсея функции разгоняются не сразу, а через несколько шагов).
Про разные теории можно почитать в книжке S.Simpson "Subsystems of second-order arithmetic".
Про недоказуемость - в моей недавней писульке здесь:
articleПро t(n) (и про соответствующие большие числа из диофантовыx игр) я пока серьезно не думал, хотя кое-какие банальности про доказуемо-рекурсивные функции сказать мог бы.