На странице "Теория доказательств" упомянуты "самопроверяющиеся теории".

Где бы про это почитать по-подробнее, с увязкой к современным языкам программирования?

Здравствуйте, Эйнсток Файр, Вы писали:

ЭФ>На странице "Теория доказательств" упомянуты "самопроверяющиеся теории".
ЭФ>Где бы про это почитать по-подробнее, с увязкой к современным языкам программирования?

https://en.wikipedia.org/wiki/Self-verifying_theories
Хотя из их названия может показаться, что это какие-то "супер-теории", на самом деле они гораздо банальнее. Это такие искусствено урезанные, куцые теории (значительно слабее арифметики Пеано), в которых невозможно сформулировать диагональный аргумент. Чтобы доказать свою непротиворечивость, они просто говорят "мамой клянусь" — ну, то есть, у них просто есть аксиома о собственной непротиворечивости (впрочем, они действительно непротиворечивы, что можно доказать в арифметике Пеано). Они интересны просто как курьёзы, демонстрирующие технические требования для применимости теоремы Гёделя. Я очень сомневаюсь, что у них есть какая-либо связь с языками программирования, т.к. в них (насколько я понимаю) невозможно доказать даже базовые классические теоремы о вычислимых функциях.

Здравствуйте, nikov, Вы писали:

ЭФ>>На странице "Теория доказательств" упомянуты "самопроверяющиеся теории".
ЭФ>>Где бы про это почитать по-подробнее, с увязкой к современным языкам программирования?

N>https://en.wikipedia.org/wiki/Self-verifying_theories

Арифметика Пеано (PA) на самом деле очень близко подходит к доказательству своей непротиворечивости. Для любого числа N, в PA можно доказать её ограниченную непротиворечивость, т.е. "В PA нет доказательства длиной ≤ N, которое приводило бы к противоречию" (где мы подставляем вместо переменной N её значение). Это немного не дотягивает до полноценного утверждения о непротиворечивости "Для любого числа N, в PA нет доказательства длиной ≤ N, которое приводило бы к противоречию" (где N — переменная, связанная квантором ∀).

Однако, непротиворечивость PA можно доказать, если воспользоваться дополнительной аксиомой о вполне-упорядоченности (well-ordering) многоэтажных многочленов с целыми положительными коэффициентами по скорости роста (которая очень интуитивна для большинства людей, если над ней чуть-чуть подумать). Ну, само собой, эту аксиому нельзя доказать в PA, и если она не очевидна, то для её доказательства уже нужна какая-то слабая версия теории множеств с хотя бы счётными ординалами и трансфинитной индукцией.

Здравствуйте, nikov, Вы писали:

N>Однако, непротиворечивость PA можно доказать, если воспользоваться дополнительной аксиомой о вполне-упорядоченности (well-ordering) многоэтажных многочленов с целыми положительными коэффициентами по скорости роста (которая очень интуитивна, если над ней чуть-учть подумать).

Многоэтажные многочлены — это расширение обычных многочленов, где в качестве степени переменной может использоваться не только натуральное число, но и другой многоэтажный многочлен (тем не менее, каждый из них остаётся конечной структурой, хотя и может иметь сколько угодно этажей). Например, n^(n^(n^3 + 1) + 2 * n^n + n^2 + 5) + 33 * n^(n^n + 7) + n^10 + n + 15. Они линейно упорядочены по скорости роста для n → ∞. Аксиома о вполне-упорядочении утверждает, что любая убывающая последовательность таких многочленов конечна. Если сесть и написать несколько таких последовательностей, то становится очевидно, почему это так.