Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 21
Текст из файла (страница 21)
Однако при этом мы использовали кванторы, так чтодля (Z, =, <) элиминация кванторов невозможна.64. Убедитесь, что в самом деле формула y = S(x) не эквивалентнаникакой бескванторной формуле этой сигнатуры.Часто такой переход приходится выполнять в обратном направлении: у нас есть некоторая ситуация, в которой элиминация кванторов не проходит. Мы обходим эту трудность, добавив некоторыевыразимые предикаты и функции в нашу сигнатуру, после чего элиминация кванторов удаётся.
В этом случае мы получаем описаниевсех выразимых предикатов (предикат выразим, если он записывается бескванторной формулой расширенной сигнатуры). Мы встретимся с такой ситуацией дальше, говоря об арифметике Пресбургера(раздел 3.7).В некоторых случаях рассуждение упрощается, если привестибескванторную формулу к дизъюнктивной нормальной форме. Вотодин из таких примеров.Теорема 30. Всякая формула в (Q, =, <) эквивалентна некоторойбескванторной формуле. Как всегда, достаточно рассмотреть случай формулы вида∃x τ (x, x1 , . . . , xn ),где τ (x, x1 , . . . , xn ) — бескванторная формула.
Формулу τ можносчитать формулой в дизъюнктивной нормальной форме (теорема 4,с. 16). Напомним, это означает, что τ представляет собой дизъюнкцию конъюнкций, а каждая конъюнкция соединяет несколько литералов (атомарных формул или их отрицаний).В данном случае можно избавиться от отрицаний, заменив формулу ¬(x = y) на ((x < y) ∨ (x > y)), а формулу ¬(x < y) — на((x = y) ∨ (x > y)). После этого надо воспользоваться дистрибутивностью и вновь придти к дизъюнктивной нормальной форме — сбольшим числом членов, но уже без отрицаний.Теперь надо воспользоваться тем, что квантор существования(«бесконечную дизъюнкцию») можно переставлять с обычной дизъюнкцией.
Точнее говоря, мы пользуемся тем, что формулы ∃x (τ1 ∨τ2 )94Языки первого порядка[гл. 3]и ∃x τ1 ∨∃x τ2 эквивалентны. (Белый или чёрный единорог существует тогда и только тогда, когда существует белый единорог или существует чёрный единорог.) Это обстоятельство позволяет заменитьформулу∃x (τ1 ∨ τ2 ∨ . .
. ∨ τn )на∃x τ1 ∨ ∃x τ2 ∨ . . . ∨ ∃x τnи дальше разбираться с каждой из формул поодиночке.Итак, нам осталось преобразовать к бескванторному виду формулу∃x (ρ1 ∧ ρ2 ∧ . . . ∧ ρk ),где каждая из формул ρi соединяет какие-то две переменные знаком= или < (напомним, что от отрицаний мы уже избавились).Некоторые из формул ρi не содержат переменной x. Тогда ихможно вынести за квантор: если x не является параметром формулыα, то формулы ∃x (α ∧ β) и α ∧ ∃x β эквивалентны (если α истиннодля некоторых значений параметров, то в обеих формулах его можноопустить; если α ложно, то обе формулы ложны при этих значенияхпараметров).Вынеся такие формулы, можно считать, что под квантором остались лишь формулы вида x < xi , x = xi и x > xi , сравнивающие переменную x с какими-то другими переменными.
Если там есть хотьодно равенство, то квантор существования вырождается — его можно удалить вместе с переменной x, заменив её на ту переменную,которой она равна. Например, формулу ∃x ((x = y) ∧ A(x)) можнозаменить на A(y).Итак, остался случай, когда переменная x встречается лишь внеравенствах. Другими словами, нас спрашивают, найдётся ли значение x, большее каких-то переменных и меньшее каких-то других.Если все ограничения на x одного знака (только снизу или толькосверху), то такое значение x существует при любых значениях других переменных (поскольку в множестве Q нет ни наибольшего, нинаименьшего элементов). Что делать, если есть ограничения разныхзнаков? Пусть наша формула, например, имеет вид∃x ((x > a) ∧ (x > b) ∧ (x < c) ∧ (x < d)).Как записать условия на a, b, c, d, при которых это верно, не используя кванторов? Надо написать такую формулу:(a < c) ∧ (a < d) ∧ (b < c) ∧ (b < d).[п.
6]Элиминация кванторов95Мы хотим написать, что наибольшая из нижних границ меньше наименьшей из верхних, но поскольку заранее неизвестно, какая будетнаибольшей и какая наименьшей, мы пишем, что любая нижняяграница меньше любой верхней. Поскольку множество Q являетсяплотным (между любыми двумя элементами найдётся третий), тоэта формула равносильна исходной.Так, постепенно сводя дело ко всё более простым случаям, мызавершили рассуждение. Заметим, что в этом доказательстве из свойств рациональных чисел мы использовали лишь отсутствие наибольшего и наименьшегоэлемента и плотность. Поэтому все наши преобразования остаютсяэквивалентными для любого упорядоченного множества с такимисвойствами, а не только для Q.
Применив эти преобразования к замкнутой формуле (формуле без параметров), мы получим или тождественно истинную формулу, или тождественно ложную (тольконадо добавить в язык константы для истины и лжи, чтобы не использовать фиктивных переменных, когда надо написать тождественноистинное или тождественно ложное выражение).
Отсюда мы заключаем, что во всех плотных упорядоченных множествах без первогои последнего элемента справедливы одни и те же формулы нашейсигнатуры. Как говорят, все такие множества элементарно эквивалентны с точки зрения нашей сигнатуры, см. раздел 3.9. (Другоедоказательство этого факта можно получить, используя теорему Левенгейма – Сколема о счётной подмодели и теорему об изоморфизмесчётных плотных линейно упорядоченных множеств без первого ипоследнего элементов, см. раздел 3.11.)В частности, мы доказали, что для рациональных и действительных чисел истинны одни и те же формулы сигнатуры (=, <).Ещё одним побочным продуктом нашего рассуждения (как и других рассуждений об элиминации кванторов) является способ выяснить, будет ли данная замкнутая формула истинной или ложной врассматриваемой интерпретации. Для этого надо привести её к бескванторному виду и посмотреть, получится ли И или Л.
Другимисловами, элиминация кванторов устанавливает разрешимость элементарной теории рациональных чисел с отношениями равенства ипорядка.Элиминация кванторов остаётся возможной (и рассуждение даже немного упрощается), если рациональные (или действительные)числа рассматривать не только с равенством и порядком, но и со сло-96Языки первого порядка[гл.
3]жением и рациональными константами. В этом случае можно воспользоваться приведённой ранее схемой с конечным представительным набором термов. В самом деле, пусть x — переменная, которую(вместе с квантором существования по ней) мы хотим элиминировать. Все атомарные формулы, её содержащие, можно «разрешить»относительно x, получив некоторое количество формул вида x = ti ,x > ti и x < ti , где ti — линейные комбинации остальных переменных с рациональными коэффициентами. (Разрешение рациональныхкоэффициентов вместо целых ничего не меняет, так как можно привести всё к общему знаменателю и получить целые коэффициенты,затем перенести отрицательные коэффициенты в другую часть, аположительные заменить многократным сложением.)Затем в качестве представительного набора надо взять набор, состоящий, во-первых, из всех ti , во-вторых, из всех средних арифметических (ti + tj )/2, и, наконец, из выражений ti − 1 и ti + 1.
Ясно,что как бы ни расположились точки ti на числовой оси, этот набор захватит как минимум по одной точке из каждого промежутка(средние арифметические нужны для интервалов, а прибавление ивычитание единицы — для лучей по краям).65. Провести это рассуждение подробно.Возможность элиминации кванторов в только что рассмотренной ситуации (Q, =, <, +, рациональные константы) имеет интересное геометрическое применение.Теорема 31.
Предположим, что единичный квадрат разрезан нанесколько квадратов. Тогда все они имеют рациональные стороны. Пусть дано такое разрезание с n меньшими квадратами. Напишем формулу с 3n параметрами (n из которых соответствуют размерам меньших квадратов, а 2n — координатам их левых верхнихуглов), которая говорит, что эти параметры действительно задаютразрезание квадрата (квадраты содержатся внутри единичного, неимеют общих точек и всякая точка единичного квадрата покрывается хотя бы одним из меньших квадратов).
Навесив кванторы существования по переменным, задающим координаты, получим формулу F (x1 , . . . , xn ) с параметрами x1 , . . . , xn , которая истинна, когда изквадратов размеров x1 , . . . , xn можно составить единичный квадрат.Элиминация кванторов позволяет считать, что формула F бескванторная, то есть представляет собой логическую комбинацию равенств и неравенств вида c1 x1 + .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
