О разрешимости ∀∃-теории решётки Σ₁-предложений арифметики Пеано

Хорошо известно, что кроме булевой алгебры Линденбаума-Тарского, носителем которой являются классы T-доказуемой эквивалентности всех арифметических предложений, со всякой арифметической формальной системой T можно также связать решётки предложений ограниченной арифметической сложности. В. Ю. Шавруковым было доказано, что элементарная теория решётки Σ₁-предложений для непротиворечивой теории T неразрешима (и даже не является арифметической). В докладе будет изложена общая схема доказательства результата о разрешимости ∀∃-фрагмента элементарной теории решётки Σ₁-предложений для непротиворечивой перечислимой арифметической теории T. Доклад основан на статье П. Линдстрёма и В. Ю. Шаврукова "The ∀∃-theory of Peano Σ₁-sentences".