Бар-индукция для классов в арифметике второго порядка

Основной результат о котором я планирую рассказать состоит в том, что в арифметике второго порядка схема βₙ-модельной рефлексии эквивалентна схеме трансфинитной индукции для фундированных Π¹ₙ частичных порядков X≺Y. Отмечу, что теоретико-доказательственная сила схемы βₙ-модельной рефлексии находится между Π¹ₙ-свертыванием и Π¹ₙ₊₁-свертыванием. Доказательство этого результата опирается на две конструкции, которые могут быть интересны и в отдельности. Во-первых, разработка соответствия между нефундированными доказательствами в логике первого порядка и фундированными инфинитарными доказательствами. Во-вторых, конструкция декартово замкнутой категории классов реляционных структур замкнутых относительно изоморфизмов и подструктур. В первом из двух докладов я опишу эти две достаточно простые конструкции. Во втором докладе я расскажу о том, как формализация этих двух конструкций в арифметике второго порядка позволяет получить основной результат.