Назовем
алфавитом языка арифметики алфавит, состоящий из:
1) десятичных цифр для записи натуральных чисел
2) символа
и нижнего индекса для записи переменных (различные переменные, входящие в одно и то же выражение, можно обозначать
,
, ...).
3) знаков арифметических операций
,
4) скобок и знака равенства
5) знаков логических операций "и", "или", "не", кванторов существования
и всеобщности
.
Конечный упорядоченный набор символов языка арифметики назовем
фразой языка арифметики.
Существует класс фраз, называемых
суждениями. Его можно определить, определив индуктивно сначала терм, затем формулу, а уж затем - суждение как формулу без свободных параметров, но мне кажется, здесь это излишне. Понятие суждения в языке арифметике вполне совпадает с этим же понятием в логике. Например,
,
- суждения. На языке арифметики можно записать как вполне тривиальные суждения ("шесть делится на три"), так и очень нетривиальные (теорема Лагранжа - "всякое натуральное число представимо в виде суммы не более чем четырех квадратов натуральных чисел"), в том числе недоказанные (гипотеза Гольдбаха).
Теорема Геделя о неполноте утверждает:
Не существует алгоритма, который для каждого суждения языка арифметики определяет, истинно оно или ложно.
(Отметим, что алгоритм, который для каждой фразы языка арифметики определяет, является ли она суждением, существует и достаточно просто пишется: "в суждении есть знак равенства", "количество открытых скобок равно количеству закрытых", "все переменные входят в суждение под кванторами" и т.д.).
Вопрос:
Существует ли суждение языка арифметики, для которого ни один алгоритм не определяет, истинно оно или ложно?Конечно, такая формулировка неудачна. Всегда можно взять два алгоритма, один из которых всегда печатает "оно ложно", а другой "оно истинно", и сказать, что уж один-то из этих алгоритмов истинность/ложность утверждения определяет. Я не об этом. Не знаю, как сформулировать корректнее. Приведу пример. Похожая теорема доказывается для алгоритмов: "не существует алгоритма, которых для всякого алгоритма
и всяких входных данных
определял бы, остановится ли этот алгоритм при этих входных данных". Затем строится универсальный алгоритм
, который для каждой пары
реализует алгоритм
, где
- номер алгоритма
в эффективной нумерации всех алгоритмов. Получается, что для универсального алгоритма
не существует алгоритма, который для любого
определял бы, остановится ли
или нет.
Существует ли в языке арифметики "универсальное суждение", на проблеме истинности которого любой алгоритм споткнется так же, как на проблеме остановки универсального алгоритма?
Тут, конечно, есть разница. Универсальный алгоритм может принимать различные (да фактически любые) входные данные, и неразрешимость проблемы его остановки формулируется именно как "не существует алгоритма, который
для любого определял бы, остановится ли
или нет". Суждение же свободных параметров не содержит. И все-таки мне кажется, что какое-то такое "алгоритмически недоказуемое и неопровержимое суждение" должно существовать.
Или мне кажется?