Ранги рефлексии и ординальный анализ

Работа исследует обнаруженную авторами естественную структуру фундированного отношения частичного порядка на булевой алгебре предложений в языке арифметики второго порядка, связанную со схемами $\Pi_1^1$-рефлексии (равномерной рефлексии для формул кванторной сложности $\Pi_1^1$). Рассматривается отношение $A < B$, определяемое как "$B$ доказывает $\Pi_1^1$-рефлексию относительно $A$". Работа начинается с относительно простого наблюдения о том, что такое отношение, в отличие от его аналога в языке арифметики первого порядка, удовлетворяет условию обрыва убывающих цепей. Это наблюдение позволяет сопоставить каждой формуле рассматриваемого языка соответствующий ординальный ранг. Дальнейшие результаты проясняют возникающую общую картину связей между рефлексией и фундированностью, ординальным рангом и теоретико-доказательственными ординалами формальных теорий в языке арифметики второго порядка. Работа устанавливает соотношение между существующими подходами к ординальному анализу формальных теорий и будет очень полезна исследователям по теории доказательств. По ходу дела, как нередко бывает при появлении некоторой общей объединяющей идеи, получены ответы на многие сравнительно частные проблемы. Одним из таких вопросов был вопрос об свойствах, из которых следует фундированность систем ординальных обозначений, полученных на основе алгебр рефлексии. Авторы дали некоторое общее условие такого рода. Интересно, что направление решения этих вопросов оказалось совершенно не таким, как предполагалось.