Языки и исчисления

Элиминация кванторов: элиминация кванторов


При всей простоте метод доказательства невыразимости с помощью автоморфизмов страдает очевидным недостатком: очень часто требуемого автоморфизма нет. Например, натуральные числа с операцией прибавления единицы вообще не допускают никакого нетривиального автоморфизма. (Тем не менее там выразимо очень немногое, как мы вскоре увидим.) Целые числа с операцией прибавления единицы допускают автоморфизмы (сдвиги), но эти автоморфизмы не позволяют доказать, что отношение порядка невыразимо (поскольку оно устойчиво относительно сдвигов).

Более прямой метод доказательства состоит в том, что мы предъявляем некоторый класс

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

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

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

Теорема 28. Для всякой формулы рассматриваемой нами сигнатуры существует эквивалентная ей бескванторная формула.

Будем доказывать индукцией по построению (или, если угодно, по длине) формулы существование эквивалентной ей в

бескванторной формулы. Для удобства (чтобы рассматривать один случай, а не два) будем считать, что наша формула может содержать только кванторы существования, но не всеобщности. Это законно, так как формулы и эквивалентны.

Случай, когда есть атомарная формула, очевиден — она и так бескванторная. Если является конъюнкцией, дизъюнкцией или импликацией двух частей, достаточно заменить каждую часть на эквивалентную бескванторную (что можно сделать по предположению индукции).

Единственный содержательный случай — когда формула

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

пишут . Нам надо найти бескванторную формулу нашей сигнатуры, эквивалентную формуле

Формула представляет собой булеву комбинацию атомарных формул. Посмотрим на те атомарные формулы, которые содержат переменную . Атомарная формула представляет собой равенство двух термов ; здесь и — либо переменные, либо константа . Если переменная

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

Здесь — либо целая константа, либо выражение вида , где — какая-то другая переменная, а — целое число. Мы позволили себе слегка отступить от канонов, разрешив прибавлять и вычитать целые константы вместо того, чтобы применять функцию

в левой и правой частях равенства. Ясно, что это не меняет класса выразимых формул, зато позволяет оставить в левой части, а константу перенести в правую.

Теперь сравним формулу

с формулой

которую мы будет обозначать . Формула представляет собой дизъюнкцию формул, полученных в результате подстановки различных вместо в бескванторную формулу . (После подстановки можно вернуться к обычному виду записи формулы, заменив прибавление констант на нужное количество применений функции с той или другой стороны равенства.)

Очевидно, что если для каких-то значений переменных формула истинна, то для этих значений истинна и формула . В самом деле, если истинен -й член дизъюнкции, то в формуле в качестве можно взять значение выражения .

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



бесконечно, а выражений лишь конечное число.

Обозначим через формулу, которая получится из

заменой всех атомарных формул, содержащих , на тождественно ложные формулы. Сказанное выше объясняет, почему формула

эквивалентна дизъюнкции . Мы достигли цели — нашли бескванторную формулу, эквивалентную формуле .

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

Немного более сложное рассуждение понадобится, если добавить к сигнатуре отношение порядка.

Теорема 29. Всякая формула в (где — функция прибавления единицы) эквивалентна некоторой бескванторной формуле. (Как говорят, допускает элиминацию кванторов.)

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

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

Как же быть? Для данных значений числа делят числовую ось (точнее, множество целых чисел) на промежутки, и для выяснения истинности формулы нам надо попробовать (помимо всех ) хотя бы по одному числу из каждого промежутка. Это будет гарантировано, если мы напишем дизъюнкцию, в которую, помимо всех формул , войдут также формулы и . Это позволяет нам обойтись без формулы и благополучно завершить доказательство.

63. Проверьте, что добавление константы к этой сигнатуре не препятствует элиминации кванторов.

Что будет, если мы из этой сигнатуры удалим функцию ? Легко понять, что класс выразимых множеств не изменится, так как можно выразить как " является наименьшим элементом, большим ". Однако при этом мы использовали кванторы, так что для элиминация кванторов невозможна.

64. Убедитесь, что в самом деле формула не эквивалентна никакой бескванторной формуле этой сигнатуры.

Часто такой переход приходится выполнять в обратном направлении: у нас есть некоторая ситуация, в которой элиминация кванторов не проходит. Мы обходим эту трудность, добавив некоторые выразимые предикаты и функции в нашу сигнатуру, после чего элиминация кванторов удается. В этом случае мы получаем описание всех выразимых предикатов (предикат выразим, если он записывается бескванторной формулой расширенной сигнатуры). Мы встретимся с такой ситуацией дальше, говоря об арифметике Пресбургера.

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

Теорема 30. Всякая формула в эквивалентна некоторой бескванторной формуле.

Как всегда, достаточно рассмотреть случай формулы вида

где — бескванторная формула. Формулу

можно считать формулой в дизъюнктивной нормальной форме (теорема 4). Напомним, это означает, что представляет собой дизъюнкцию конъюнкций, а каждая конъюнкция соединяет несколько литералов (атомарных формул или их отрицаний).

В данном случае можно избавится от отрицаний, заменив на , а — на . После этого надо воспользоваться дистрибутивностью и вновь придти к дизъюнктивной нормальной форме — с большим числом членов, но уже без отрицаний.

Теперь надо воспользоваться тем, что квантор существования (который есть "бесконечная дизъюнкция") можно переставлять с дизъюнкцией. Точнее говоря, мы пользуемся тем, что формулы и

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

на

и дальше разбираться с каждой из формул поодиночке.

Итак, нам осталось преобразовать к бескванторному виду формулу

где каждая из формул соединяет какие-то две переменные знаком или (напомним, что от отрицаний мы уже избавились).

Некоторые из формул не содержат переменной . Тогда их можно вынести за квантор: если не является параметром формулы , то формулы и эквивалентны (если истинно для некоторых значений параметров, то в обеих формулах его можно опустить; если ложно, то обе формулы ложны при этих значениях параметров).

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

Итак, остался случай, когда переменная встречается лишь в неравенствах. Другими словами, нас спрашивают, найдется ли значение , большее каких-то переменных и меньшее каких-то других. Если все ограничения на одного знака (только снизу или только сверху), то такое значение

существует при любых значениях других переменных (поскольку в множестве нет ни наибольшего, ни наименьшего элементов). Что делать, если есть ограничения разных знаков? Пусть наша формула, например, имеет вид

Как записать условия на , при которых это верно, не используя кванторов? Надо написать такую формулу:

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

является плотным (между любыми двумя элементами найдется третий), то эта формула равносильна исходной.

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

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

В частности, мы доказали, что для рациональных и действительных чисел истинны одни и те же формулы сигнатуры .

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

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

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

65. Провести это рассуждение подробно.

Возможность элиминации кванторов в только что рассмотренной ситуации ( , рациональные константы) имеет интересное геометрическое применение.

Теорема 31. Пусть единичный квадрат разрезан на несколько меньших квадратов. Тогда все они имеют рациональные стороны.

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

Элиминация кванторов позволяет считать, что формула

бескванторная, то есть представляет собой логическую комбинацию равенств и неравенств вида

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

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

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

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

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

66. Описать выразимые предикаты, проведя элиминацию кванторов (и расширив сигнатуру, если нужно) для (а), где — произвольное бесконечное множество; (б); (в), где — операция прибавления единицы; (г), где — операция прибавления единицы; (д), где — операция прибавления единицы, а — одноместный предикат "быть степенью двойки".


Содержание раздела