Арифметика Пресбургера
В этом разделе мы описываем выразимые множества в . Отметим сразу же, что с такой сигнатурой элиминация кванторов невозможна. В самом деле, формула
истинная для четных , не эквивалентна никакой бескванторной формуле. Поэтому нам нужно, прежде чем проводить элиминацию кванторов, расширить сигнатуру. Приведенный пример формулы подсказывает, какое расширение нам необходимо. Рассмотрим счетное семейство двуместных предикатных символов Символ будет интерпретироваться как равенство по модулю . Другими словами, формула будет истинна в нашей интерпретации, если сравнимо с по модулю (остатки по модулю равны; кратно ).
Важно иметь в виду, что индекс в не является переменной: у нас не трехместный предикат, а счетное семейство двуместных предикатов.
Такое расширение не меняет класса выразимых предикатов, поскольку, например, можно выразить как . Зато после этого всякая формула эквивалентна бескванторной, как показывает следующая теорема (называемая теоремой об элиминации кванторов в арифметике Пресбургера).
Теорема 32. В выполнима элиминация кванторов.
Мы будем применять метод, опробованный в предыдущем разделе: выбор представительного множества термов (после некоторых преобразований формулы).
Напомним, как это делается. Мы хотим доказать, что всякая формула эквивалентна бескванторной. Рассуждая по индукции, мы должны лишь проверить, что всякая формула вида
где обозначает бескванторную формулу, все переменные которой содержатся среди , эквивалентна некоторой бескванторной формуле (с теми же переменными, не считая ).
Посмотрим, какие атомарные формулы, содержащие переменную , входят в . Перенося члены в одну сторону, эти атомарные формулы можно записать в одном из трех видов: , или , где представляет собой линейную комбинацию переменных с целыми коэффициентами и целочисленным свободным членом. (В отличие от ситуации в , здесь нельзя делить на коэффициент при .) Перенося в левую часть, а все остальное — в правую, получаем соотношение одного из четырех видов:
где — положительное целое число (разное для разных атомарных формул), а — линейная комбинация переменных с целыми коэффициентами и свободным членом.
Как мы говорили, коэффициенты в левой части ( а также, разумеется, правые части) у разных атомарных формул разные. Однако мы можем их унифицировать, перейдя к общему кратному. В самом деле, неравенства и равенства можно умножать на число, сравнения — тоже, если модуль сравнения (индекс в ) умножить на то же самое число. Поэтому можно считать, что наша формула имеет вид , понимая под этим, что появляется только в левых частях и везде с коэффициентом . Такую формулу можно переписать как Таким образом, без ограничения общности можно считать, что , поскольку новая формула имеет тот же самый вид
что и исходная, но уже безо всякого коэффициента при (и с модифицированной формулой ). Пусть — выражения, стоящие в правых частях равенств, неравенств и сравнений с левой частью .
Мы хотим, как и в предыдущем разделе, указать представительный набор значений . Каждое из представляет собой линейную комбинацию переменных с целыми коэффициентами и свободным членом. "Представительность" означает, что если для каких-то найдется , для которого
то такой можно найти и среди значений (при тех же ).
Чтобы указать представительный набор, разделим все атомарные формулы в , содержащие , на два типа — сравнения по модулю и остальные (равенства и неравенства). Посмотрим, по каким модулям проводятся сравнения. Пусть — общее кратное всех этих модулей. В этом случае изменение значения переменной на величину, кратную , не влияет на результаты сравнений. Теперь возьмем все выражения, встречающиеся в правых частях равенств или неравенств, и будем прибавлять к ним всевозможные целые числа из отрезка от до . Это и будет представительный набор. Другими словами, в представительный набор входят все выражения , где — одна из правых частей равенств или неравенств, содержащих в левой части, а — целое число, не превосходящее по абсолютной величине.
Покажем, что полученный набор действительно будет представительным. Пусть при данных найдется некоторое , для которого . Посмотрим, какие значения принимают правые части равенств и неравенств при данных .
Если значение попало в объединение - окрестностей этих значений, то доказывать нечего. Если же нет, начнем смещать , двигаясь шагами размера в направлении какой-то точки из этого объединения. Миновать мы ее не можем (ширина окрестности равна , а размер шага равен ), поэтому в какой-то момент мы впервые попадем в это объединение. Обозначим эту точку (первую попавшую в объединение) через . Тогда при подстановке в дает те же самые результаты, что и . В самом деле, для сравнений это гарантировано, потому что сдвиг кратен модулю сравнений. Но это верно и для равенств и неравенств, поскольку на предыдущем шаге мы были вне -окрестности всех правых частей и потому не могли перейти с одной стороны на другую.
Таким образом, среди представительного набора есть значение (а именно, ), удовлетворяющее формуле , что и требовалось доказать.
Итак, мы получили ответ на интересующий нас вопрос: выразимые в арифметике Пресбургера предикаты — это предикаты, выразимые бескванторными формулами, содержащими целые константы, сложение, равенство, отношение порядка и сравнения по любым фиксированным модулям.
