Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

decidable?

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

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

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

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 2 comments