pub_02.md 4.3 KB
Анти-теорема о полноте (привет Гёделю)
Пусть Σ — формальная система, конечная по:
множеству аксиом |A| = n < ∞
множеству правил вывода |R| = m < ∞
длине вывода l ≤ L < ∞ (максимальное число шагов)
размеру формулы s ≤ S < ∞ (максимальная длина строки)
Тогда Σ полна и непротиворечива.
Доказательство
1. Конечность множества утверждений
Все формулы ограничены длиной S, алфавит конечен → множество всех синтаксически корректных формул конечно.
Обозначим: |F| = N < ∞.
2. Перечислимость выводов
Для каждой формулы f ∈ F можно проверить:
Является ли f аксиомой? (перебор A, конечный)
Выводима ли f за ≤ L шагов? (перебор всех последовательностей длины ≤ L, конечный)
Число возможных выводов длины ≤ L: m^L · n — конечно.
3. Разрешимость
Для любой формулы f:
Перебираем все выводы длины ≤ L
Если найден вывод f — f доказуема (истинна в Σ)
Если найден вывод ¬f — f опровержима (ложна в Σ)
Если ни то, ни другое — f неразрешима в рамках ресурсов, но не принципиально недоказуема
Поскольку перебор конечен, для каждой f результат получается за конечное время.
4. Полнота
Для любой f ∈ F:
Либо f выводима (истинна)
Либо ¬f выводима (ложна)
Либо ни одно не выводимо за ≤ L шагов
Но третий случай — не "недоказуемость", а ограничение ресурса L. Увеличим L — получим результат.
В пределе (теоретическом, при L → ∞, но конечном для каждой конкретной f) — каждая f разрешима.
5. Непротиворечивость
Если Σ выводит f и ¬f — это обнаруживается за конечное время (перебор выводов).
Такая Σ бракуется. Работаем только с непротиворечивыми.
Ключевое отличие от Гёделя
| Гёдель | Антитеорема | |
|---|---|---|
| Длина вывода | Не ограничена | Ограничена L |
| Множество формул | Бесконечно (все конечные строки) | Конечно (ограниченные S) |
| Результат | Существуют недоказуемые истинные | Все разрешимы (при достаточных ресурсах) |
Интерпретация
"Неполнота" Гёделя — артефакт бесконечности.
"Полнота" конечной системы — следствие конечности.
В реальности: L и S огромны, но конечны. Перебор теоретически возможен, практически неосуществим.
Но это сложность, не принципиальная неразрешимость.
Следствие для машины Тьюринга
Конечная МТ (лента ограничена M ячеек, время ограничено T шагов):
Число состояний: |Q| · M^T · T — конечно
Либо остановится, либо войдёт в цикл длины ≤ |Q| · M^T
Цикл обнаруживается за конечное время
Проблема остановки разрешима для конечной МТ.