decidable?

Всем известно, что арифметика сложения (Presburger arithmetic) разрешима, т.е. существует (хоть и очень медленный) алгоритм, определяющий истиность или ложность любого заданного утверждения. Более того, арифметику сложения можно обобщить разными спосбами, не теряя разрешимости. Туда можно добавить инструментарий для вычисления двоичных разложений чисел и экзистенциальный фрагмент арифметики делимости.

Известно, что язык арифметики сложения как таковой слишком слаб для гёделева кодирования доказательств в эрбрандовой нормальной форме и тем более для кодирования утверждения Contradiction(p), означающего что доказательство с гёделевым кодом p доказывает противоречие. Но я не вижу причин, почему это нельзя было закодировать в одном из разрешимых обобщений. Утверждение Cons(a) = “∀ p : P(p). !Contradiсtion(p)”, естественно, выходило бы за пределы разрешимого фрагмента теории, и, таким образом, в теорему Гёделя мы бы не упирались, а инструмент для релативированной проверки непротиворечивости теорий имели. (Т.е. могли бы за конечное время убедиться, что для заданного n никакие доказательства длиной менее n в данной теории к противоречиям не приводят.)

Чёт я на эту тему искал-искал публикации, а не нашёл ничего.

Upd: Написал мейл Дану Ўилларду (крупному специалисту по этой тематике) — посмотрим, что ответит и ответит ли.