Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 35
Текст из файла (страница 35)
И тот, и другой способы имеют недостатки,а выбор нами первого подхода — результат не единодушия авторов,а волевого решения.4.7. Предварённая нормальная формаГоворят, что формула находится в предварённой нормальной форме, если все кванторы в ней вынесены налево, то есть она имеет видQ1 ξ1 .
. . Qk ξk ϕ,в котором Q1 , . . . , Qk — кванторы (всеобщности или существования),ξ1 , . . . , ξk — переменные, а ϕ — бескванторная формула. Эта формуламожет иметь параметры (если формула ϕ имеет параметры, отличные от ξ1 , . . . , ξk ).Основной результат этого раздела гласит, что всякая формула(доказуемо) эквивалентна некоторой формуле в предварённой нормальной форме (предварённой формуле). Мы докажем его, одновременно построив некоторую классификацию формул (в каком-тосмысле отражающую их «логическую сложность»).
В качестве меры сложности можно было бы взять число кванторов в предварённойнормальной форме. Но правильнее учитывать число групп кванторов (считая одноимённые рядом стоящие кванторы за один).Говорят, что предварённая формула является Σn -формулой, если её кванторная приставка содержит n групп кванторов, причёмпервыми стоят кванторы существования. Если первыми стоят кванторы всеобщности, говорят о классе Πn . (Аналогичные обозначенияиспользуются в теории алгоритмов для классификации арифметических множеств, см. [5]).Скажем, формула ∀x∃y∃z∀u (A(x, u, z) → B(z, u)) принадлежитклассу Π3 , формула ∃u∀v C(u, v) принадлежит классу Σ2 , а формула∀x (A(x) → ∃yB(x, y)) вообще не находится в предварённой нормальной форме.158Исчисление предикатов[гл.
4]103. Указать формулу в предварённой нормальной форме, доказуемоэквивалентную последней из перечисленных формул.Нас интересует, что происходит с измеряемой таким образом «логической сложностью» формулы при логических операциях. Начнёмс совсем простых наблюдений.• Всякая формула из класса Σn или Πn доказуемо эквивалентна формуле из класса Σn+1 , а также формуле из класса Πn+1 .В самом деле, если формула ψ не имеет параметра η, то онабудет доказуемо эквивалентна формулам ∃η ψ и ∀η ψ (одна импликация является аксиомой, другая получается из ψ → ψ поправилу Бернайса).
Таким образом, можно добавить фиктивный квантор в начало кванторной приставки или в её конец; вовтором случае надо сослаться на лемму 2 раздела 4.6 (с. 155).• Отрицание любой формулы из класса Σn доказуемо эквивалентно некоторой формуле из класса Πn и наоборот. В самомделе, мы видели, что ¬∃ξ ψ выводимо эквивалентно ∀ξ ¬ψ инаоборот (с. 141), так что отрицание можно проносить внутрь,меняя по ходу дела кванторы на двойственные.• Конъюнкция любых двух формул из Π1 доказуемо эквивалентна некоторой формуле из Π1 . Например, конъюнкция ∀x A(x)∧∧ ∀y B(y) доказуемо эквивалентна формуле ∀x∀y (A(x) ∧ B(y)).В самом деле, используя аксиомы про квантор всеобщности,можно из ∀x A(x) вывести A(x), а из ∀y B(y) вывести B(y), поэтому из их конъюнкции выводится A(x) ∧ B(y), после чегоможно навесить два квантора всеобщности.
В другую сторону:выводим формулу ∀x∀y (A(x) ∧ B(y)) → A(x), затем применяем правило Бернайса и т. д.104. Покажите, что можно сэкономить один квантор и использоватьформулу ∀x (A(x) ∧ B(x)).Общее рассуждение (для любых двух формул из класса Π1 )почти столь же просто, надо лишь переименовать связанныепеременные, пользуясь теоремой 52 (с. 155).• Аналогично можно доказать, что дизъюнкция двух формул изкласса Σ1 доказуемо эквивалентна некоторой формуле класса Σ1 . (Можно также перейти к двойственному классу Π1 , воспользовавшись уже известными свойствами отрицания.)[п. 7]Предварённая нормальная форма159• Покажем теперь, что конъюнкция двух формул из класса Σ1доказуемо эквивалентна формуле класса Σ1 и что дизъюнкция двух формул класса Π1 доказуемо эквивалентна формулекласса Π1 .
Для этого надо воспользоваться эквивалентностямивида∃x A(x) ∧ ∃y B(y) ↔ ∃x∃y(A(x) ∧ B(y))и∀x A(x) ∨ ∀y B(y) ↔ ∀x∀y(A(x) ∨ B(y)).Отметим кстати, что в них уже нельзя сэкономить квантор;например, формула ∃x(A(x) ∧ B(x)) не равносильна формуле∃x A(x) ∧ ∃x B(x). (В одном из выступлений времён начала перестройки М.
С. Горбачёв сказал, что нужны «преданные делусоциализма, но квалифицированные специалисты» — впрочем,в газетной публикации «но» было заменено на нейтральное «и».Так вот, их существование не вытекает из отдельного существования тех и других.)Указанные эквивалентности, как легко видеть, общезначимыи потому выводимы.
Это совсем просто понять для первой изних (чтобы найти пару объектов с заданными свойствами, надо найти отдельно первый и второй члены пары). Вторая эквивалентность немного сложнее — проще всего заметить, чтоона переходит в первую при добавлении отрицания. (Большаясложность отражает тот факт, что вторая эквивалентность, вотличие от первой, не является интуиционистски верной.)• Теперь легко понять, что конъюнкция и дизъюнкция двух формул из класса Σn (или Πn ) доказуемо эквивалентны формуламиз того же класса. В самом деле, с помощью указанных вышеэквивалентностей можно слить кванторные приставки. Например, формула∀x∃y A(x, y) ∨ ∀u∃v B(u, v)доказуемо эквивалентна сначала формуле∀x∀u (∃y A(x, y) ∨ ∃v B(u, v)),а затем формуле∀x∀u∃y∃v (A(x, y) ∨ B(u, v)).105.
Как сэкономить один квантор в этом преобразовании?160Исчисление предикатов[гл. 4]Теперь всё готово для доказательства упомянутого в начале раздела результата.Теорема 53 (о предварённой нормальной форме). Любая формулапроизвольной сигнатуры доказуемо эквивалентна некоторой формуле той же сигнатуры, имеющей предварённую нормальную форму. Индукция по построению формулы. Для атомарных формулэто очевидно. Отрицание переводит формулу класса Σn в класс Πnи наоборот. Конъюнкция и дизъюнкция: приведём каждую формулу к предварённой нормальной форме, затем добавим фиктивныекванторы так, чтобы они попали в один класс, а затем воспользуемся доказанным утверждением. Импликация сводится к дизъюнкциии отрицанию (ϕ → ψ доказуемо эквивалентно ¬ϕ ∨ ψ).
Отметим, что ни формулировка, ни доказательство этой теоремыне предполагают замкнутости формулы.106. Привести к предварённой нормальной форме формулу ∀x A(x) →→ ∀x B(x).107. Формулы ϕ и ψ принадлежат классу ˚n . Найдём формулу в предварённой нормальной форме, выводимо эквивалентную формуле ϕ → ψ.В каком классе она окажется? (Указание: возможны разные варианты.)108. Применим описанный метод приведения к общезначимой формуле ∃x∀y A(x, y) → ∀y∃xA(x, y). Какая предварённая формула получится?(Естественно, она будет общезначимой.)4.8.
Теорема ЭрбранаЕстественно ожидать, что вопрос о выводимости (или общезначимости) формулы тем сложнее, чем сложнее сама формула. В этомразделе (а также в следующем) мы рассмотрим его для формул класса Σn и Πn .Начнём с самого простого случая. Пусть ϕ — бескванторная формула. Посмотрим, из каких атомарных формул она составлена, и заменим их на пропозициональные переменные (разные — на разные,одинаковые — на одинаковые). Получится формула логики высказываний, которую мы будем называть прототипом формулы ϕ. Имеетместо следующее (почти очевидное) утверждение.Теорема 54 (выводимость бескванторных формул). Бескванторная формула выводима (общезначима) тогда и только тогда, когдаеё прототип является тавтологией.
Если прототип формулы ϕ является тавтологией, то формула ϕявляется частным случаем пропозициональной тавтологии и потомувыводима и общезначима.[п. 8]Теорема Эрбрана161Пусть прототип формулы ϕ не является тавтологией. Можно считать, что формула ϕ замкнута, поскольку свободные переменные сточки зрения общезначимости и выводимости ничем не отличаются от констант (мы уже отмечали это при доказательстве теоремыо полноте).
Построим интерпретацию, где формула ϕ будет ложной.Носителем её будут замкнутые термы. Значения предикатов мы подберём так, чтобы атомарные формулы принимали те самые значения, которые делают прототип формулы ϕ ложным. Это возможно,так как значения разных атомарных формул можно выбирать независимо (это значения либо разных предикатов, либо одного и тогоже предиката, но на разных термах).
Что можно сказать про общезначимость формул классов Π1 и Σ1 ?Для класса Π1 всё просто: общезначимость формулы со свободнымипеременными равносильна общезначимости её замыкания (котороеполучается, если навесить кванторы всеобщности по всем переменным), поэтому формулы класса Π1 по существу ничем не отличаютсяот бескванторных.Вопрос для класса Σ1 решается следующей теоремой:Теорема 55 (Эрбрана). Формула ∃ξ1 . . . ∃ξk ϕ (где формула ϕ —бескванторная) общезначима тогда и только тогда, когда найдётсяконечный список подстановокϕ(t1 /ξ1 , .
. . , tk /ξk ),ϕ(u1 /ξ1 , . . . , uk /ξk ),....................ϕ(w1 /ξ1 , . . . , wk /ξk )(вместо переменных подставляются термы нашей сигнатуры), дизъюнкция которых общезначима.Заметим, что дизъюнкция, о которой идёт речь в теореме, является бескванторной формулой. По теореме 54 она общезначима тогдаи только тогда, когда является частным случае пропозициональнойтавтологии.Прежде чем доказывать эту теорему, приведём пример.
Рассмотрим формулу∃x (A(c, x) → A(x, d))(в которой c и d — константы). Она общезначима; соответствующийнабор состоит из подстановок c/x и d/x. В самом деле, формула(A(c, c) → A(c, d)) ∨ (A(c, d) → A(d, d))162Исчисление предикатов[гл. 4]истинна как при истинном A(c, d), так и при ложном. Заметим, чтов этом примере нам понадобились две подстановки. Доказательство теоремы Эрбрана. В одну сторону утверждение очевидно: если общезначима дизъюнкция подстановок, то общезначима формула с квантором. (Мы уже использовали это приэлиминации кванторов в разделе 3.6 при доказательстве теоремы 28.)Докажем обратное утверждение.
Будем считать, что формула ϕне содержит переменных, кроме ξ1 , . . . , ξk (как мы уже замечали,остальные переменные можно заменить константами). Рассмотрим(бесконечное) множество формул¬ϕ(t1 /ξ1 , . . . , tk /ξk )для всевозможных наборов замкнутых термов t1 , . . . , tk . Если этомножество противоречиво, всё доказано (тогда выводима дизъюнкция подстановок, отрицания которых используются при выводе противоречия). Если оно непротиворечиво, то существует интерпретация, в которой все эти формулы истинны.
Мы не можем утверждать,что в этой интерпретации ложна формула∃ξ1 . . . ∃ξk ϕ(носитель интерпретации может содержать элементы, не являющиеся значениями замкнутых термов). Однако если мы выбросим лишние элементы и оставим только значения термов, то эта формуластанет ложной, так что она не общезначима. Теорему Эрбрана можно сформулировать чисто синтаксически:если выводима Σ1 -формула ∃ξ1 . . . ∃ξk ϕ, то можно найти конечноечисло подстановок, дизъюнкция которых выводима. Можно предложить и доказательство, не использующее понятия общезначимости.Такое доказательство приведено, например, в книге Клини [16] (длягенценовского варианта исчисления предикатов) и в книге Шёнфилда [31] (для гильбертовского варианта).
Синтаксическое доказательство (в отличие от нашего) конструктивно: по выводу Σ1 -формулыможно алгоритмически указать соответствующие термы.Если сигнатура не содержит функциональных символов, то с помощью теоремы Эрбрана можно алгоритмически проверять выводимость формул класса Σ1 , поскольку число возможных подстановокконечно. Это же можно сказать и про формулы класса Π2 , так каквнешние кванторы всеобщности можно отбросить, не меняя выводимости.[п.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
