Неразрешимость логики доказуемости второго порядка с операцией сравнения свидетелей

Пусть $\mathscr{L}^2$ – пропозициональный язык с двуместной модальностью $\rhd$ и кванторами по пропозициональным переменным. Рассмотрены формулы языка $\mathscr{L}^2$ которые доказуемы в арифметике Пеано при следующем переводе: переменные пробегают множество арифметических предложений, а модальность $A\rhd B$ интерпретируется как "формула $A$ доказуема не позже чем $B$". Доказана неразрешимость множества таких формул.
Библиогр. 2.