О логике доказуемости арифметики Нибергалля

К.-Г. Нибергалль привел известный пример неперечислимой непротиворечивой теории, расширяющей арифметику Пеано PA, в которой доказуема естественная формализация утверждения о собственной непротиворечивости. В докладе будет рассмотрен вопрос об аксиоматизации логики доказуемости данной теории (относительно арифметики Пеано), которая представляет собой нормальную модальную логику, не сравнимую по включению с логикой доказуемости Гёделя-Лёба. Мы установим финитную аппроксимируемость и опишем класс всех шкал Крипке данной логики. Также мы опишем её замкнутый фрагмент и универсальную модель Крипке для замкнутого фрагмента.
С точки зрения модальной логики данная логика интересна тем, что содержит аксиому [ ][ ] p -> [ ][ ][ ] p, но не содержит стандартную аксиому транзитивности и при этом является финитно аппроксимируемой и разрешимой. Однако, к сожалению, на данный момент нам не известно явного описания аксиом этой логики.