Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 36
Текст из файла (страница 36)
9]Сколемовские функции163Естественный вопрос: можно ли построить аналогичные алгоритмы для следующих классов? Отрицательный ответ даётся в следующем разделе.4.9. Сколемовские функцииВ этом разделе мы в разных формах используем ровно одну идею:истинность утверждения∀x∃y A(x, y)равносильна существованию функции, которая по любому x даёттакой y, что A(x, y). Это утверждение нельзя записать в виде эквивалентности∀x∃y A(x, y) ⇔ ∃f ∀x A(x, f (x)),поскольку в нашем языке нет квантора по функциям и ∃f мы писать не имеем права. (Языки, содержащие кванторы по множествами функциям, называются языками второго порядка и мы их не рассматриваем.)Тем не менее это утверждение можно сформулировать и в нашихтерминах.
Пусть, например, имеется формула ϕ с двумя параметрами x и y. Тогда замкнутая формула ∀x∃y ϕ выполнима тогда итолько тогда, когда выполнима формула ∀xϕ(f (x)/y), где f — новый одноместный функциональный символ. (Аккуратный читательпоправит: надо ещё требовать, чтобы подстановка f (x) вместо y была корректна. Мы уже знаем, что переменные можно переименовывать, поэтому будем легкомысленно считать, что все необходимыепереименования уже сделаны.)Аналогичное можно преобразовать произвольные предварённыеформулы.
Например, формула∀x∀y∃z∀u∃v ϕ(x, y, z, u, v)выполнима тогда и только тогда, когда выполнима формула∀x∀y∀u ϕ(x, y, f (x, y), u, g(x, y, u))(здесь ϕ(x, y, z, u, v) — формула, не имеющая параметров, кроме явно указанных x, y, z, u, v, запись ϕ(x, y, f (x, y), u, g(x, y, u)) обозначает результат соответствующих подстановок, которые мы предполагаем корректными, а f и g — функциональные символы, не встречающиеся в формуле ϕ).164Исчисление предикатов[гл. 4]Сходное преобразование имеют в виду преподаватели математического анализа, которые иногда записывают определение предела(∀ε∃δ . .
.) в несколько странной для логика форме ∀ε∃δ = δ(ε) . . . —имеется в виду, что если для каждого ε найдётся δ, то это самое δпредставляет собой функцию от ε.Отметим, что это рассуждение использует аксиому выбора, когдаиз различных возможных (для данного ε) значений δ мы выбираемкакое-то одно и объявляем его значением функции δ(ε).109. Казалось бы, выбор v в приведённом выше примере зависит отx, y, z, u, так что следовало бы написать ϕ(x, y, f (x, y), u, g(x, y, f (x, y), u)),но мы так не делаем. Почему это допустимо?В общем случае мы получаем такое утверждение:Теорема 56.
Для всякой замкнутой формулы τ сигнатуры σ можно указать формулу τ 0 класса Π1 сигнатуры σ с добавленными функциональными символами, которая выполнима или невыполнима одновременно с формулой τ . При этом преобразование τ 7→ τ 0 эффективно (выполняется некоторым алгоритмом). Приведя τ к предварённой нормальной форме, получим доказуемо эквивалентную формулу (выполнимую или невыполнимуюодновременно с τ ). После этого применяем описанное выше преобразование. Формула τ невыполнима тогда и только тогда, когда её отрицание общезначимо. Поэтому наши рассуждения показывают, что,скажем, формула ¬∀x∃y ψ(x, y) общезначима одновременно с формулой ¬∀x ψ(x, f (x)). Внося отрицание внутрь и заменяя ¬ψ на ϕ,получаем такое утверждение: формулы∃x∀y ϕ(x, y) и∃x ϕ(x, f (x))одновременно общезначимы.
(Это утверждение чуть менее наглядно,чем двойственное ему утверждение о выполнимости.) В общем видедвойственное к теореме 56 утверждение выглядит так:Теорема 57. Для всякой замкнутой формулы τ сигнатуры σ можно указать формулу τ 0 класса Σ1 сигнатуры σ с добавленными функциональными символами, которая общезначима или необщезначимаодновременно с формулой τ .
При этом преобразование τ 7→ τ 0 эффективно (выполняется некоторым алгоритмом).Заметим, что к формуле τ 0 можно применить теорему Эрбрана(с. 161): она общезначима тогда и только тогда, когда дизъюнкциянескольких подстановок является тавтологией.[п. 9]Сколемовские функции165Теорема о полноте позволяет заменить в этой формулировке общезначимость на выводимость: формулы τ и τ 0 одновременно выводимы. После этого естественно искать явный метод, который преобразует вывод формулы τ в вывод формулы τ 0 и обратно. Такой методдействительно существует, но для этого требуется более детальныйанализ структуры выводов, при котором удобно пользоваться исчислениями генценовского типа.Идея использования функций вместо групп кванторов ∀∃ восходит к Эрбрану и Сколему. Такие функции иногда называют «эрбрановскими» или «сколемовскими», а их добавление — «сколемизацией».
Есть также термин «сколемовская нормальная форма», нов ней добавляются не функциональные символы, а предикатные, иполучается формула не класса Σ1 , как в теореме 57, а класса Σ2 .Теорема 58 (о сколемовской нормальной форме). Для всякой замкнутой формулы τ сигнатуры σ можно указать формулу τ 0 классаΣ2 сигнатуры σ с добавленными предикатными символами, котораяобщезначима или необщезначима одновременно с формулой τ . Приэтом преобразование τ 7→ τ 0 эффективно (выполняется некоторымалгоритмом).
Как и раньше, нам будет удобнее говорить о выполнимости идоказывать, что для всякой формулы τ найдётся одновременно с нейвыполнимая формула τ 0 из класса Π2 . Построение такой формулымы объясним на примере. Пусть исходная формула имеет вид∀x∀y∃z∀u∃v ϕ(x, y, z, u, v).Мы теперь не можем ввести функции f и g, как это делалось выше, на с. 163. Поэтому мы введём предикаты F и G, заменяющиеграфики этих функций, и напишем формулу∀x∀y∃z F (x, y, z)∧∀x∀y∀u∃v G(x, y, u, v)∧∀x∀y∀z∀u∀v (F (x, y, z) ∧ G(x, y, u, v) → ϕ(x, y, z, u, v))Если исходная формула выполнима, то новая тоже выполнима: достаточно взять в качестве F и G графики сколемовских функций.Напротив, если новая формула выполнима, то выполнима и старая(более того, из новой формулы следует старая): надо взять z и v согласно первым двум строкам и заметить, что согласно третьей строкеони подойдут.166Исчисление предикатов[гл. 4]Такая конструкция применима к любой предварённой форме идаёт конъюнкцию Π2 -формул (последняя из которых будет даже иΠ1 -формулой).
А мы знаем (с. 159), что такая конъюнкция эквивалентна Π2 -формуле. 110. Дайте синтаксическое доказательство теоремы о сколемовскойнормальной форме (показав, что из выводимости формулы следует выводимость её сколемовской нормальной формы и наоборот). (Указание: этопроще, чем для формул с функциональными символами, и не требуетсяиспользовать генценовское исчисление.)Утверждения этого раздела сводят вопрос о выводимости произвольной формулы исчисления предикатов к выводимости Σ1 -формулы (с функциональными символами). Если мы запрещаем функциональные символы, то вопрос о выводимости произвольной формулысводится к выводимости Σ2 -формулы.Как мы увидим в разделе 5.4 (теорема Чёрча, c.
191), вопрос овыводимости произвольных формул языка первого порядка неразрешим: не существует алгоритма, который бы по произвольной замкнутой формуле определял бы, выводима она или нет. Результатыэтого раздела показывают, что уже для формул класса Σ1 (с функциональными символами) или Σ2 (без них) такого алгоритма не существует, поскольку из него можно было бы получить и общий алгоритм.
(В предыдущем разделе мы видели, что для формул класса Σ1без функциональных символов такой алгоритм существует.)5. Теории и модели5.1. Аксиомы равенстваПусть сигнатура σ включает в себя двуместный предикат равенства (записываемый традиционно x = y). Интерпретация этой сигнатуры называется нормальной, если предикат равенства интерпретируется как тождественное совпадение элементов носителя.Возникает естественный вопрос. Пусть имеется некоторая теория T (множество замкнутых формул) в языке, сигнатура котороговключает равенство.
Мы знаем что теория имеет модель (интерпретацию, в которой все формулы из T истинны) тогда и только тогда,когда она непротиворечива. В каком случае она имеет нормальнуюмодель (нормальную интерпретацию, в которой все формулы из Tистинны)?Чтобы ответить на этот вопрос, введём аксиомы равенства. Пустьσ — произвольная сигнатура. Аксиомами равенства в сигнатуре σбудут формулы∀x (x = x),∀x∀y ((x = y) → (y = x)),∀x∀y∀z (((x = y) ∧ (y = z)) → (x = z))(называемые аксиомами рефлексивности, симметричности и транзитивности). Это ещё не всё. Для каждого функционального символамы формулируем аксиому равенства, которая говорит, что его значение не меняется, если аргументы заменить на равные. Например,для двуместного функционального символа f соответствующая аксиома выглядит так:∀x1 ∀x2 ∀y1 ∀y2 (((x1 = x2 ) ∧ (y1 = y2 )) → (f (x1 , y1 ) = f (x2 , y2 ))).Для предикатных символов аксиомы равенства говорят, что истинный предикат остаётся истинным, если заменить аргументы на равные.
Например, для двуместного предикатного символа A аксиоматакова:∀x1 ∀x2 ∀y1 ∀y2 (((x1 = x2 ) ∧ (y1 = y2 ) ∧ A(x1 , y1 ) → A(x2 , y2 )).(Нет необходимости специально говорить, что предикат, соответствующий символу A, остаётся ложным при замене аргументов наравные, так как равенство симметрично.)168Теории и модели[гл. 5]Теорема 59 (полноты для нормальных моделей). Теория T сигнатуры σ с равенством имеет нормальную модель тогда и только тогда,когда она остаётся непротиворечивой после добавления аксиом равенства. Прежде всего заметим, что теоремы о корректности и полноте(раздел 4.5) позволяют говорить о совместности вместо непротиворечивости.В нормальной модели теории T аксиомы равенства истинны, такчто в одну сторону утверждение теоремы очевидно.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
