Алгоритмы и логика

В этом заключительном разделе мы обсудим связи между логикой и теорией алгоритмов. Изложение будет более кратким, чем в остальных разделах. Многие важные факты оставлены в качестве задач для самостоятельного решения.

Используя понятия теории алгоритмов можно уточнить требования к формальным системам, которые описывают математическое рассуждение. Интуитивно ясное требование состоит в том, что множество аксиом и все правила вывода должны быть разрешимы. В самом деле, мы хотим разбить математическое рассуждение на элементарные шаги. Но тогда каждый такой шаг должен быть достаточно прост, чтобы допускать механическую проверку.

Из разрешимости множества формул, аксиом и правил вывода следует разрешимость множества всех выводов в данной формальной системе.

Задача 4.18. Приведите строгую формулировку предыдущего утверждения и докажите его.

Однако множество формальных теорем формальной системы с разрешимыми аксиомами и правилами вывода может оказаться неразрешимым.

Неразрешимость проверки общезначимости формул

Теорема 4.65. Множество общезначимых формул неразрешимо.

Конечно, такая краткая формулировка требует уточнения формулы это слова в бесконечном алфавите, а мы определяли разрешимость множеств лишь для слов в конечном алфавите. Поэтому нужно зафиксировать способ описания формул в конечном алфавите.

Мы сделаем это в два шага. Сначала сопоставим формулам конечные последовательности натуральных чисел. Для этого занумеруем символы в алфавите исчисления предикатов следующим образом:

символу переменной Xi сопоставим номер 5(г + 1) (г ^ 0), предикатному символу Pf (г-й символ арности к) сопоставим номер 5((^/ь+2⁺¹)+^+1) + 1' Функциональному символу /* (г-й символ арности к) сопоставим номер 5((^fc+2⁺¹)+^+l)+2. Странные формулы в этой нумерации имеют простое объяснение, которое мы сформулируем в виде задачи.

Задача 4.19. Докажите, что отображение.

является биекцией N х N на. N. Постройте алгоритмы, вычисляющее это отображение и обратное к нему.

Итак, мы сопоставляем формуле в исчислении предикатов (конечная последовательность символов в алфавите исчисления предикатов) конечную последовательность номеров символов.

Второй шаг состоит в том, чтобы закодировать конечные последовательности натуральных чисел словами в некотором конечном алфавите. Для этого будем использовать уже рассмотренную выше кодировку. Последовательность vi, V2, …, v_n будем кодировать словом.

в алфавите {#, 0,1}. Здесь v обозначает двоичную запись числа v.

Теперь можно уточнить формулировку теоремы 4.65: множество кодов общезначимых формул неразрешимо.

Доказательство теоремы 4.65. Сведём проблему равенства слов в полугруппах к проверке общезначимости формул в языке первого порядка.

Рассмотрим такой набор правил преобразования слов.

в алфавите А и два слова ?/, V, что левые и правые части правил преобразования непусты.

Напомним, что проблема равенства слов заключается в том, чтобы решить, эквивалентны ли слова U и V относительно заданных правил преобразования.

Мы построим формулу исчисления предикатов, которая будет общезначима тогда и только тогда, когда эти слова эквивалентны.

Построенное соответствие будет вычислимым, т. е. существует алгоритм, который по описанию слов U, V и правил подстановки строит код соответствующей формулы.

Далее рассуждаем стандартно: если бы существовал алгоритм проверки общезначимости формул, его можно было бы использовать для проверки общезначимости построенной формулы и получить тем самым алгоритм для решения проблемы равенства слов в полугруппах при отсутствии пустых слов в порождающих соотношениях (пустое слово это единица в полугруппе). Заметим, что в доказательстве теоремы 4.30 использовались только правила с непустыми левыми и правыми частями, так что этот частный случай также алгоритмически неразрешим.

Искомая формула имеет вид В->С, где В является конъюнкцией⁸^ п + 5 формул. Первые пять из них перечислим явно.

В этих формулах использован бинарный предикатный символ Е и бинарный функциональный символ т. Для кодирования считаем, что Е = Pq, т = /q.

При интерпретации символу Е соответствует бинарное отношение. Из истинности первых трёх формул следует, что это отношение является отношением эквивалентности (рефлексивность, симметричность и транзитивность в точности описываются этими формулами).

Напомним, что конъюнкция (и остальные использованные в рассуждении пропозициональные связки) выражается через 1 и —.

Интерпретацией символа т является некоторая бинарная операция, будем называть её умножением. Четвёртая формула означает, что умножение корректно: класс произведения не зависит от выбора представителей в классах сомножителей. Пятая формула утверждает ассоциативность умножения.

Таким образом, любая интерпретация с областью интерпретации М, в которой указанные выше формулы истинны, корректно определяет полугруппу на множестве М/Е классов эквивалентности отношения Е.

Остальные п членов конъюнкции В соответствуют правилам подстановки и имеют вид.

В этих формула использованы константы (0-арные функциональные символы) /_г°, которые соответствуют символам алфавита а*. Константа соответствует г-му символу левой части правила подстановки, а константа г* — г-му символ}' правой части.

Наконец формула С имеет вид, аналогичный (4.36). В ней соответствует г-му символу слова ?/, а г₇; — г-му слова V.

Описанное соответствие вычислимо (проверку этого утверждения оставляем читателю в качестве самостоятельного упражнения).

Если построенная формула Z?—общезначима, то слова U и V эквивалентны относительно данных правил подстановки. В самом деле, пусть множество слов в алфавите А служит областью интерпретации формулы J3—предикатный символ Е интерпретируется как отношение эквивалентности, а функциональный символ гп как умножение (конкатенация) слов. Тогда истинность В—>С в этой интерпретации означает равенство U = V в полугруппе А*/Е, что равносильно достижимости слова V из слова U преобразованиями из заданного набора правил.

В обратную сторону. Пусть слова U и V эквивалентны относительно данных правил подстановки. Рассмотрим некоторую интерпретацию формулы Я—на области Л/, в которой В истинна, (в противном случае J3—истинна). Это означает, что в полугруппе М/Е выполняются равенства, задаваемые всеми правилами подстановки. Но тогда в полугруппе выполняются равенства ULiU2 = URjU2 для любых слов U, U2 и любого правила подстановки Li Я*. Поэтому последовательность подстановок определяет цепочку равенств, которая начинается со слова U и заканчивается на слове V. Из транзитивности отношения Е заключаем, что истинна формула С. Это доказывает общезначимость формулы В—>С. ?

Из теоремы 4.65 и теоремы 3.65 о полноте исчисления предикатов следует, что исчисление предикатов является примером формальной системы, в которой аксиомы и правила вывода разрешимы (см. задачи 4.21−4.23), а множество выводимых формул неразрешимо (по теореме 4.65).

Задачи.

• 4.20. Предложите алгоритм проверки общезначимости формул, которые содержат только унарные предикатные и функциональные символы.
• 4.21. Докажите, что множество кодов формул исчисления предикатов разрешимо.
• 4.22. Докажите, что разрешимо множество {А, А—>В, В), где А, В формулы исчисления предикатов.
• 4.23. Докажите, что множество кодов аксиом исчисления предикатов разрешимо.